THEOREM (Cantor-Bernstein-Schroeder)
*******
Suppose we have sets x and y, and injections f: x -> y and g: y -> x
Set(x) (x is a set)
& Set(y) (y is a set)
& ALL(a):[a e x => f(a) e y] (f: x -> y)
& ALL(a):[a e y => g(a) e x] (g: y -> x)
& Injection(f,x,y) (f is an injection)
& Injection(g,y,x) (g is an injection)
then there exists bijection k: x -> y
ALL(a):[a e x => k(a) e y] (k: x -> y)
& Bijection(k,x,y) (k is a bijection)
This proof written with the aid of, and mechanically verified by the author's DC Proof 2.0 software available at http://www.dcproof.com
Outline
*******
We start with sets x and y, injections f: x -> y and g: y -> x
From these, we construct, using the axioms of set theory and previously established lemmas, various sets and functions
that will be required:
px = the power set of x
py = the power set of y
px2 = the Cartesian prouduct of px with itself
xy = the Cartesian prouduct of x and y
imgF(s) = the image of s under f
imgG(s) = the image of s under g
cx(s) = the complement of s relative to x
cy(s) = the complement of s relative to y
h(s) = cx(imgG(cy(imgF(s))))
g' = the inverse of a suitable restriction (subset) of g
Then we prove that for subsets s1 and s1 of x, if s1 is a subset of s2, then h(s1) is also a subset of h(s2). We say
that h is increasing.
Using the Knaster-Tarski Fixed-Point Lemma, we establish the existence of a subset z of x such h(z)=z.
Then we construct the function k: x -> y such that
k(a) = f(a) if a e z
= g'(a) otherwise
Finally, we prove that k is required bijection.
DEFINITIONS & PREVIOUS RESULTS
******************************
Define: Subset
**************
1 ALL(a):ALL(b):[Subset(a,b) <=> ALL(c):[c e a => c e b]]
Axiom
Define: Injection
*****************
2 ALL(f):ALL(a):ALL(b):[Injection(f,a,b) <=> ALL(c):ALL(d):[c e a & d e a => [f(c)=f(d) => c=d]]]
Axiom
Define: Surjection
******************
3 ALL(f):ALL(a):ALL(b):[Surjection(f,a,b) <=> ALL(c):[c e b => EXIST(d):[d e a & f(d)=c]]]
Axiom
Define: Bijection
*****************
Both arguments a and b should represent a Set, and f should represent a function mapping a to b.
4 ALL(f):ALL(a):ALL(b):[Bijection(f,a,b) <=> Injection(f,a,b) & Surjection(f,a,b)]
Axiom
Knaster-Tarski Fixed-Point Lemma Proof
5 ALL(s):ALL(ps):ALL(f):[Set(s)
& Set(ps)
& ALL(a):[a e ps <=> Set(a) & Subset(a,s)]
& ALL(a):[a e ps => f(a) e ps]
& ALL(a):ALL(b):[a e ps & b e ps
=> [Subset(a,b) => Subset(f(a),f(b))]]
=> EXIST(a):[Set(a) & Subset(a,s) & f(a)=a]]
Axiom
Complement Function Lemma Proof
6 ALL(s1):ALL(ps1):[Set(s1) & Set(ps1)
& ALL(a):[a e ps1 <=> Set(a) & ALL(b):[b e a => b e s1]]
=> EXIST(f1):[ALL(a):[a e ps1 => f1(a) e ps1]
& ALL(a):[a e ps1 => ALL(c):[c e s1 => [c e f1(a) <=> ~c e a]]]]]
Axiom
Image Function Lemma Proof
7 ALL(s1):ALL(s2):ALL(ps1):ALL(ps2):ALL(f1):[Set(s1) & Set(s2) & Set(ps1) & Set(ps2)
& ALL(a):[a e s1 => f1(a) e s2]
& ALL(a):[a e ps1 <=> Set(a) & ALL(b):[b e a => b e s1]]
& ALL(a):[a e ps2 <=> Set(a) & ALL(b):[b e a => b e s2]]
=> EXIST(f2):[ALL(a):[a e ps1 => f2(a) e ps2]
& ALL(a):[a e ps1
=> ALL(c):[c e f2(a) <=> EXIST(d):[d e a & f1(d)=c]]]]]
Axiom
Complement of a Complement Lemma Proof
8 ALL(s):ALL(ps):ALL(f):[Set(s)
& Set(ps)
& ALL(a):[a e ps <=> Set(a) & ALL(b):[b e a => b e s]]
& ALL(a):[a e ps => f(a) e ps]
& ALL(a):[a e ps => ALL(b):[b e s => [b e f(a) <=> ~b e a]]]
=> ALL(a):[a e ps => f(f(a))=a]]
Axiom
Existence of Inverse Function Lemma Proof
9 ALL(x):ALL(y):ALL(f):[Set(x) & Set(y)
& ALL(a):[a e x => f(a) e y]
& ALL(a):[a e y => EXIST(b):[b e x & f(b)=a]]
& ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]
=> EXIST(f'):[ALL(a):[a e y => f'(a) e x]
& ALL(a):ALL(b):[a e x & b e y => [f'(b)=a <=> f(a)=b]]]]
Axiom
Inverses are Bijections Lemma Proof
10 ALL(set1):ALL(set2):ALL(func):ALL(inv):[Set(set1) & Set(set2)
& ALL(a):[a e set1 => func(a) e set2]
& ALL(a):[a e set2 => inv(a) e set1]
& ALL(a):ALL(b):[a e set1 & b e set2 => [inv(b)=a <=> func(a)=b]]
=> ALL(a):ALL(b):[a e set2 & b e set2 => [inv(a)=inv(b) => a=b]]
& ALL(a):[a e set1 => EXIST(b):[b e set2 & inv(b)=a]]]
Axiom
Suppose...
11 Set(x)
& Set(y)
& ALL(a):[a e x => f(a) e y]
& ALL(a):[a e y => g(a) e x]
& Injection(f,x,y)
& Injection(g,y,x)
Premise
Splitting out this premise into its component parts...
12 Set(x)
Split, 11
13 Set(y)
Split, 11
14 ALL(a):[a e x => f(a) e y]
Split, 11
15 ALL(a):[a e y => g(a) e x]
Split, 11
16 Injection(f,x,y)
Split, 11
17 Injection(g,y,x)
Split, 11
Apply the Power Set axiom (twice)
18 ALL(a):[Set(a) => EXIST(b):[Set(b)
& ALL(c):[c e b <=> Set(c) & ALL(d):[d e c => d e a]]]]
Power Set
19 Set(x) => EXIST(b):[Set(b)
& ALL(c):[c e b <=> Set(c) & ALL(d):[d e c => d e x]]]
U Spec, 18
20 EXIST(b):[Set(b)
& ALL(c):[c e b <=> Set(c) & ALL(d):[d e c => d e x]]]
Detach, 19, 12
21 Set(px)
& ALL(c):[c e px <=> Set(c) & ALL(d):[d e c => d e x]]
E Spec, 20
Define: px (the power set of x)
**********
22 Set(px)
Split, 21
23 ALL(c):[c e px <=> Set(c) & ALL(d):[d e c => d e x]]
Split, 21
24 Set(y) => EXIST(b):[Set(b)
& ALL(c):[c e b <=> Set(c) & ALL(d):[d e c => d e y]]]
U Spec, 18
25 EXIST(b):[Set(b)
& ALL(c):[c e b <=> Set(c) & ALL(d):[d e c => d e y]]]
Detach, 24, 13
26 Set(py)
& ALL(c):[c e py <=> Set(c) & ALL(d):[d e c => d e y]]
E Spec, 25
Define: py (the power set of y)
**********
27 Set(py)
Split, 26
28 ALL(c):[c e py <=> Set(c) & ALL(d):[d e c => d e y]]
Split, 26
Apply the Cartesian Product axiom
29 ALL(a1):ALL(a2):[Set(a1) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e a1 & c2 e a2]]]
Cart Prod
30 ALL(a2):[Set(px) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e px & c2 e a2]]]
U Spec, 29
31 Set(px) & Set(px) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e px & c2 e px]]
U Spec, 30
32 Set(px) & Set(px)
Join, 22, 22
33 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e px & c2 e px]]
Detach, 31, 32
34 Set'(px2) & ALL(c1):ALL(c2):[(c1,c2) e px2 <=> c1 e px & c2 e px]
E Spec, 33
Define: px2 (the Cartesian Product of px with itself)
***********
35 Set'(px2)
Split, 34
36 ALL(c1):ALL(c2):[(c1,c2) e px2 <=> c1 e px & c2 e px]
Split, 34
Apply the Image Function Lemma
37 ALL(s2):ALL(ps1):ALL(ps2):ALL(f1):[Set(x) & Set(s2) & Set(ps1) & Set(ps2)
& ALL(a):[a e x => f1(a) e s2]
& ALL(a):[a e ps1 <=> Set(a) & ALL(b):[b e a => b e x]]
& ALL(a):[a e ps2 <=> Set(a) & ALL(b):[b e a => b e s2]]
=> EXIST(f2):[ALL(a):[a e ps1 => f2(a) e ps2]
& ALL(a):[a e ps1
=> ALL(c):[c e f2(a) <=> EXIST(d):[d e a & f1(d)=c]]]]]
U Spec, 7
38 ALL(ps1):ALL(ps2):ALL(f1):[Set(x) & Set(y) & Set(ps1) & Set(ps2)
& ALL(a):[a e x => f1(a) e y]
& ALL(a):[a e ps1 <=> Set(a) & ALL(b):[b e a => b e x]]
& ALL(a):[a e ps2 <=> Set(a) & ALL(b):[b e a => b e y]]
=> EXIST(f2):[ALL(a):[a e ps1 => f2(a) e ps2]
& ALL(a):[a e ps1
=> ALL(c):[c e f2(a) <=> EXIST(d):[d e a & f1(d)=c]]]]]
U Spec, 37
39 ALL(ps2):ALL(f1):[Set(x) & Set(y) & Set(px) & Set(ps2)
& ALL(a):[a e x => f1(a) e y]
& ALL(a):[a e px <=> Set(a) & ALL(b):[b e a => b e x]]
& ALL(a):[a e ps2 <=> Set(a) & ALL(b):[b e a => b e y]]
=> EXIST(f2):[ALL(a):[a e px => f2(a) e ps2]
& ALL(a):[a e px
=> ALL(c):[c e f2(a) <=> EXIST(d):[d e a & f1(d)=c]]]]]
U Spec, 38
40 ALL(f1):[Set(x) & Set(y) & Set(px) & Set(py)
& ALL(a):[a e x => f1(a) e y]
& ALL(a):[a e px <=> Set(a) & ALL(b):[b e a => b e x]]
& ALL(a):[a e py <=> Set(a) & ALL(b):[b e a => b e y]]
=> EXIST(f2):[ALL(a):[a e px => f2(a) e py]
& ALL(a):[a e px
=> ALL(c):[c e f2(a) <=> EXIST(d):[d e a & f1(d)=c]]]]]
U Spec, 39
41 Set(x) & Set(y) & Set(px) & Set(py)
& ALL(a):[a e x => f(a) e y]
& ALL(a):[a e px <=> Set(a) & ALL(b):[b e a => b e x]]
& ALL(a):[a e py <=> Set(a) & ALL(b):[b e a => b e y]]
=> EXIST(f2):[ALL(a):[a e px => f2(a) e py]
& ALL(a):[a e px
=> ALL(c):[c e f2(a) <=> EXIST(d):[d e a & f(d)=c]]]]
U Spec, 40
42 Set(x) & Set(y)
Join, 12, 13
43 Set(x) & Set(y) & Set(px)
Join, 42, 22
44 Set(x) & Set(y) & Set(px) & Set(py)
Join, 43, 27
45 Set(x) & Set(y) & Set(px) & Set(py)
& ALL(a):[a e x => f(a) e y]
Join, 44, 14
46 Set(x) & Set(y) & Set(px) & Set(py)
& ALL(a):[a e x => f(a) e y]
& ALL(c):[c e px <=> Set(c) & ALL(d):[d e c => d e x]]
Join, 45, 23
47 Set(x) & Set(y) & Set(px) & Set(py)
& ALL(a):[a e x => f(a) e y]
& ALL(c):[c e px <=> Set(c) & ALL(d):[d e c => d e x]]
& ALL(c):[c e py <=> Set(c) & ALL(d):[d e c => d e y]]
Join, 46, 28
48 EXIST(f2):[ALL(a):[a e px => f2(a) e py]
& ALL(a):[a e px
=> ALL(c):[c e f2(a) <=> EXIST(d):[d e a & f(d)=c]]]]
Detach, 41, 47
49 ALL(a):[a e px => imgF(a) e py]
& ALL(a):[a e px
=> ALL(c):[c e imgF(a) <=> EXIST(d):[d e a & f(d)=c]]]
E Spec, 48
Define: imgF (function mapping subsets of x to their image under f)
************
50 ALL(a):[a e px => imgF(a) e py]
Split, 49
51 ALL(a):[a e px
=> ALL(c):[c e imgF(a) <=> EXIST(d):[d e a & f(d)=c]]]
Split, 49
Apply Image Function Lemma
52 ALL(s2):ALL(ps1):ALL(ps2):ALL(f1):[Set(y) & Set(s2) & Set(ps1) & Set(ps2)
& ALL(a):[a e y => f1(a) e s2]
& ALL(a):[a e ps1 <=> Set(a) & ALL(b):[b e a => b e y]]
& ALL(a):[a e ps2 <=> Set(a) & ALL(b):[b e a => b e s2]]
=> EXIST(f2):[ALL(a):[a e ps1 => f2(a) e ps2]
& ALL(a):[a e ps1
=> ALL(c):[c e f2(a) <=> EXIST(d):[d e a & f1(d)=c]]]]]
U Spec, 7
53 ALL(ps1):ALL(ps2):ALL(f1):[Set(y) & Set(x) & Set(ps1) & Set(ps2)
& ALL(a):[a e y => f1(a) e x]
& ALL(a):[a e ps1 <=> Set(a) & ALL(b):[b e a => b e y]]
& ALL(a):[a e ps2 <=> Set(a) & ALL(b):[b e a => b e x]]
=> EXIST(f2):[ALL(a):[a e ps1 => f2(a) e ps2]
& ALL(a):[a e ps1
=> ALL(c):[c e f2(a) <=> EXIST(d):[d e a & f1(d)=c]]]]]
U Spec, 52
54 ALL(ps2):ALL(f1):[Set(y) & Set(x) & Set(py) & Set(ps2)
& ALL(a):[a e y => f1(a) e x]
& ALL(a):[a e py <=> Set(a) & ALL(b):[b e a => b e y]]
& ALL(a):[a e ps2 <=> Set(a) & ALL(b):[b e a => b e x]]
=> EXIST(f2):[ALL(a):[a e py => f2(a) e ps2]
& ALL(a):[a e py
=> ALL(c):[c e f2(a) <=> EXIST(d):[d e a & f1(d)=c]]]]]
U Spec, 53
55 ALL(f1):[Set(y) & Set(x) & Set(py) & Set(px)
& ALL(a):[a e y => f1(a) e x]
& ALL(a):[a e py <=> Set(a) & ALL(b):[b e a => b e y]]
& ALL(a):[a e px <=> Set(a) & ALL(b):[b e a => b e x]]
=> EXIST(f2):[ALL(a):[a e py => f2(a) e px]
& ALL(a):[a e py
=> ALL(c):[c e f2(a) <=> EXIST(d):[d e a & f1(d)=c]]]]]
U Spec, 54
56 Set(y) & Set(x) & Set(py) & Set(px)
& ALL(a):[a e y => g(a) e x]
& ALL(a):[a e py <=> Set(a) & ALL(b):[b e a => b e y]]
& ALL(a):[a e px <=> Set(a) & ALL(b):[b e a => b e x]]
=> EXIST(f2):[ALL(a):[a e py => f2(a) e px]
& ALL(a):[a e py
=> ALL(c):[c e f2(a) <=> EXIST(d):[d e a & g(d)=c]]]]
U Spec, 55
57 Set(y) & Set(x)
Join, 13, 12
58 Set(y) & Set(x) & Set(py)
Join, 57, 27
59 Set(y) & Set(x) & Set(py) & Set(px)
Join, 58, 22
60 Set(y) & Set(x) & Set(py) & Set(px)
& ALL(a):[a e y => g(a) e x]
Join, 59, 15
61 Set(y) & Set(x) & Set(py) & Set(px)
& ALL(a):[a e y => g(a) e x]
& ALL(c):[c e py <=> Set(c) & ALL(d):[d e c => d e y]]
Join, 60, 28
62 Set(y) & Set(x) & Set(py) & Set(px)
& ALL(a):[a e y => g(a) e x]
& ALL(c):[c e py <=> Set(c) & ALL(d):[d e c => d e y]]
& ALL(c):[c e px <=> Set(c) & ALL(d):[d e c => d e x]]
Join, 61, 23
63 EXIST(f2):[ALL(a):[a e py => f2(a) e px]
& ALL(a):[a e py
=> ALL(c):[c e f2(a) <=> EXIST(d):[d e a & g(d)=c]]]]
Detach, 56, 62
64 ALL(a):[a e py => imgG(a) e px]
& ALL(a):[a e py
=> ALL(c):[c e imgG(a) <=> EXIST(d):[d e a & g(d)=c]]]
E Spec, 63
Define: imgG (function mapping subsets of y to their image under g)
************
65 ALL(a):[a e py => imgG(a) e px]
Split, 64
66 ALL(a):[a e py
=> ALL(c):[c e imgG(a) <=> EXIST(d):[d e a & g(d)=c]]]
Split, 64
Apply Complement Function Lemma
67 ALL(ps1):[Set(x) & Set(ps1)
& ALL(a):[a e ps1 <=> Set(a) & ALL(b):[b e a => b e x]]
=> EXIST(f1):[ALL(a):[a e ps1 => f1(a) e ps1]
& ALL(a):[a e ps1 => ALL(c):[c e x => [c e f1(a) <=> ~c e a]]]]]
U Spec, 6
68 Set(x) & Set(px)
& ALL(a):[a e px <=> Set(a) & ALL(b):[b e a => b e x]]
=> EXIST(f1):[ALL(a):[a e px => f1(a) e px]
& ALL(a):[a e px => ALL(c):[c e x => [c e f1(a) <=> ~c e a]]]]
U Spec, 67
69 Set(x) & Set(px)
Join, 12, 22
70 Set(x) & Set(px)
& ALL(c):[c e px <=> Set(c) & ALL(d):[d e c => d e x]]
Join, 69, 23
71 EXIST(f1):[ALL(a):[a e px => f1(a) e px]
& ALL(a):[a e px => ALL(c):[c e x => [c e f1(a) <=> ~c e a]]]]
Detach, 68, 70
72 ALL(a):[a e px => cx(a) e px]
& ALL(a):[a e px => ALL(c):[c e x => [c e cx(a) <=> ~c e a]]]
E Spec, 71
Define: cx (function mapping subsets of x to their complements wrt x)
**********
73 ALL(a):[a e px => cx(a) e px]
Split, 72
74 ALL(a):[a e px => ALL(c):[c e x => [c e cx(a) <=> ~c e a]]]
Split, 72
Apply Complement Function Lemma
75 ALL(ps1):[Set(y) & Set(ps1)
& ALL(a):[a e ps1 <=> Set(a) & ALL(b):[b e a => b e y]]
=> EXIST(f1):[ALL(a):[a e ps1 => f1(a) e ps1]
& ALL(a):[a e ps1 => ALL(c):[c e y => [c e f1(a) <=> ~c e a]]]]]
U Spec, 6
76 Set(y) & Set(py)
& ALL(a):[a e py <=> Set(a) & ALL(b):[b e a => b e y]]
=> EXIST(f1):[ALL(a):[a e py => f1(a) e py]
& ALL(a):[a e py => ALL(c):[c e y => [c e f1(a) <=> ~c e a]]]]
U Spec, 75
77 Set(y) & Set(py)
Join, 13, 27
78 Set(y) & Set(py)
& ALL(c):[c e py <=> Set(c) & ALL(d):[d e c => d e y]]
Join, 77, 28
79 EXIST(f1):[ALL(a):[a e py => f1(a) e py]
& ALL(a):[a e py => ALL(c):[c e y => [c e f1(a) <=> ~c e a]]]]
Detach, 76, 78
80 ALL(a):[a e py => cy(a) e py]
& ALL(a):[a e py => ALL(c):[c e y => [c e cy(a) <=> ~c e a]]]
E Spec, 79
Define: cy (function mapping subsets of y to their complements wrt y
**********
81 ALL(a):[a e py => cy(a) e py]
Split, 80
82 ALL(a):[a e py => ALL(c):[c e y => [c e cy(a) <=> ~c e a]]]
Split, 80
Apply Subset axiom
83 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e px2 & b=cx(imgG(cy(imgF(a))))]]
Subset, 35
84 Set'(h) & ALL(a):ALL(b):[(a,b) e h <=> (a,b) e px2 & b=cx(imgG(cy(imgF(a))))]
E Spec, 83
Define: h
*********
85 Set'(h)
Split, 84
86 ALL(a):ALL(b):[(a,b) e h <=> (a,b) e px2 & b=cx(imgG(cy(imgF(a))))]
Split, 84
Apply Function axiom
87 ALL(f):ALL(a):ALL(b):[ALL(c):ALL(d):[(c,d) e f => c e a & d e b]
& ALL(c):[c e a => EXIST(d):[d e b & (c,d) e f]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e f & (c,d2) e f => d1=d2]
=> ALL(c):ALL(d):[d=f(c) <=> (c,d) e f]]
Function
88 ALL(a):ALL(b):[ALL(c):ALL(d):[(c,d) e h => c e a & d e b]
& ALL(c):[c e a => EXIST(d):[d e b & (c,d) e h]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e h & (c,d2) e h => d1=d2]
=> ALL(c):ALL(d):[d=h(c) <=> (c,d) e h]]
U Spec, 87
89 ALL(b):[ALL(c):ALL(d):[(c,d) e h => c e px & d e b]
& ALL(c):[c e px => EXIST(d):[d e b & (c,d) e h]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e h & (c,d2) e h => d1=d2]
=> ALL(c):ALL(d):[d=h(c) <=> (c,d) e h]]
U Spec, 88
Sufficient: For functionality of h
90 ALL(c):ALL(d):[(c,d) e h => c e px & d e px]
& ALL(c):[c e px => EXIST(d):[d e px & (c,d) e h]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e h & (c,d2) e h => d1=d2]
=> ALL(c):ALL(d):[d=h(c) <=> (c,d) e h]
U Spec, 89
Prove: ALL(c):ALL(d):[(c,d) e h => c e px & d e px]
Suppose...
91 (p,q) e h
Premise
Apply definition of h
92 ALL(b):[(p,b) e h <=> (p,b) e px2 & b=cx(imgG(cy(imgF(p))))]
U Spec, 86
93 (p,q) e h <=> (p,q) e px2 & q=cx(imgG(cy(imgF(p))))
U Spec, 92
94 [(p,q) e h => (p,q) e px2 & q=cx(imgG(cy(imgF(p))))]
& [(p,q) e px2 & q=cx(imgG(cy(imgF(p)))) => (p,q) e h]
Iff-And, 93
95 (p,q) e h => (p,q) e px2 & q=cx(imgG(cy(imgF(p))))
Split, 94
96 (p,q) e px2 & q=cx(imgG(cy(imgF(p)))) => (p,q) e h
Split, 94
97 (p,q) e px2 & q=cx(imgG(cy(imgF(p))))
Detach, 95, 91
98 (p,q) e px2
Split, 97
99 q=cx(imgG(cy(imgF(p))))
Split, 97
Apply definition of px2
100 ALL(c2):[(p,c2) e px2 <=> p e px & c2 e px]
U Spec, 36
101 (p,q) e px2 <=> p e px & q e px
U Spec, 100
102 [(p,q) e px2 => p e px & q e px]
& [p e px & q e px => (p,q) e px2]
Iff-And, 101
103 (p,q) e px2 => p e px & q e px
Split, 102
104 p e px & q e px => (p,q) e px2
Split, 102
105 p e px & q e px
Detach, 103, 98
As Required:
106 ALL(c):ALL(d):[(c,d) e h => c e px & d e px]
4 Conclusion, 91
Prove: ALL(c):[c e px => EXIST(d):[d e px & (c,d) e h]]
Suppose...
107 p e px
Premise
Apply definition of h
108 ALL(b):[(p,b) e h <=> (p,b) e px2 & b=cx(imgG(cy(imgF(p))))]
U Spec, 86
109 (p,cx(imgG(cy(imgF(p))))) e h <=> (p,cx(imgG(cy(imgF(p))))) e px2 & cx(imgG(cy(imgF(p))))=cx(imgG(cy(imgF(p))))
U Spec, 108
110 [(p,cx(imgG(cy(imgF(p))))) e h => (p,cx(imgG(cy(imgF(p))))) e px2 & cx(imgG(cy(imgF(p))))=cx(imgG(cy(imgF(p))))]
& [(p,cx(imgG(cy(imgF(p))))) e px2 & cx(imgG(cy(imgF(p))))=cx(imgG(cy(imgF(p)))) => (p,cx(imgG(cy(imgF(p))))) e h]
Iff-And, 109
111 (p,cx(imgG(cy(imgF(p))))) e h => (p,cx(imgG(cy(imgF(p))))) e px2 & cx(imgG(cy(imgF(p))))=cx(imgG(cy(imgF(p))))
Split, 110
112 (p,cx(imgG(cy(imgF(p))))) e px2 & cx(imgG(cy(imgF(p))))=cx(imgG(cy(imgF(p)))) => (p,cx(imgG(cy(imgF(p))))) e h
Split, 110
Apply definition of px2
113 ALL(c2):[(p,c2) e px2 <=> p e px & c2 e px]
U Spec, 36
114 (p,cx(imgG(cy(imgF(p))))) e px2 <=> p e px & cx(imgG(cy(imgF(p)))) e px
U Spec, 113
115 [(p,cx(imgG(cy(imgF(p))))) e px2 => p e px & cx(imgG(cy(imgF(p)))) e px]
& [p e px & cx(imgG(cy(imgF(p)))) e px => (p,cx(imgG(cy(imgF(p))))) e px2]
Iff-And, 114
116 (p,cx(imgG(cy(imgF(p))))) e px2 => p e px & cx(imgG(cy(imgF(p)))) e px
Split, 115
117 p e px & cx(imgG(cy(imgF(p)))) e px => (p,cx(imgG(cy(imgF(p))))) e px2
Split, 115
Apply definition of imgF function
118 p e px => imgF(p) e py
U Spec, 50
119 imgF(p) e py
Detach, 118, 107
120 imgF(p) e py => cy(imgF(p)) e py
U Spec, 81
121 cy(imgF(p)) e py
Detach, 120, 119
Apply definition of cy function
122 cy(imgF(p)) e py => imgG(cy(imgF(p))) e px
U Spec, 65
123 imgG(cy(imgF(p))) e px
Detach, 122, 121
Apply definition of imgG function
124 imgG(cy(imgF(p))) e px => cx(imgG(cy(imgF(p)))) e px
U Spec, 73
125 cx(imgG(cy(imgF(p)))) e px
Detach, 124, 123
126 p e px & cx(imgG(cy(imgF(p)))) e px
Join, 107, 125
127 (p,cx(imgG(cy(imgF(p))))) e px2
Detach, 117, 126
128 cx(imgG(cy(imgF(p))))=cx(imgG(cy(imgF(p))))
Reflex
129 (p,cx(imgG(cy(imgF(p))))) e px2
& cx(imgG(cy(imgF(p))))=cx(imgG(cy(imgF(p))))
Join, 127, 128
130 (p,cx(imgG(cy(imgF(p))))) e h
Detach, 112, 129
131 cx(imgG(cy(imgF(p)))) e px
& (p,cx(imgG(cy(imgF(p))))) e h
Join, 125, 130
132 EXIST(d):[d e px
& (p,d) e h]
E Gen, 131
As Required:
133 ALL(c):[c e px => EXIST(d):[d e px
& (c,d) e h]]
4 Conclusion, 107
Prove: ALL(c):ALL(d1):ALL(d2):[(c,d1) e h & (c,d2) e h => d1=d2]
Suppose...
134 (p,q1) e h & (p,q2) e h
Premise
135 (p,q1) e h
Split, 134
136 (p,q2) e h
Split, 134
Apply definition of h
137 ALL(b):[(p,b) e h <=> (p,b) e px2 & b=cx(imgG(cy(imgF(p))))]
U Spec, 86
138 (p,q1) e h <=> (p,q1) e px2 & q1=cx(imgG(cy(imgF(p))))
U Spec, 137
139 [(p,q1) e h => (p,q1) e px2 & q1=cx(imgG(cy(imgF(p))))]
& [(p,q1) e px2 & q1=cx(imgG(cy(imgF(p)))) => (p,q1) e h]
Iff-And, 138
140 (p,q1) e h => (p,q1) e px2 & q1=cx(imgG(cy(imgF(p))))
Split, 139
141 (p,q1) e px2 & q1=cx(imgG(cy(imgF(p)))) => (p,q1) e h
Split, 139
142 (p,q1) e px2 & q1=cx(imgG(cy(imgF(p))))
Detach, 140, 135
143 (p,q1) e px2
Split, 142
144 q1=cx(imgG(cy(imgF(p))))
Split, 142
145 (p,q2) e h <=> (p,q2) e px2 & q2=cx(imgG(cy(imgF(p))))
U Spec, 137
146 [(p,q2) e h => (p,q2) e px2 & q2=cx(imgG(cy(imgF(p))))]
& [(p,q2) e px2 & q2=cx(imgG(cy(imgF(p)))) => (p,q2) e h]
Iff-And, 145
147 (p,q2) e h => (p,q2) e px2 & q2=cx(imgG(cy(imgF(p))))
Split, 146
148 (p,q2) e px2 & q2=cx(imgG(cy(imgF(p)))) => (p,q2) e h
Split, 146
149 (p,q2) e px2 & q2=cx(imgG(cy(imgF(p))))
Detach, 147, 136
150 (p,q2) e px2
Split, 149
151 q2=cx(imgG(cy(imgF(p))))
Split, 149
152 q1=q2
Substitute, 151, 144
As Required:
153 ALL(c):ALL(d1):ALL(d2):[(c,d1) e h & (c,d2) e h => d1=d2]
4 Conclusion, 134
154 ALL(c):ALL(d):[(c,d) e h => c e px & d e px]
& ALL(c):[c e px => EXIST(d):[d e px
& (c,d) e h]]
Join, 106, 133
155 ALL(c):ALL(d):[(c,d) e h => c e px & d e px]
& ALL(c):[c e px => EXIST(d):[d e px
& (c,d) e h]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e h & (c,d2) e h => d1=d2]
Join, 154, 153
h is a function
156 ALL(c):ALL(d):[d=h(c) <=> (c,d) e h]
Detach, 90, 155
Prove: ALL(a):[a e px => h(a) e px]
Suppose...
157 p e px
Premise
Apply previous result
158 p e px => EXIST(d):[d e px
& (p,d) e h]
U Spec, 133
159 EXIST(d):[d e px
& (p,d) e h]
Detach, 158, 157
160 q e px
& (p,q) e h
E Spec, 159
161 q e px
Split, 160
162 (p,q) e h
Split, 160
Apply previous result
163 ALL(d):[d=h(p) <=> (p,d) e h]
U Spec, 156
164 q=h(p) <=> (p,q) e h
U Spec, 163
165 [q=h(p) => (p,q) e h] & [(p,q) e h => q=h(p)]
Iff-And, 164
166 q=h(p) => (p,q) e h
Split, 165
167 (p,q) e h => q=h(p)
Split, 165
168 q=h(p)
Detach, 167, 162
169 h(p) e px
Substitute, 168, 161
As Required:
170 ALL(a):[a e px => h(a) e px]
4 Conclusion, 157
Prove: ALL(a):[a e px => h(a)=cx(imgG(cy(imgF(a))))]
Suppose...
171 p e px
Premise
Apply previous result
172 p e px => EXIST(d):[d e px
& (p,d) e h]
U Spec, 133
173 EXIST(d):[d e px
& (p,d) e h]
Detach, 172, 171
174 q e px
& (p,q) e h
E Spec, 173
175 q e px
Split, 174
176 (p,q) e h
Split, 174
Apply definition of h
177 ALL(b):[(p,b) e h <=> (p,b) e px2 & b=cx(imgG(cy(imgF(p))))]
U Spec, 86
178 (p,q) e h <=> (p,q) e px2 & q=cx(imgG(cy(imgF(p))))
U Spec, 177
179 [(p,q) e h => (p,q) e px2 & q=cx(imgG(cy(imgF(p))))]
& [(p,q) e px2 & q=cx(imgG(cy(imgF(p)))) => (p,q) e h]
Iff-And, 178
180 (p,q) e h => (p,q) e px2 & q=cx(imgG(cy(imgF(p))))
Split, 179
181 (p,q) e px2 & q=cx(imgG(cy(imgF(p)))) => (p,q) e h
Split, 179
182 (p,q) e px2 & q=cx(imgG(cy(imgF(p))))
Detach, 180, 176
183 (p,q) e px2
Split, 182
184 q=cx(imgG(cy(imgF(p))))
Split, 182
185 ALL(d):[d=h(p) <=> (p,d) e h]
U Spec, 156
Apply previous result
186 q=h(p) <=> (p,q) e h
U Spec, 185
187 [q=h(p) => (p,q) e h] & [(p,q) e h => q=h(p)]
Iff-And, 186
188 q=h(p) => (p,q) e h
Split, 187
189 (p,q) e h => q=h(p)
Split, 187
190 q=h(p)
Detach, 189, 176
191 h(p)=cx(imgG(cy(imgF(p))))
Substitute, 190, 184
As Required:
192 ALL(a):[a e px => h(a)=cx(imgG(cy(imgF(a))))]
4 Conclusion, 171
Apply the Knaster-Tarski Fixed-Point Lemma
193 ALL(ps):ALL(f):[Set(x)
& Set(ps)
& ALL(a):[a e ps <=> Set(a) & Subset(a,x)]
& ALL(a):[a e ps => f(a) e ps]
& ALL(a):ALL(b):[a e ps & b e ps
=> [Subset(a,b) => Subset(f(a),f(b))]]
=> EXIST(a):[Set(a) & Subset(a,x) & f(a)=a]]
U Spec, 5
194 ALL(f):[Set(x)
& Set(px)
& ALL(a):[a e px <=> Set(a) & Subset(a,x)]
& ALL(a):[a e px => f(a) e px]
& ALL(a):ALL(b):[a e px & b e px
=> [Subset(a,b) => Subset(f(a),f(b))]]
=> EXIST(a):[Set(a) & Subset(a,x) & f(a)=a]]
U Spec, 193
Sufficient: For EXIST(a):[Set(a) & Subset(a,x) & h(a)=a]
195 Set(x)
& Set(px)
& ALL(a):[a e px <=> Set(a) & Subset(a,x)]
& ALL(a):[a e px => h(a) e px]
& ALL(a):ALL(b):[a e px & b e px
=> [Subset(a,b) => Subset(h(a),h(b))]]
=> EXIST(a):[Set(a) & Subset(a,x) & h(a)=a]
U Spec, 194
Prove that if p and q are subsets of x, and Subset(p,q) then Subset(h(p),h(q)).
Suppose...
196 p e px & q e px
Premise
197 p e px
Split, 196
198 q e px
Split, 196
Suppose...
199 Subset(p,q)
Premise
200 ALL(b):[Subset(p,b) <=> ALL(c):[c e p => c e b]]
U Spec, 1
201 Subset(p,q) <=> ALL(c):[c e p => c e q]
U Spec, 200
202 [Subset(p,q) => ALL(c):[c e p => c e q]]
& [ALL(c):[c e p => c e q] => Subset(p,q)]
Iff-And, 201
203 Subset(p,q) => ALL(c):[c e p => c e q]
Split, 202
204 ALL(c):[c e p => c e q] => Subset(p,q)
Split, 202
205 ALL(c):[c e p => c e q]
Detach, 203, 199
206 p e px
=> ALL(c):[c e imgF(p) <=> EXIST(d):[d e p & f(d)=c]]
U Spec, 51
207 ALL(c):[c e imgF(p) <=> EXIST(d):[d e p & f(d)=c]]
Detach, 206, 197
208 q e px
=> ALL(c):[c e imgF(q) <=> EXIST(d):[d e q & f(d)=c]]
U Spec, 51
209 ALL(c):[c e imgF(q) <=> EXIST(d):[d e q & f(d)=c]]
Detach, 208, 198
Suppose...
210 r e imgF(p)
Premise
211 r e imgF(p) <=> EXIST(d):[d e p & f(d)=r]
U Spec, 207
212 [r e imgF(p) => EXIST(d):[d e p & f(d)=r]]
& [EXIST(d):[d e p & f(d)=r] => r e imgF(p)]
Iff-And, 211
213 r e imgF(p) => EXIST(d):[d e p & f(d)=r]
Split, 212
214 EXIST(d):[d e p & f(d)=r] => r e imgF(p)
Split, 212
215 EXIST(d):[d e p & f(d)=r]
Detach, 213, 210
216 s e p & f(s)=r
E Spec, 215
217 s e p
Split, 216
218 f(s)=r
Split, 216
219 r e imgF(q) <=> EXIST(d):[d e q & f(d)=r]
U Spec, 209
220 [r e imgF(q) => EXIST(d):[d e q & f(d)=r]]
& [EXIST(d):[d e q & f(d)=r] => r e imgF(q)]
Iff-And, 219
221 r e imgF(q) => EXIST(d):[d e q & f(d)=r]
Split, 220
222 EXIST(d):[d e q & f(d)=r] => r e imgF(q)
Split, 220
223 s e p => s e q
U Spec, 205
224 s e q
Detach, 223, 217
225 s e q & f(s)=r
Join, 224, 218
226 EXIST(d):[d e q & f(d)=r]
E Gen, 225
227 r e imgF(q)
Detach, 222, 226
As Required:
228 ALL(c):[c e imgF(p) => c e imgF(q)]
4 Conclusion, 210
Suppose...
229 r e cy(imgF(q))
Premise
230 imgF(q) e py => ALL(c):[c e y => [c e cy(imgF(q)) <=> ~c e imgF(q)]]
U Spec, 82
231 imgF(p) e py => ALL(c):[c e y => [c e cy(imgF(p)) <=> ~c e imgF(p)]]
U Spec, 82
232 q e px => imgF(q) e py
U Spec, 50
233 imgF(q) e py
Detach, 232, 198
234 ALL(c):[c e y => [c e cy(imgF(q)) <=> ~c e imgF(q)]]
Detach, 230, 233
235 r e y => [r e cy(imgF(q)) <=> ~r e imgF(q)]
U Spec, 234
236 imgF(q) e py => cy(imgF(q)) e py
U Spec, 81
237 cy(imgF(q)) e py
Detach, 236, 233
238 cy(imgF(q)) e py <=> Set(cy(imgF(q))) & ALL(d):[d e cy(imgF(q)) => d e y]
U Spec, 28
239 [cy(imgF(q)) e py => Set(cy(imgF(q))) & ALL(d):[d e cy(imgF(q)) => d e y]]
& [Set(cy(imgF(q))) & ALL(d):[d e cy(imgF(q)) => d e y] => cy(imgF(q)) e py]
Iff-And, 238
240 cy(imgF(q)) e py => Set(cy(imgF(q))) & ALL(d):[d e cy(imgF(q)) => d e y]
Split, 239
241 Set(cy(imgF(q))) & ALL(d):[d e cy(imgF(q)) => d e y] => cy(imgF(q)) e py
Split, 239
242 Set(cy(imgF(q))) & ALL(d):[d e cy(imgF(q)) => d e y]
Detach, 240, 237
243 Set(cy(imgF(q)))
Split, 242
244 ALL(d):[d e cy(imgF(q)) => d e y]
Split, 242
245 r e cy(imgF(q)) => r e y
U Spec, 244
246 r e y
Detach, 245, 229
247 r e cy(imgF(q)) <=> ~r e imgF(q)
Detach, 235, 246
248 [r e cy(imgF(q)) => ~r e imgF(q)]
& [~r e imgF(q) => r e cy(imgF(q))]
Iff-And, 247
249 r e cy(imgF(q)) => ~r e imgF(q)
Split, 248
250 ~r e imgF(q) => r e cy(imgF(q))
Split, 248
*****************
251 ~r e imgF(q)
Detach, 249, 229
252 p e px => imgF(p) e py
U Spec, 50
253 imgF(p) e py
Detach, 252, 197
254 ALL(c):[c e y => [c e cy(imgF(p)) <=> ~c e imgF(p)]]
Detach, 231, 253
255 r e y => [r e cy(imgF(p)) <=> ~r e imgF(p)]
U Spec, 254
256 r e cy(imgF(p)) <=> ~r e imgF(p)
Detach, 255, 246
257 [r e cy(imgF(p)) => ~r e imgF(p)]
& [~r e imgF(p) => r e cy(imgF(p))]
Iff-And, 256
258 r e cy(imgF(p)) => ~r e imgF(p)
Split, 257
Sufficient:
259 ~r e imgF(p) => r e cy(imgF(p))
Split, 257
260 r e imgF(p) => r e imgF(q)
U Spec, 228
261 ~r e imgF(q) => ~r e imgF(p)
Contra, 260
262 ~r e imgF(p)
Detach, 261, 251
263 r e cy(imgF(p))
Detach, 259, 262
As Required:
264 ALL(a):[a e cy(imgF(q)) => a e cy(imgF(p))]
4 Conclusion, 229
Suppose...
265 r e imgG(cy(imgF(q)))
Premise
266 cy(imgF(q)) e py
=> ALL(c):[c e imgG(cy(imgF(q))) <=> EXIST(d):[d e cy(imgF(q)) & g(d)=c]]
U Spec, 66
267 q e px => imgF(q) e py
U Spec, 50
268 imgF(q) e py
Detach, 267, 198
269 imgF(q) e py => cy(imgF(q)) e py
U Spec, 81
270 cy(imgF(q)) e py
Detach, 269, 268
271 ALL(c):[c e imgG(cy(imgF(q))) <=> EXIST(d):[d e cy(imgF(q)) & g(d)=c]]
Detach, 266, 270
272 r e imgG(cy(imgF(q))) <=> EXIST(d):[d e cy(imgF(q)) & g(d)=r]
U Spec, 271
273 [r e imgG(cy(imgF(q))) => EXIST(d):[d e cy(imgF(q)) & g(d)=r]]
& [EXIST(d):[d e cy(imgF(q)) & g(d)=r] => r e imgG(cy(imgF(q)))]
Iff-And, 272
274 r e imgG(cy(imgF(q))) => EXIST(d):[d e cy(imgF(q)) & g(d)=r]
Split, 273
275 EXIST(d):[d e cy(imgF(q)) & g(d)=r] => r e imgG(cy(imgF(q)))
Split, 273
276 EXIST(d):[d e cy(imgF(q)) & g(d)=r]
Detach, 274, 265
277 s e cy(imgF(q)) & g(s)=r
E Spec, 276
278 s e cy(imgF(q))
Split, 277
279 g(s)=r
Split, 277
280 cy(imgF(p)) e py
=> ALL(c):[c e imgG(cy(imgF(p))) <=> EXIST(d):[d e cy(imgF(p)) & g(d)=c]]
U Spec, 66
281 p e px => imgF(p) e py
U Spec, 50
282 imgF(p) e py
Detach, 281, 197
283 imgF(p) e py => cy(imgF(p)) e py
U Spec, 81
284 cy(imgF(p)) e py
Detach, 283, 282
285 ALL(c):[c e imgG(cy(imgF(p))) <=> EXIST(d):[d e cy(imgF(p)) & g(d)=c]]
Detach, 280, 284
286 r e imgG(cy(imgF(p))) <=> EXIST(d):[d e cy(imgF(p)) & g(d)=r]
U Spec, 285
287 [r e imgG(cy(imgF(p))) => EXIST(d):[d e cy(imgF(p)) & g(d)=r]]
& [EXIST(d):[d e cy(imgF(p)) & g(d)=r] => r e imgG(cy(imgF(p)))]
Iff-And, 286
288 r e imgG(cy(imgF(p))) => EXIST(d):[d e cy(imgF(p)) & g(d)=r]
Split, 287
289 EXIST(d):[d e cy(imgF(p)) & g(d)=r] => r e imgG(cy(imgF(p)))
Split, 287
290 s e cy(imgF(q)) => s e cy(imgF(p))
U Spec, 264
291 s e cy(imgF(p))
Detach, 290, 278
292 s e cy(imgF(p)) & g(s)=r
Join, 291, 279
293 EXIST(d):[d e cy(imgF(p)) & g(d)=r]
E Gen, 292
294 r e imgG(cy(imgF(p)))
Detach, 289, 293
As Required:
295 ALL(a):[a e imgG(cy(imgF(q))) => a e imgG(cy(imgF(p)))]
4 Conclusion, 265
Suppose...
296 r e cx(imgG(cy(imgF(p))))
Premise
297 imgG(cy(imgF(p))) e px => ALL(c):[c e x => [c e cx(imgG(cy(imgF(p)))) <=> ~c e imgG(cy(imgF(p)))]]
U Spec, 74
298 imgG(cy(imgF(q))) e px => ALL(c):[c e x => [c e cx(imgG(cy(imgF(q)))) <=> ~c e imgG(cy(imgF(q)))]]
U Spec, 74
299 p e px => imgF(p) e py
U Spec, 50
300 imgF(p) e py
Detach, 299, 197
301 imgF(p) e py => cy(imgF(p)) e py
U Spec, 81
302 cy(imgF(p)) e py
Detach, 301, 300
303 cy(imgF(p)) e py => imgG(cy(imgF(p))) e px
U Spec, 65
304 imgG(cy(imgF(p))) e px
Detach, 303, 302
305 imgG(cy(imgF(p))) e px => cx(imgG(cy(imgF(p)))) e px
U Spec, 73
306 cx(imgG(cy(imgF(p)))) e px
Detach, 305, 304
307 ALL(c):[c e x => [c e cx(imgG(cy(imgF(p)))) <=> ~c e imgG(cy(imgF(p)))]]
Detach, 297, 304
308 r e x => [r e cx(imgG(cy(imgF(p)))) <=> ~r e imgG(cy(imgF(p)))]
U Spec, 307
309 cx(imgG(cy(imgF(p)))) e px <=> Set(cx(imgG(cy(imgF(p))))) & ALL(d):[d e cx(imgG(cy(imgF(p)))) => d e x]
U Spec, 23
310 [cx(imgG(cy(imgF(p)))) e px => Set(cx(imgG(cy(imgF(p))))) & ALL(d):[d e cx(imgG(cy(imgF(p)))) => d e x]]
& [Set(cx(imgG(cy(imgF(p))))) & ALL(d):[d e cx(imgG(cy(imgF(p)))) => d e x] => cx(imgG(cy(imgF(p)))) e px]
Iff-And, 309
311 cx(imgG(cy(imgF(p)))) e px => Set(cx(imgG(cy(imgF(p))))) & ALL(d):[d e cx(imgG(cy(imgF(p)))) => d e x]
Split, 310
312 Set(cx(imgG(cy(imgF(p))))) & ALL(d):[d e cx(imgG(cy(imgF(p)))) => d e x] => cx(imgG(cy(imgF(p)))) e px
Split, 310
313 Set(cx(imgG(cy(imgF(p))))) & ALL(d):[d e cx(imgG(cy(imgF(p)))) => d e x]
Detach, 311, 306
314 Set(cx(imgG(cy(imgF(p)))))
Split, 313
315 ALL(d):[d e cx(imgG(cy(imgF(p)))) => d e x]
Split, 313
316 r e cx(imgG(cy(imgF(p)))) => r e x
U Spec, 315
317 r e x
Detach, 316, 296
318 r e cx(imgG(cy(imgF(p)))) <=> ~r e imgG(cy(imgF(p)))
Detach, 308, 317
319 [r e cx(imgG(cy(imgF(p)))) => ~r e imgG(cy(imgF(p)))]
& [~r e imgG(cy(imgF(p))) => r e cx(imgG(cy(imgF(p))))]
Iff-And, 318
320 r e cx(imgG(cy(imgF(p)))) => ~r e imgG(cy(imgF(p)))
Split, 319
321 ~r e imgG(cy(imgF(p))) => r e cx(imgG(cy(imgF(p))))
Split, 319
322 ~r e imgG(cy(imgF(p)))
Detach, 320, 296
323 q e px => imgF(q) e py
U Spec, 50
324 imgF(q) e py
Detach, 323, 198
325 imgF(q) e py => cy(imgF(q)) e py
U Spec, 81
326 cy(imgF(q)) e py
Detach, 325, 324
327 cy(imgF(q)) e py => imgG(cy(imgF(q))) e px
U Spec, 65
328 imgG(cy(imgF(q))) e px
Detach, 327, 326
329 imgG(cy(imgF(q))) e px => cx(imgG(cy(imgF(q)))) e px
U Spec, 73
330 cx(imgG(cy(imgF(q)))) e px
Detach, 329, 328
331 ALL(c):[c e x => [c e cx(imgG(cy(imgF(q)))) <=> ~c e imgG(cy(imgF(q)))]]
Detach, 298, 328
332 r e x => [r e cx(imgG(cy(imgF(q)))) <=> ~r e imgG(cy(imgF(q)))]
U Spec, 331
333 r e cx(imgG(cy(imgF(q)))) <=> ~r e imgG(cy(imgF(q)))
Detach, 332, 317
334 [r e cx(imgG(cy(imgF(q)))) => ~r e imgG(cy(imgF(q)))]
& [~r e imgG(cy(imgF(q))) => r e cx(imgG(cy(imgF(q))))]
Iff-And, 333
335 r e cx(imgG(cy(imgF(q)))) => ~r e imgG(cy(imgF(q)))
Split, 334
336 ~r e imgG(cy(imgF(q))) => r e cx(imgG(cy(imgF(q))))
Split, 334
337 r e imgG(cy(imgF(q))) => r e imgG(cy(imgF(p)))
U Spec, 295
338 ~r e imgG(cy(imgF(p))) => ~r e imgG(cy(imgF(q)))
Contra, 337
339 ~r e imgG(cy(imgF(q)))
Detach, 338, 322
340 r e cx(imgG(cy(imgF(q))))
Detach, 336, 339
As Required:
341 ALL(a):[a e cx(imgG(cy(imgF(p))))
=> a e cx(imgG(cy(imgF(q))))]
4 Conclusion, 296
342 p e px => h(p)=cx(imgG(cy(imgF(p))))
U Spec, 192
343 h(p)=cx(imgG(cy(imgF(p))))
Detach, 342, 197
344 q e px => h(q)=cx(imgG(cy(imgF(q))))
U Spec, 192
345 h(q)=cx(imgG(cy(imgF(q))))
Detach, 344, 198
346 ALL(a):[a e h(p)
=> a e cx(imgG(cy(imgF(q))))]
Substitute, 343, 341
347 ALL(a):[a e h(p)
=> a e h(q)]
Substitute, 345, 346
348 ALL(b):[Subset(h(p),b) <=> ALL(c):[c e h(p) => c e b]]
U Spec, 1
349 Subset(h(p),h(q)) <=> ALL(c):[c e h(p) => c e h(q)]
U Spec, 348
350 [Subset(h(p),h(q)) => ALL(c):[c e h(p) => c e h(q)]]
& [ALL(c):[c e h(p) => c e h(q)] => Subset(h(p),h(q))]
Iff-And, 349
351 Subset(h(p),h(q)) => ALL(c):[c e h(p) => c e h(q)]
Split, 350
352 ALL(c):[c e h(p) => c e h(q)] => Subset(h(p),h(q))
Split, 350
353 Subset(h(p),h(q))
Detach, 352, 347
354 Subset(p,q) => Subset(h(p),h(q))
4 Conclusion, 199
As Required:
355 ALL(a):ALL(b):[a e px & b e px => [Subset(a,b) => Subset(h(a),h(b))]]
4 Conclusion, 196
Prove: ALL(a):[a e px => Set(a) & Subset(a,x)]
Suppose...
356 p e px
Premise
357 p e px <=> Set(p) & ALL(d):[d e p => d e x]
U Spec, 23
358 [p e px => Set(p) & ALL(d):[d e p => d e x]]
& [Set(p) & ALL(d):[d e p => d e x] => p e px]
Iff-And, 357
359 p e px => Set(p) & ALL(d):[d e p => d e x]
Split, 358
360 Set(p) & ALL(d):[d e p => d e x] => p e px
Split, 358
361 Set(p) & ALL(d):[d e p => d e x]
Detach, 359, 356
362 Set(p)
Split, 361
363 ALL(d):[d e p => d e x]
Split, 361
364 ALL(b):[Subset(p,b) <=> ALL(c):[c e p => c e b]]
U Spec, 1
365 Subset(p,x) <=> ALL(c):[c e p => c e x]
U Spec, 364
366 [Subset(p,x) => ALL(c):[c e p => c e x]]
& [ALL(c):[c e p => c e x] => Subset(p,x)]
Iff-And, 365
367 Subset(p,x) => ALL(c):[c e p => c e x]
Split, 366
368 ALL(c):[c e p => c e x] => Subset(p,x)
Split, 366
369 Subset(p,x)
Detach, 368, 363
370 Set(p) & Subset(p,x)
Join, 362, 369
As Required:
371 ALL(a):[a e px => Set(a) & Subset(a,x)]
4 Conclusion, 356
372 Set(x) & Set(px)
Join, 12, 22
373 Set(x) & Set(px)
& ALL(a):[a e px => Set(a) & Subset(a,x)]
Join, 372, 371
374 Set(x) & Set(px)
& ALL(a):[a e px => Set(a) & Subset(a,x)]
& ALL(a):[a e px => h(a) e px]
Join, 373, 170
Prove: ALL(a):[Set(a) & Subset(a,x) => a e px]
Suppose...
375 Set(p) & Subset(p,x)
Premise
376 Set(p)
Split, 375
377 Subset(p,x)
Split, 375
378 ALL(b):[Subset(p,b) <=> ALL(c):[c e p => c e b]]
U Spec, 1
379 Subset(p,x) <=> ALL(c):[c e p => c e x]
U Spec, 378
380 [Subset(p,x) => ALL(c):[c e p => c e x]]
& [ALL(c):[c e p => c e x] => Subset(p,x)]
Iff-And, 379
381 Subset(p,x) => ALL(c):[c e p => c e x]
Split, 380
382 ALL(c):[c e p => c e x] => Subset(p,x)
Split, 380
383 ALL(c):[c e p => c e x]
Detach, 381, 377
384 p e px <=> Set(p) & ALL(d):[d e p => d e x]
U Spec, 23
385 [p e px => Set(p) & ALL(d):[d e p => d e x]]
& [Set(p) & ALL(d):[d e p => d e x] => p e px]
Iff-And, 384
386 p e px => Set(p) & ALL(d):[d e p => d e x]
Split, 385
387 Set(p) & ALL(d):[d e p => d e x] => p e px
Split, 385
388 Set(p) & ALL(c):[c e p => c e x]
Join, 376, 383
389 p e px
Detach, 387, 388
As Required:
390 ALL(a):[Set(a) & Subset(a,x) => a e px]
4 Conclusion, 375
391 ALL(a):[[a e px => Set(a) & Subset(a,x)] & [Set(a) & Subset(a,x) => a e px]]
Join, 371, 390
As Required:
392 ALL(a):[a e px <=> Set(a) & Subset(a,x)]
Iff-And, 391
393 Set(x) & Set(px)
Join, 12, 22
394 Set(x) & Set(px)
& ALL(a):[a e px <=> Set(a) & Subset(a,x)]
Join, 393, 392
395 Set(x) & Set(px)
& ALL(a):[a e px <=> Set(a) & Subset(a,x)]
& ALL(a):[a e px => h(a) e px]
Join, 394, 170
396 Set(x) & Set(px)
& ALL(a):[a e px <=> Set(a) & Subset(a,x)]
& ALL(a):[a e px => h(a) e px]
& ALL(a):ALL(b):[a e px & b e px => [Subset(a,b) => Subset(h(a),h(b))]]
Join, 395, 355
397 EXIST(a):[Set(a) & Subset(a,x) & h(a)=a]
Detach, 195, 396
398 Set(z) & Subset(z,x) & h(z)=z
E Spec, 397
Define: z (the fixed point)
*********
399 Set(z)
Split, 398
400 Subset(z,x)
Split, 398
401 h(z)=z
Split, 398
402 z e px => h(z)=cx(imgG(cy(imgF(z))))
U Spec, 192
403 ALL(b):[Subset(z,b) <=> ALL(c):[c e z => c e b]]
U Spec, 1
404 Subset(z,x) <=> ALL(c):[c e z => c e x]
U Spec, 403
405 [Subset(z,x) => ALL(c):[c e z => c e x]]
& [ALL(c):[c e z => c e x] => Subset(z,x)]
Iff-And, 404
406 Subset(z,x) => ALL(c):[c e z => c e x]
Split, 405
407 ALL(c):[c e z => c e x] => Subset(z,x)
Split, 405
408 ALL(c):[c e z => c e x]
Detach, 406, 400
409 z e px <=> Set(z) & ALL(d):[d e z => d e x]
U Spec, 23
410 [z e px => Set(z) & ALL(d):[d e z => d e x]]
& [Set(z) & ALL(d):[d e z => d e x] => z e px]
Iff-And, 409
411 z e px => Set(z) & ALL(d):[d e z => d e x]
Split, 410
412 Set(z) & ALL(d):[d e z => d e x] => z e px
Split, 410
413 Set(z) & ALL(c):[c e z => c e x]
Join, 399, 408
As Required:
414 z e px
Detach, 412, 413
415 h(z)=cx(imgG(cy(imgF(z))))
Detach, 402, 414
416 z=cx(imgG(cy(imgF(z))))
Substitute, 401, 415
417 cx(z)=cx(z)
Reflex
As Required:
418 cx(cx(imgG(cy(imgF(z)))))=cx(z)
Substitute, 416, 417
419 z e px => imgF(z) e py
U Spec, 50
420 imgF(z) e py
Detach, 419, 414
421 imgF(z) e py => cy(imgF(z)) e py
U Spec, 81
422 cy(imgF(z)) e py
Detach, 421, 420
423 cy(imgF(z)) e py => imgG(cy(imgF(z))) e px
U Spec, 65
As Required:
424 imgG(cy(imgF(z))) e px
Detach, 423, 422
425 ALL(b):[Subset(imgG(cy(imgF(z))),b) <=> ALL(c):[c e imgG(cy(imgF(z))) => c e b]]
U Spec, 1
426 Subset(imgG(cy(imgF(z))),x) <=> ALL(c):[c e imgG(cy(imgF(z))) => c e x]
U Spec, 425
427 [Subset(imgG(cy(imgF(z))),x) => ALL(c):[c e imgG(cy(imgF(z))) => c e x]]
& [ALL(c):[c e imgG(cy(imgF(z))) => c e x] => Subset(imgG(cy(imgF(z))),x)]
Iff-And, 426
428 Subset(imgG(cy(imgF(z))),x) => ALL(c):[c e imgG(cy(imgF(z))) => c e x]
Split, 427
429 ALL(c):[c e imgG(cy(imgF(z))) => c e x] => Subset(imgG(cy(imgF(z))),x)
Split, 427
430 imgG(cy(imgF(z))) e px <=> Set(imgG(cy(imgF(z)))) & ALL(d):[d e imgG(cy(imgF(z))) => d e x]
U Spec, 23
431 [imgG(cy(imgF(z))) e px => Set(imgG(cy(imgF(z)))) & ALL(d):[d e imgG(cy(imgF(z))) => d e x]]
& [Set(imgG(cy(imgF(z)))) & ALL(d):[d e imgG(cy(imgF(z))) => d e x] => imgG(cy(imgF(z))) e px]
Iff-And, 430
432 imgG(cy(imgF(z))) e px => Set(imgG(cy(imgF(z)))) & ALL(d):[d e imgG(cy(imgF(z))) => d e x]
Split, 431
433 Set(imgG(cy(imgF(z)))) & ALL(d):[d e imgG(cy(imgF(z))) => d e x] => imgG(cy(imgF(z))) e px
Split, 431
434 Set(imgG(cy(imgF(z)))) & ALL(d):[d e imgG(cy(imgF(z))) => d e x]
Detach, 432, 424
435 Set(imgG(cy(imgF(z))))
Split, 434
436 ALL(d):[d e imgG(cy(imgF(z))) => d e x]
Split, 434
As Required:
437 Subset(imgG(cy(imgF(z))),x)
Detach, 429, 436
Apply Complement of a Complement Lemma
438 ALL(ps):ALL(f):[Set(x)
& Set(ps)
& ALL(a):[a e ps <=> Set(a) & ALL(b):[b e a => b e x]]
& ALL(a):[a e ps => f(a) e ps]
& ALL(a):[a e ps => ALL(b):[b e x => [b e f(a) <=> ~b e a]]]
=> ALL(a):[a e ps => f(f(a))=a]]
U Spec, 8
439 ALL(f):[Set(x)
& Set(px)
& ALL(a):[a e px <=> Set(a) & ALL(b):[b e a => b e x]]
& ALL(a):[a e px => f(a) e px]
& ALL(a):[a e px => ALL(b):[b e x => [b e f(a) <=> ~b e a]]]
=> ALL(a):[a e px => f(f(a))=a]]
U Spec, 438
440 Set(x)
& Set(px)
& ALL(a):[a e px <=> Set(a) & ALL(b):[b e a => b e x]]
& ALL(a):[a e px => cx(a) e px]
& ALL(a):[a e px => ALL(b):[b e x => [b e cx(a) <=> ~b e a]]]
=> ALL(a):[a e px => cx(cx(a))=a]
U Spec, 439
441 Set(x) & Set(px)
Join, 12, 22
442 Set(x) & Set(px)
& ALL(c):[c e px <=> Set(c) & ALL(d):[d e c => d e x]]
Join, 441, 23
443 Set(x) & Set(px)
& ALL(c):[c e px <=> Set(c) & ALL(d):[d e c => d e x]]
& ALL(a):[a e px => cx(a) e px]
Join, 442, 73
444 Set(x) & Set(px)
& ALL(c):[c e px <=> Set(c) & ALL(d):[d e c => d e x]]
& ALL(a):[a e px => cx(a) e px]
& ALL(a):[a e px => ALL(c):[c e x => [c e cx(a) <=> ~c e a]]]
Join, 443, 74
445 ALL(a):[a e px => cx(cx(a))=a]
Detach, 440, 444
446 imgG(cy(imgF(z))) e px => cx(cx(imgG(cy(imgF(z)))))=imgG(cy(imgF(z)))
U Spec, 445
As Required:
447 cx(cx(imgG(cy(imgF(z)))))=imgG(cy(imgF(z)))
Detach, 446, 424
As Required:
448 imgG(cy(imgF(z)))=cx(z)
Substitute, 447, 418
449 z e px => imgF(z) e py
U Spec, 50
Define: imgF(z)
***************
450 imgF(z) e py
Detach, 449, 414
451 imgF(z) e py <=> Set(imgF(z)) & ALL(d):[d e imgF(z) => d e y]
U Spec, 28
452 [imgF(z) e py => Set(imgF(z)) & ALL(d):[d e imgF(z) => d e y]]
& [Set(imgF(z)) & ALL(d):[d e imgF(z) => d e y] => imgF(z) e py]
Iff-And, 451
453 imgF(z) e py => Set(imgF(z)) & ALL(d):[d e imgF(z) => d e y]
Split, 452
454 Set(imgF(z)) & ALL(d):[d e imgF(z) => d e y] => imgF(z) e py
Split, 452
455 Set(imgF(z)) & ALL(d):[d e imgF(z) => d e y]
Detach, 453, 450
456 Set(imgF(z))
Split, 455
457 ALL(d):[d e imgF(z) => d e y]
Split, 455
458 z e px
=> ALL(c):[c e imgF(z) <=> EXIST(d):[d e z & f(d)=c]]
U Spec, 51
459 ALL(c):[c e imgF(z) <=> EXIST(d):[d e z & f(d)=c]]
Detach, 458, 414
460 imgF(z) e py => cy(imgF(z)) e py
U Spec, 81
Define: cy(imgF(z))
*******************
461 cy(imgF(z)) e py
Detach, 460, 450
462 imgF(z) e py => ALL(c):[c e y => [c e cy(imgF(z)) <=> ~c e imgF(z)]]
U Spec, 82
463 ALL(c):[c e y => [c e cy(imgF(z)) <=> ~c e imgF(z)]]
Detach, 462, 450
464 z e px => cx(z) e px
U Spec, 73
Define: cx(z)
*************
465 cx(z) e px
Detach, 464, 414
466 z e px => ALL(c):[c e x => [c e cx(z) <=> ~c e z]]
U Spec, 74
467 ALL(c):[c e x => [c e cx(z) <=> ~c e z]]
Detach, 466, 414
468 cy(imgF(z)) e py => imgG(cy(imgF(z))) e px
U Spec, 65
Define: imgG(cy(imgF(z)))
*************************
469 imgG(cy(imgF(z))) e px
Detach, 468, 461
470 cy(imgF(z)) e py
=> ALL(c):[c e imgG(cy(imgF(z))) <=> EXIST(d):[d e cy(imgF(z)) & g(d)=c]]
U Spec, 66
471 ALL(c):[c e imgG(cy(imgF(z))) <=> EXIST(d):[d e cy(imgF(z)) & g(d)=c]]
Detach, 470, 461
Prove: ALL(a):[a e z => f(a) e imgF(z)]
Suppose...
472 p e z
Premise
473 f(p) e imgF(z) <=> EXIST(d):[d e z & f(d)=f(p)]
U Spec, 459
474 [f(p) e imgF(z) => EXIST(d):[d e z & f(d)=f(p)]]
& [EXIST(d):[d e z & f(d)=f(p)] => f(p) e imgF(z)]
Iff-And, 473
475 f(p) e imgF(z) => EXIST(d):[d e z & f(d)=f(p)]
Split, 474
476 EXIST(d):[d e z & f(d)=f(p)] => f(p) e imgF(z)
Split, 474
477 f(p)=f(p)
Reflex
478 p e z & f(p)=f(p)
Join, 472, 477
479 EXIST(d):[d e z & f(d)=f(p)]
E Gen, 478
480 f(p) e imgF(z)
Detach, 476, 479
Define: f f: z -> imgF(z) (a restriction on f)
*********
481 ALL(a):[a e z => f(a) e imgF(z)]
4 Conclusion, 472
482 ALL(a):ALL(b):[Injection(f,a,b) <=> ALL(c):ALL(d):[c e a & d e a => [f(c)=f(d) => c=d]]]
U Spec, 2
483 ALL(b):[Injection(f,x,b) <=> ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]]
U Spec, 482
484 Injection(f,x,y) <=> ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]
U Spec, 483
485 [Injection(f,x,y) => ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]]
& [ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]] => Injection(f,x,y)]
Iff-And, 484
486 Injection(f,x,y) => ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]
Split, 485
487 ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]] => Injection(f,x,y)
Split, 485
488 ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]
Detach, 486, 16
489 p e z & q e z
Premise
490 p e z
Split, 489
491 q e z
Split, 489
492 ALL(b):[Subset(z,b) <=> ALL(c):[c e z => c e b]]
U Spec, 1
493 Subset(z,x) <=> ALL(c):[c e z => c e x]
U Spec, 492
494 [Subset(z,x) => ALL(c):[c e z => c e x]]
& [ALL(c):[c e z => c e x] => Subset(z,x)]
Iff-And, 493
495 Subset(z,x) => ALL(c):[c e z => c e x]
Split, 494
496 ALL(c):[c e z => c e x] => Subset(z,x)
Split, 494
497 ALL(c):[c e z => c e x]
Detach, 495, 400
498 p e z => p e x
U Spec, 497
499 p e x
Detach, 498, 490
500 q e z => q e x
U Spec, 497
501 q e x
Detach, 500, 491
502 ALL(d):[p e x & d e x => [f(p)=f(d) => p=d]]
U Spec, 488
503 p e x & q e x => [f(p)=f(q) => p=q]
U Spec, 502
504 p e x & q e x
Join, 499, 501
505 f(p)=f(q) => p=q
Detach, 503, 504
f: z -> imgF(z) is injective
506 ALL(a):ALL(b):[a e z & b e z => [f(a)=f(b) => a=b]]
4 Conclusion, 489
Apply Existence of Inverse Lemma
507 ALL(y):ALL(f):[Set(z) & Set(y)
& ALL(a):[a e z => f(a) e y]
& ALL(a):[a e y => EXIST(b):[b e z & f(b)=a]]
& ALL(a):ALL(b):[a e z & b e z => [f(a)=f(b) => a=b]]
=> EXIST(f'):[ALL(a):[a e y => f'(a) e z]
& ALL(a):ALL(b):[a e z & b e y => [f'(b)=a <=> f(a)=b]]]]
U Spec, 9
508 ALL(f):[Set(z) & Set(imgF(z))
& ALL(a):[a e z => f(a) e imgF(z)]
& ALL(a):[a e imgF(z) => EXIST(b):[b e z & f(b)=a]]
& ALL(a):ALL(b):[a e z & b e z => [f(a)=f(b) => a=b]]
=> EXIST(f'):[ALL(a):[a e imgF(z) => f'(a) e z]
& ALL(a):ALL(b):[a e z & b e imgF(z) => [f'(b)=a <=> f(a)=b]]]]
U Spec, 507
509 Set(z) & Set(imgF(z))
& ALL(a):[a e z => f(a) e imgF(z)]
& ALL(a):[a e imgF(z) => EXIST(b):[b e z & f(b)=a]]
& ALL(a):ALL(b):[a e z & b e z => [f(a)=f(b) => a=b]]
=> EXIST(f'):[ALL(a):[a e imgF(z) => f'(a) e z]
& ALL(a):ALL(b):[a e z & b e imgF(z) => [f'(b)=a <=> f(a)=b]]]
U Spec, 508
510 Set(z) & Set(imgF(z))
Join, 399, 456
511 Set(z) & Set(imgF(z))
& ALL(a):[a e z => f(a) e imgF(z)]
Join, 510, 481
Prove: ALL(a):[a e cy(imgF(z)) => g(a) e imgG(cy(imgF(z))]
512 p e cy(imgF(z))
Premise
513 g(p) e imgG(cy(imgF(z))) <=> EXIST(d):[d e cy(imgF(z)) & g(d)=g(p)]
U Spec, 471
514 [g(p) e imgG(cy(imgF(z))) => EXIST(d):[d e cy(imgF(z)) & g(d)=g(p)]]
& [EXIST(d):[d e cy(imgF(z)) & g(d)=g(p)] => g(p) e imgG(cy(imgF(z)))]
Iff-And, 513
515 g(p) e imgG(cy(imgF(z))) => EXIST(d):[d e cy(imgF(z)) & g(d)=g(p)]
Split, 514
516 EXIST(d):[d e cy(imgF(z)) & g(d)=g(p)] => g(p) e imgG(cy(imgF(z)))
Split, 514
517 g(p)=g(p)
Reflex
518 p e cy(imgF(z)) & g(p)=g(p)
Join, 512, 517
519 EXIST(d):[d e cy(imgF(z)) & g(d)=g(p)]
E Gen, 518
520 g(p) e imgG(cy(imgF(z)))
Detach, 516, 519
Define: g g: cy(imgF(z)) -> imgG(cy(imgF(z))
*********
521 ALL(a):[a e cy(imgF(z)) => g(a) e imgG(cy(imgF(z)))]
4 Conclusion, 512
Prove: ALL(a):ALL(b):[a e cy(imgF(z)) & b e cy(imgF(z)) => [g(a)=g(b) => a=b]]
Suppose...
522 p e cy(imgF(z)) & q e cy(imgF(z))
Premise
523 p e cy(imgF(z))
Split, 522
524 q e cy(imgF(z))
Split, 522
525 ALL(a):ALL(b):[Injection(g,a,b) <=> ALL(c):ALL(d):[c e a & d e a => [g(c)=g(d) => c=d]]]
U Spec, 2
526 ALL(b):[Injection(g,y,b) <=> ALL(c):ALL(d):[c e y & d e y => [g(c)=g(d) => c=d]]]
U Spec, 525
527 Injection(g,y,x) <=> ALL(c):ALL(d):[c e y & d e y => [g(c)=g(d) => c=d]]
U Spec, 526
528 [Injection(g,y,x) => ALL(c):ALL(d):[c e y & d e y => [g(c)=g(d) => c=d]]]
& [ALL(c):ALL(d):[c e y & d e y => [g(c)=g(d) => c=d]] => Injection(g,y,x)]
Iff-And, 527
529 Injection(g,y,x) => ALL(c):ALL(d):[c e y & d e y => [g(c)=g(d) => c=d]]
Split, 528
530 ALL(c):ALL(d):[c e y & d e y => [g(c)=g(d) => c=d]] => Injection(g,y,x)
Split, 528
531 ALL(c):ALL(d):[c e y & d e y => [g(c)=g(d) => c=d]]
Detach, 529, 17
532 cy(imgF(z)) e py <=> Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]
U Spec, 28
533 [cy(imgF(z)) e py => Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]]
& [Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y] => cy(imgF(z)) e py]
Iff-And, 532
534 cy(imgF(z)) e py => Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]
Split, 533
535 Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y] => cy(imgF(z)) e py
Split, 533
536 Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]
Detach, 534, 461
537 Set(cy(imgF(z)))
Split, 536
538 ALL(d):[d e cy(imgF(z)) => d e y]
Split, 536
539 p e cy(imgF(z)) => p e y
U Spec, 538
540 p e y
Detach, 539, 523
541 q e cy(imgF(z)) => q e y
U Spec, 538
542 q e y
Detach, 541, 524
543 ALL(d):[p e y & d e y => [g(p)=g(d) => p=d]]
U Spec, 531
544 p e y & q e y => [g(p)=g(q) => p=q]
U Spec, 543
545 p e y & q e y
Join, 540, 542
546 g(p)=g(q) => p=q
Detach, 544, 545
Function g: cy(imgF(z)) -> imgG(cy(imgF(z)) is injective
547 ALL(a):ALL(b):[a e cy(imgF(z)) & b e cy(imgF(z)) => [g(a)=g(b) => a=b]]
4 Conclusion, 522
Prove: ALL(a):[a e imgG(cy(imgF(z)))
=> EXIST(d):[d e cy(imgF(z)) & g(d)=a]]
Suppose...
548 p e imgG(cy(imgF(z)))
Premise
549 p e imgG(cy(imgF(z))) <=> EXIST(d):[d e cy(imgF(z)) & g(d)=p]
U Spec, 471
550 [p e imgG(cy(imgF(z))) => EXIST(d):[d e cy(imgF(z)) & g(d)=p]]
& [EXIST(d):[d e cy(imgF(z)) & g(d)=p] => p e imgG(cy(imgF(z)))]
Iff-And, 549
551 p e imgG(cy(imgF(z))) => EXIST(d):[d e cy(imgF(z)) & g(d)=p]
Split, 550
552 EXIST(d):[d e cy(imgF(z)) & g(d)=p] => p e imgG(cy(imgF(z)))
Split, 550
553 EXIST(d):[d e cy(imgF(z)) & g(d)=p]
Detach, 551, 548
Function g: cy(imgF(z)) -> imgG(cy(imgF(z)) is surjective
554 ALL(a):[a e imgG(cy(imgF(z)))
=> EXIST(d):[d e cy(imgF(z)) & g(d)=a]]
4 Conclusion, 548
555 ALL(a):[a e cy(imgF(z)) => g(a) e cx(z)]
Substitute, 448, 521
556 ALL(a):[a e cx(z)
=> EXIST(d):[d e cy(imgF(z)) & g(d)=a]]
Substitute, 448, 554
557 ALL(y):ALL(f):[Set(cy(imgF(z))) & Set(y)
& ALL(a):[a e cy(imgF(z)) => f(a) e y]
& ALL(a):[a e y => EXIST(b):[b e cy(imgF(z)) & f(b)=a]]
& ALL(a):ALL(b):[a e cy(imgF(z)) & b e cy(imgF(z)) => [f(a)=f(b) => a=b]]
=> EXIST(f'):[ALL(a):[a e y => f'(a) e cy(imgF(z))]
& ALL(a):ALL(b):[a e cy(imgF(z)) & b e y => [f'(b)=a <=> f(a)=b]]]]
U Spec, 9
558 ALL(f):[Set(cy(imgF(z))) & Set(cx(z))
& ALL(a):[a e cy(imgF(z)) => f(a) e cx(z)]
& ALL(a):[a e cx(z) => EXIST(b):[b e cy(imgF(z)) & f(b)=a]]
& ALL(a):ALL(b):[a e cy(imgF(z)) & b e cy(imgF(z)) => [f(a)=f(b) => a=b]]
=> EXIST(f'):[ALL(a):[a e cx(z) => f'(a) e cy(imgF(z))]
& ALL(a):ALL(b):[a e cy(imgF(z)) & b e cx(z) => [f'(b)=a <=> f(a)=b]]]]
U Spec, 557
559 Set(cy(imgF(z))) & Set(cx(z))
& ALL(a):[a e cy(imgF(z)) => g(a) e cx(z)]
& ALL(a):[a e cx(z) => EXIST(b):[b e cy(imgF(z)) & g(b)=a]]
& ALL(a):ALL(b):[a e cy(imgF(z)) & b e cy(imgF(z)) => [g(a)=g(b) => a=b]]
=> EXIST(f'):[ALL(a):[a e cx(z) => f'(a) e cy(imgF(z))]
& ALL(a):ALL(b):[a e cy(imgF(z)) & b e cx(z) => [f'(b)=a <=> g(a)=b]]]
U Spec, 558
560 cy(imgF(z)) e py <=> Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]
U Spec, 28
561 [cy(imgF(z)) e py => Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]]
& [Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y] => cy(imgF(z)) e py]
Iff-And, 560
562 cy(imgF(z)) e py => Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]
Split, 561
563 Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y] => cy(imgF(z)) e py
Split, 561
564 Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]
Detach, 562, 461
565 Set(cy(imgF(z)))
Split, 564
566 ALL(d):[d e cy(imgF(z)) => d e y]
Split, 564
567 cx(z) e px <=> Set(cx(z)) & ALL(d):[d e cx(z) => d e x]
U Spec, 23
568 [cx(z) e px => Set(cx(z)) & ALL(d):[d e cx(z) => d e x]]
& [Set(cx(z)) & ALL(d):[d e cx(z) => d e x] => cx(z) e px]
Iff-And, 567
569 cx(z) e px => Set(cx(z)) & ALL(d):[d e cx(z) => d e x]
Split, 568
570 Set(cx(z)) & ALL(d):[d e cx(z) => d e x] => cx(z) e px
Split, 568
571 Set(cx(z)) & ALL(d):[d e cx(z) => d e x]
Detach, 569, 465
572 Set(cx(z))
Split, 571
573 ALL(d):[d e cx(z) => d e x]
Split, 571
574 Set(cy(imgF(z))) & Set(cx(z))
Join, 565, 572
575 Set(cy(imgF(z))) & Set(cx(z))
& ALL(a):[a e cy(imgF(z)) => g(a) e cx(z)]
Join, 574, 555
576 Set(cy(imgF(z))) & Set(cx(z))
& ALL(a):[a e cy(imgF(z)) => g(a) e cx(z)]
& ALL(a):[a e cx(z)
=> EXIST(d):[d e cy(imgF(z)) & g(d)=a]]
Join, 575, 556
577 Set(cy(imgF(z))) & Set(cx(z))
& ALL(a):[a e cy(imgF(z)) => g(a) e cx(z)]
& ALL(a):[a e cx(z)
=> EXIST(d):[d e cy(imgF(z)) & g(d)=a]]
& ALL(a):ALL(b):[a e cy(imgF(z)) & b e cy(imgF(z)) => [g(a)=g(b) => a=b]]
Join, 576, 547
578 EXIST(f'):[ALL(a):[a e cx(z) => f'(a) e cy(imgF(z))]
& ALL(a):ALL(b):[a e cy(imgF(z)) & b e cx(z) => [f'(b)=a <=> g(a)=b]]]
Detach, 559, 577
579 ALL(a):[a e cx(z) => g'(a) e cy(imgF(z))]
& ALL(a):ALL(b):[a e cy(imgF(z)) & b e cx(z) => [g'(b)=a <=> g(a)=b]]
E Spec, 578
Define: g' (inverse of g: cy(imgF(z)) -> cx(z)
**********
580 ALL(a):[a e cx(z) => g'(a) e cy(imgF(z))]
Split, 579
581 ALL(a):ALL(b):[a e cy(imgF(z)) & b e cx(z) => [g'(b)=a <=> g(a)=b]]
Split, 579
Apply Inverses are Bijections Lemma
582 ALL(set2):ALL(func):ALL(inv):[Set(cy(imgF(z))) & Set(set2)
& ALL(a):[a e cy(imgF(z)) => func(a) e set2]
& ALL(a):[a e set2 => inv(a) e cy(imgF(z))]
& ALL(a):ALL(b):[a e cy(imgF(z)) & b e set2 => [inv(b)=a <=> func(a)=b]]
=> ALL(a):ALL(b):[a e set2 & b e set2 => [inv(a)=inv(b) => a=b]]
& ALL(a):[a e cy(imgF(z)) => EXIST(b):[b e set2 & inv(b)=a]]]
U Spec, 10
583 ALL(func):ALL(inv):[Set(cy(imgF(z))) & Set(imgG(cy(imgF(z))))
& ALL(a):[a e cy(imgF(z)) => func(a) e imgG(cy(imgF(z)))]
& ALL(a):[a e imgG(cy(imgF(z))) => inv(a) e cy(imgF(z))]
& ALL(a):ALL(b):[a e cy(imgF(z)) & b e imgG(cy(imgF(z))) => [inv(b)=a <=> func(a)=b]]
=> ALL(a):ALL(b):[a e imgG(cy(imgF(z))) & b e imgG(cy(imgF(z))) => [inv(a)=inv(b) => a=b]]
& ALL(a):[a e cy(imgF(z)) => EXIST(b):[b e imgG(cy(imgF(z))) & inv(b)=a]]]
U Spec, 582
584 ALL(inv):[Set(cy(imgF(z))) & Set(imgG(cy(imgF(z))))
& ALL(a):[a e cy(imgF(z)) => g(a) e imgG(cy(imgF(z)))]
& ALL(a):[a e imgG(cy(imgF(z))) => inv(a) e cy(imgF(z))]
& ALL(a):ALL(b):[a e cy(imgF(z)) & b e imgG(cy(imgF(z))) => [inv(b)=a <=> g(a)=b]]
=> ALL(a):ALL(b):[a e imgG(cy(imgF(z))) & b e imgG(cy(imgF(z))) => [inv(a)=inv(b) => a=b]]
& ALL(a):[a e cy(imgF(z)) => EXIST(b):[b e imgG(cy(imgF(z))) & inv(b)=a]]]
U Spec, 583
585 Set(cy(imgF(z))) & Set(imgG(cy(imgF(z))))
& ALL(a):[a e cy(imgF(z)) => g(a) e imgG(cy(imgF(z)))]
& ALL(a):[a e imgG(cy(imgF(z))) => g'(a) e cy(imgF(z))]
& ALL(a):ALL(b):[a e cy(imgF(z)) & b e imgG(cy(imgF(z))) => [g'(b)=a <=> g(a)=b]]
=> ALL(a):ALL(b):[a e imgG(cy(imgF(z))) & b e imgG(cy(imgF(z))) => [g'(a)=g'(b) => a=b]]
& ALL(a):[a e cy(imgF(z)) => EXIST(b):[b e imgG(cy(imgF(z))) & g'(b)=a]]
U Spec, 584
586 Set(cy(imgF(z))) & Set(imgG(cy(imgF(z))))
Join, 565, 435
587 Set(cy(imgF(z))) & Set(imgG(cy(imgF(z))))
& ALL(a):[a e cy(imgF(z)) => g(a) e imgG(cy(imgF(z)))]
Join, 586, 521
588 Set(cy(imgF(z))) & Set(imgG(cy(imgF(z))))
& ALL(a):[a e cy(imgF(z)) => g(a) e imgG(cy(imgF(z)))]
& ALL(a):[a e cx(z) => g'(a) e cy(imgF(z))]
Join, 587, 580
589 Set(cy(imgF(z))) & Set(imgG(cy(imgF(z))))
& ALL(a):[a e cy(imgF(z)) => g(a) e imgG(cy(imgF(z)))]
& ALL(a):[a e imgG(cy(imgF(z))) => g'(a) e cy(imgF(z))]
Substitute, 448, 588
590 Set(cy(imgF(z))) & Set(imgG(cy(imgF(z))))
& ALL(a):[a e cy(imgF(z)) => g(a) e imgG(cy(imgF(z)))]
& ALL(a):[a e imgG(cy(imgF(z))) => g'(a) e cy(imgF(z))]
& ALL(a):ALL(b):[a e cy(imgF(z)) & b e cx(z) => [g'(b)=a <=> g(a)=b]]
Join, 589, 581
591 Set(cy(imgF(z))) & Set(imgG(cy(imgF(z))))
& ALL(a):[a e cy(imgF(z)) => g(a) e imgG(cy(imgF(z)))]
& ALL(a):[a e imgG(cy(imgF(z))) => g'(a) e cy(imgF(z))]
& ALL(a):ALL(b):[a e cy(imgF(z)) & b e imgG(cy(imgF(z))) => [g'(b)=a <=> g(a)=b]]
Substitute, 448, 590
592 ALL(a):ALL(b):[a e imgG(cy(imgF(z))) & b e imgG(cy(imgF(z))) => [g'(a)=g'(b) => a=b]]
& ALL(a):[a e cy(imgF(z)) => EXIST(b):[b e imgG(cy(imgF(z))) & g'(b)=a]]
Detach, 585, 591
g' is injective
593 ALL(a):ALL(b):[a e imgG(cy(imgF(z))) & b e imgG(cy(imgF(z))) => [g'(a)=g'(b) => a=b]]
Split, 592
g' is surjective
594 ALL(a):[a e cy(imgF(z)) => EXIST(b):[b e imgG(cy(imgF(z))) & g'(b)=a]]
Split, 592
595 ALL(a):ALL(b):[a e cx(z) & b e cx(z) => [g'(a)=g'(b) => a=b]]
Substitute, 448, 593
596 ALL(a):[a e cy(imgF(z)) => EXIST(b):[b e cx(z) & g'(b)=a]]
Substitute, 448, 594
Apply Cartesian Product Axiom
597 ALL(a1):ALL(a2):[Set(a1) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e a1 & c2 e a2]]]
Cart Prod
598 ALL(a2):[Set(x) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e a2]]]
U Spec, 597
599 Set(x) & Set(y) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e y]]
U Spec, 598
600 Set(x) & Set(y)
Join, 12, 13
601 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e y]]
Detach, 599, 600
602 Set'(xy) & ALL(c1):ALL(c2):[(c1,c2) e xy <=> c1 e x & c2 e y]
E Spec, 601
Define: xy (Cartesian product of x and y)
**********
603 Set'(xy)
Split, 602
604 ALL(c1):ALL(c2):[(c1,c2) e xy <=> c1 e x & c2 e y]
Split, 602
Apply Subset axiom
605 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e xy & [a e z & b=f(a) | ~a e z & b=g'(a)]]]
Subset, 603
606 Set'(k) & ALL(a):ALL(b):[(a,b) e k <=> (a,b) e xy & [a e z & b=f(a) | ~a e z & b=g'(a)]]
E Spec, 605
Define: k
*********
607 Set'(k)
Split, 606
608 ALL(a):ALL(b):[(a,b) e k <=> (a,b) e xy & [a e z & b=f(a) | ~a e z & b=g'(a)]]
Split, 606
Apply Function axiom
609 ALL(f):ALL(a):ALL(b):[ALL(c):ALL(d):[(c,d) e f => c e a & d e b]
& ALL(c):[c e a => EXIST(d):[d e b & (c,d) e f]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e f & (c,d2) e f => d1=d2]
=> ALL(c):ALL(d):[d=f(c) <=> (c,d) e f]]
Function
610 ALL(a):ALL(b):[ALL(c):ALL(d):[(c,d) e k => c e a & d e b]
& ALL(c):[c e a => EXIST(d):[d e b & (c,d) e k]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e k & (c,d2) e k => d1=d2]
=> ALL(c):ALL(d):[d=k(c) <=> (c,d) e k]]
U Spec, 609
611 ALL(b):[ALL(c):ALL(d):[(c,d) e k => c e x & d e b]
& ALL(c):[c e x => EXIST(d):[d e b & (c,d) e k]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e k & (c,d2) e k => d1=d2]
=> ALL(c):ALL(d):[d=k(c) <=> (c,d) e k]]
U Spec, 610
Sufficient: For functionality of k
612 ALL(c):ALL(d):[(c,d) e k => c e x & d e y]
& ALL(c):[c e x => EXIST(d):[d e y & (c,d) e k]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e k & (c,d2) e k => d1=d2]
=> ALL(c):ALL(d):[d=k(c) <=> (c,d) e k]
U Spec, 611
Prove: ALL(c):ALL(d):[(c,d) e k => c e x & d e y]
Suppose...
613 (p,q) e k
Premise
614 ALL(b):[(p,b) e k <=> (p,b) e xy & [p e z & b=f(p) | ~p e z & b=g'(p)]]
U Spec, 608
615 (p,q) e k <=> (p,q) e xy & [p e z & q=f(p) | ~p e z & q=g'(p)]
U Spec, 614
616 [(p,q) e k => (p,q) e xy & [p e z & q=f(p) | ~p e z & q=g'(p)]]
& [(p,q) e xy & [p e z & q=f(p) | ~p e z & q=g'(p)] => (p,q) e k]
Iff-And, 615
617 (p,q) e k => (p,q) e xy & [p e z & q=f(p) | ~p e z & q=g'(p)]
Split, 616
618 (p,q) e xy & [p e z & q=f(p) | ~p e z & q=g'(p)] => (p,q) e k
Split, 616
619 (p,q) e xy & [p e z & q=f(p) | ~p e z & q=g'(p)]
Detach, 617, 613
620 (p,q) e xy
Split, 619
621 p e z & q=f(p) | ~p e z & q=g'(p)
Split, 619
622 ALL(c2):[(p,c2) e xy <=> p e x & c2 e y]
U Spec, 604
623 (p,q) e xy <=> p e x & q e y
U Spec, 622
624 [(p,q) e xy => p e x & q e y]
& [p e x & q e y => (p,q) e xy]
Iff-And, 623
625 (p,q) e xy => p e x & q e y
Split, 624
626 p e x & q e y => (p,q) e xy
Split, 624
627 p e x & q e y
Detach, 625, 620
As Required:
628 ALL(c):ALL(d):[(c,d) e k => c e x & d e y]
4 Conclusion, 613
Prove: ALL(c):[c e x => EXIST(d):[d e y & (c,d) e k]]
Suppose...
629 p e x
Premise
2 cases:
630 p e z | ~p e z
Or Not
Case 1
Prove: p e z => EXIST(d):[d e y & (p,d) e k]
Suppose...
631 p e z
Premise
632 ALL(b):[(p,b) e k <=> (p,b) e xy & [p e z & b=f(p) | ~p e z & b=g'(p)]]
U Spec, 608
633 (p,f(p)) e k <=> (p,f(p)) e xy & [p e z & f(p)=f(p) | ~p e z & f(p)=g'(p)]
U Spec, 632
634 [(p,f(p)) e k => (p,f(p)) e xy & [p e z & f(p)=f(p) | ~p e z & f(p)=g'(p)]]
& [(p,f(p)) e xy & [p e z & f(p)=f(p) | ~p e z & f(p)=g'(p)] => (p,f(p)) e k]
Iff-And, 633
635 (p,f(p)) e k => (p,f(p)) e xy & [p e z & f(p)=f(p) | ~p e z & f(p)=g'(p)]
Split, 634
636 (p,f(p)) e xy & [p e z & f(p)=f(p) | ~p e z & f(p)=g'(p)] => (p,f(p)) e k
Split, 634
637 ALL(c2):[(p,c2) e xy <=> p e x & c2 e y]
U Spec, 604
638 (p,f(p)) e xy <=> p e x & f(p) e y
U Spec, 637
639 [(p,f(p)) e xy => p e x & f(p) e y]
& [p e x & f(p) e y => (p,f(p)) e xy]
Iff-And, 638
640 (p,f(p)) e xy => p e x & f(p) e y
Split, 639
641 p e x & f(p) e y => (p,f(p)) e xy
Split, 639
642 z e px <=> Set(z) & ALL(d):[d e z => d e x]
U Spec, 23
643 [z e px => Set(z) & ALL(d):[d e z => d e x]]
& [Set(z) & ALL(d):[d e z => d e x] => z e px]
Iff-And, 642
644 z e px => Set(z) & ALL(d):[d e z => d e x]
Split, 643
645 Set(z) & ALL(d):[d e z => d e x] => z e px
Split, 643
646 Set(z) & ALL(d):[d e z => d e x]
Detach, 644, 414
647 Set(z)
Split, 646
648 ALL(d):[d e z => d e x]
Split, 646
649 p e z => p e x
U Spec, 648
650 p e x
Detach, 649, 631
651 p e x => f(p) e y
U Spec, 14
652 f(p) e y
Detach, 651, 650
653 p e x & f(p) e y
Join, 650, 652
654 (p,f(p)) e xy
Detach, 641, 653
655 f(p)=f(p)
Reflex
656 p e z & f(p)=f(p)
Join, 631, 655
657 p e z & f(p)=f(p) | ~p e z & f(p)=g'(p)
Arb Or, 656
658 (p,f(p)) e xy
& [p e z & f(p)=f(p) | ~p e z & f(p)=g'(p)]
Join, 654, 657
659 (p,f(p)) e k
Detach, 636, 658
660 f(p) e y & (p,f(p)) e k
Join, 652, 659
661 EXIST(d):[d e y & (p,d) e k]
E Gen, 660
Case 1
As Required:
662 p e z => EXIST(d):[d e y & (p,d) e k]
4 Conclusion, 631
Case 2
Prove: ~p e z => EXIST(d):[d e y & (p,d) e k]
Suppose...
663 ~p e z
Premise
664 ALL(b):[(p,b) e k <=> (p,b) e xy & [p e z & b=f(p) | ~p e z & b=g'(p)]]
U Spec, 608
665 (p,g'(p)) e k <=> (p,g'(p)) e xy & [p e z & g'(p)=f(p) | ~p e z & g'(p)=g'(p)]
U Spec, 664
666 [(p,g'(p)) e k => (p,g'(p)) e xy & [p e z & g'(p)=f(p) | ~p e z & g'(p)=g'(p)]]
& [(p,g'(p)) e xy & [p e z & g'(p)=f(p) | ~p e z & g'(p)=g'(p)] => (p,g'(p)) e k]
Iff-And, 665
667 (p,g'(p)) e k => (p,g'(p)) e xy & [p e z & g'(p)=f(p) | ~p e z & g'(p)=g'(p)]
Split, 666
668 (p,g'(p)) e xy & [p e z & g'(p)=f(p) | ~p e z & g'(p)=g'(p)] => (p,g'(p)) e k
Split, 666
669 ALL(c2):[(p,c2) e xy <=> p e x & c2 e y]
U Spec, 604
670 (p,g'(p)) e xy <=> p e x & g'(p) e y
U Spec, 669
671 [(p,g'(p)) e xy => p e x & g'(p) e y]
& [p e x & g'(p) e y => (p,g'(p)) e xy]
Iff-And, 670
672 (p,g'(p)) e xy => p e x & g'(p) e y
Split, 671
673 p e x & g'(p) e y => (p,g'(p)) e xy
Split, 671
674 p e cx(z) => g'(p) e cy(imgF(z))
U Spec, 580
675 p e x => [p e cx(z) <=> ~p e z]
U Spec, 467
676 p e cx(z) <=> ~p e z
Detach, 675, 629
677 [p e cx(z) => ~p e z] & [~p e z => p e cx(z)]
Iff-And, 676
678 p e cx(z) => ~p e z
Split, 677
679 ~p e z => p e cx(z)
Split, 677
680 p e cx(z)
Detach, 679, 663
681 g'(p) e cy(imgF(z))
Detach, 674, 680
682 cy(imgF(z)) e py <=> Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]
U Spec, 28
683 [cy(imgF(z)) e py => Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]]
& [Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y] => cy(imgF(z)) e py]
Iff-And, 682
684 cy(imgF(z)) e py => Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]
Split, 683
685 Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y] => cy(imgF(z)) e py
Split, 683
686 Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]
Detach, 684, 461
687 Set(cy(imgF(z)))
Split, 686
688 ALL(d):[d e cy(imgF(z)) => d e y]
Split, 686
689 g'(p) e cy(imgF(z)) => g'(p) e y
U Spec, 688
690 g'(p) e y
Detach, 689, 681
691 p e x & g'(p) e y
Join, 629, 690
692 (p,g'(p)) e xy
Detach, 673, 691
693 g'(p)=g'(p)
Reflex
694 ~p e z & g'(p)=g'(p)
Join, 663, 693
695 p e z & g'(p)=f(p) | ~p e z & g'(p)=g'(p)
Arb Or, 694
696 (p,g'(p)) e xy
& [p e z & g'(p)=f(p) | ~p e z & g'(p)=g'(p)]
Join, 692, 695
697 (p,g'(p)) e k
Detach, 668, 696
698 g'(p) e y & (p,g'(p)) e k
Join, 690, 697
699 EXIST(d):[d e y & (p,d) e k]
E Gen, 698
Case 2
As Required:
700 ~p e z => EXIST(d):[d e y & (p,d) e k]
4 Conclusion, 663
701 [p e z => EXIST(d):[d e y & (p,d) e k]]
& [~p e z => EXIST(d):[d e y & (p,d) e k]]
Join, 662, 700
702 EXIST(d):[d e y & (p,d) e k]
Cases, 630, 701
As Required:
703 ALL(c):[c e x => EXIST(d):[d e y & (c,d) e k]]
4 Conclusion, 629
Prove: ALL(c):ALL(d1):ALL(d2):[(c,d1) e k & (c,d2) e k => d1=d2]
Suppose...
704 (p,q1) e k & (p,q2) e k
Premise
705 (p,q1) e k
Split, 704
706 (p,q2) e k
Split, 704
2 cases:
707 p e z | ~p e z
Or Not
Case 1
Suppose...
708 p e z
Premise
709 ALL(b):[(p,b) e k <=> (p,b) e xy & [p e z & b=f(p) | ~p e z & b=g'(p)]]
U Spec, 608
710 (p,q1) e k <=> (p,q1) e xy & [p e z & q1=f(p) | ~p e z & q1=g'(p)]
U Spec, 709
711 [(p,q1) e k => (p,q1) e xy & [p e z & q1=f(p) | ~p e z & q1=g'(p)]]
& [(p,q1) e xy & [p e z & q1=f(p) | ~p e z & q1=g'(p)] => (p,q1) e k]
Iff-And, 710
712 (p,q1) e k => (p,q1) e xy & [p e z & q1=f(p) | ~p e z & q1=g'(p)]
Split, 711
713 (p,q1) e xy & [p e z & q1=f(p) | ~p e z & q1=g'(p)] => (p,q1) e k
Split, 711
714 (p,q1) e xy & [p e z & q1=f(p) | ~p e z & q1=g'(p)]
Detach, 712, 705
715 (p,q1) e xy
Split, 714
716 p e z & q1=f(p) | ~p e z & q1=g'(p)
Split, 714
717 ~[p e z & q1=f(p)] => ~p e z & q1=g'(p)
Imply-Or, 716
718 ~[~p e z & q1=g'(p)] => ~~[p e z & q1=f(p)]
Contra, 717
719 ~[~p e z & q1=g'(p)] => p e z & q1=f(p)
Rem DNeg, 718
720 ~p e z & q1=g'(p)
Premise
721 ~p e z
Split, 720
722 q1=g'(p)
Split, 720
723 p e z & ~p e z
Join, 708, 721
724 ~[~p e z & q1=g'(p)]
4 Conclusion, 720
725 p e z & q1=f(p)
Detach, 719, 724
726 p e z
Split, 725
727 q1=f(p)
Split, 725
728 (p,q2) e k <=> (p,q2) e xy & [p e z & q2=f(p) | ~p e z & q2=g'(p)]
U Spec, 709
729 [(p,q2) e k => (p,q2) e xy & [p e z & q2=f(p) | ~p e z & q2=g'(p)]]
& [(p,q2) e xy & [p e z & q2=f(p) | ~p e z & q2=g'(p)] => (p,q2) e k]
Iff-And, 728
730 (p,q2) e k => (p,q2) e xy & [p e z & q2=f(p) | ~p e z & q2=g'(p)]
Split, 729
731 (p,q2) e xy & [p e z & q2=f(p) | ~p e z & q2=g'(p)] => (p,q2) e k
Split, 729
732 (p,q2) e xy & [p e z & q2=f(p) | ~p e z & q2=g'(p)]
Detach, 730, 706
733 (p,q2) e xy
Split, 732
734 p e z & q2=f(p) | ~p e z & q2=g'(p)
Split, 732
735 ~[p e z & q2=f(p)] => ~p e z & q2=g'(p)
Imply-Or, 734
736 ~[~p e z & q2=g'(p)] => ~~[p e z & q2=f(p)]
Contra, 735
737 ~[~p e z & q2=g'(p)] => p e z & q2=f(p)
Rem DNeg, 736
738 ~p e z & q2=g'(p)
Premise
739 ~p e z
Split, 738
740 q2=g'(p)
Split, 738
741 p e z & ~p e z
Join, 708, 739
742 ~[~p e z & q2=g'(p)]
4 Conclusion, 738
743 p e z & q2=f(p)
Detach, 737, 742
744 p e z
Split, 743
745 q2=f(p)
Split, 743
746 q1=q2
Substitute, 745, 727
Case 1
As Required:
747 p e z => q1=q2
4 Conclusion, 708
748 ~p e z
Premise
749 ALL(b):[(p,b) e k <=> (p,b) e xy & [p e z & b=f(p) | ~p e z & b=g'(p)]]
U Spec, 608
750 (p,q1) e k <=> (p,q1) e xy & [p e z & q1=f(p) | ~p e z & q1=g'(p)]
U Spec, 749
751 [(p,q1) e k => (p,q1) e xy & [p e z & q1=f(p) | ~p e z & q1=g'(p)]]
& [(p,q1) e xy & [p e z & q1=f(p) | ~p e z & q1=g'(p)] => (p,q1) e k]
Iff-And, 750
752 (p,q1) e k => (p,q1) e xy & [p e z & q1=f(p) | ~p e z & q1=g'(p)]
Split, 751
753 (p,q1) e xy & [p e z & q1=f(p) | ~p e z & q1=g'(p)] => (p,q1) e k
Split, 751
754 (p,q1) e xy & [p e z & q1=f(p) | ~p e z & q1=g'(p)]
Detach, 752, 705
755 (p,q1) e xy
Split, 754
756 p e z & q1=f(p) | ~p e z & q1=g'(p)
Split, 754
757 ~[p e z & q1=f(p)] => ~p e z & q1=g'(p)
Imply-Or, 756
758 p e z & q1=f(p)
Premise
759 p e z
Split, 758
760 q1=f(p)
Split, 758
761 p e z & ~p e z
Join, 759, 748
762 ~[p e z & q1=f(p)]
4 Conclusion, 758
763 ~p e z & q1=g'(p)
Detach, 757, 762
764 ~p e z
Split, 763
765 q1=g'(p)
Split, 763
766 (p,q2) e k <=> (p,q2) e xy & [p e z & q2=f(p) | ~p e z & q2=g'(p)]
U Spec, 749
767 [(p,q2) e k => (p,q2) e xy & [p e z & q2=f(p) | ~p e z & q2=g'(p)]]
& [(p,q2) e xy & [p e z & q2=f(p) | ~p e z & q2=g'(p)] => (p,q2) e k]
Iff-And, 766
768 (p,q2) e k => (p,q2) e xy & [p e z & q2=f(p) | ~p e z & q2=g'(p)]
Split, 767
769 (p,q2) e xy & [p e z & q2=f(p) | ~p e z & q2=g'(p)] => (p,q2) e k
Split, 767
770 (p,q2) e xy & [p e z & q2=f(p) | ~p e z & q2=g'(p)]
Detach, 768, 706
771 (p,q2) e xy
Split, 770
772 p e z & q2=f(p) | ~p e z & q2=g'(p)
Split, 770
773 ~[p e z & q2=f(p)] => ~p e z & q2=g'(p)
Imply-Or, 772
774 p e z & q2=f(p)
Premise
775 p e z
Split, 774
776 q2=f(p)
Split, 774
777 p e z & ~p e z
Join, 775, 748
778 ~[p e z & q2=f(p)]
4 Conclusion, 774
779 ~p e z & q2=g'(p)
Detach, 773, 778
780 ~p e z
Split, 779
781 q2=g'(p)
Split, 779
782 q1=q2
Substitute, 781, 765
As Required:
783 ~p e z => q1=q2
4 Conclusion, 748
784 [p e z => q1=q2] & [~p e z => q1=q2]
Join, 747, 783
785 q1=q2
Cases, 707, 784
As Required:
786 ALL(c):ALL(d1):ALL(d2):[(c,d1) e k & (c,d2) e k => d1=d2]
4 Conclusion, 704
787 ALL(c):ALL(d):[(c,d) e k => c e x & d e y]
& ALL(c):[c e x => EXIST(d):[d e y & (c,d) e k]]
Join, 628, 703
788 ALL(c):ALL(d):[(c,d) e k => c e x & d e y]
& ALL(c):[c e x => EXIST(d):[d e y & (c,d) e k]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e k & (c,d2) e k => d1=d2]
Join, 787, 786
As Required: k is a function
789 ALL(c):ALL(d):[d=k(c) <=> (c,d) e k]
Detach, 612, 788
Prove: ALL(a):[a e x => k(a) e y]
Suppose...
790 p e x
Premise
791 p e x => EXIST(d):[d e y & (p,d) e k]
U Spec, 703
792 EXIST(d):[d e y & (p,d) e k]
Detach, 791, 790
793 q e y & (p,q) e k
E Spec, 792
794 q e y
Split, 793
795 (p,q) e k
Split, 793
796 ALL(d):[d=k(p) <=> (p,d) e k]
U Spec, 789
797 q=k(p) <=> (p,q) e k
U Spec, 796
798 [q=k(p) => (p,q) e k] & [(p,q) e k => q=k(p)]
Iff-And, 797
799 q=k(p) => (p,q) e k
Split, 798
800 (p,q) e k => q=k(p)
Split, 798
801 q=k(p)
Detach, 800, 795
802 k(p) e y
Substitute, 801, 794
As Required:
803 ALL(a):[a e x => k(a) e y]
4 Conclusion, 790
Prove: ALL(a):[a e x
=> [a e z => k(a)=f(a)] & [~a e z => k(a)=g'(a)]]
Suppose...
804 p e x
Premise
Prove: p e z => k(p)=f(p)
Suppose...
805 p e z
Premise
806 ALL(b):[(p,b) e k <=> (p,b) e xy & [p e z & b=f(p) | ~p e z & b=g'(p)]]
U Spec, 608
807 (p,f(p)) e k <=> (p,f(p)) e xy & [p e z & f(p)=f(p) | ~p e z & f(p)=g'(p)]
U Spec, 806
808 [(p,f(p)) e k => (p,f(p)) e xy & [p e z & f(p)=f(p) | ~p e z & f(p)=g'(p)]]
& [(p,f(p)) e xy & [p e z & f(p)=f(p) | ~p e z & f(p)=g'(p)] => (p,f(p)) e k]
Iff-And, 807
809 (p,f(p)) e k => (p,f(p)) e xy & [p e z & f(p)=f(p) | ~p e z & f(p)=g'(p)]
Split, 808
810 (p,f(p)) e xy & [p e z & f(p)=f(p) | ~p e z & f(p)=g'(p)] => (p,f(p)) e k
Split, 808
811 ALL(c2):[(p,c2) e xy <=> p e x & c2 e y]
U Spec, 604
812 (p,f(p)) e xy <=> p e x & f(p) e y
U Spec, 811
813 [(p,f(p)) e xy => p e x & f(p) e y]
& [p e x & f(p) e y => (p,f(p)) e xy]
Iff-And, 812
814 (p,f(p)) e xy => p e x & f(p) e y
Split, 813
815 p e x & f(p) e y => (p,f(p)) e xy
Split, 813
816 p e x => f(p) e y
U Spec, 14
817 f(p) e y
Detach, 816, 804
818 p e x & f(p) e y
Join, 804, 817
819 (p,f(p)) e xy
Detach, 815, 818
820 (p,f(p)) e xy
Detach, 815, 818
821 f(p)=f(p)
Reflex
822 p e z & f(p)=f(p)
Join, 805, 821
823 p e z & f(p)=f(p) | ~p e z & f(p)=g'(p)
Arb Or, 822
824 (p,f(p)) e xy
& [p e z & f(p)=f(p) | ~p e z & f(p)=g'(p)]
Join, 820, 823
825 (p,f(p)) e k
Detach, 810, 824
826 ALL(d):[d=k(p) <=> (p,d) e k]
U Spec, 789
827 f(p)=k(p) <=> (p,f(p)) e k
U Spec, 826
828 [f(p)=k(p) => (p,f(p)) e k]
& [(p,f(p)) e k => f(p)=k(p)]
Iff-And, 827
829 f(p)=k(p) => (p,f(p)) e k
Split, 828
830 (p,f(p)) e k => f(p)=k(p)
Split, 828
831 f(p)=k(p)
Detach, 830, 825
832 k(p)=f(p)
Sym, 831
As Required:
833 p e z => k(p)=f(p)
4 Conclusion, 805
Prove: ~p e z => k(p)=g'(p)
Suppose...
834 ~p e z
Premise
835 ALL(b):[(p,b) e k <=> (p,b) e xy & [p e z & b=f(p) | ~p e z & b=g'(p)]]
U Spec, 608
836 (p,g'(p)) e k <=> (p,g'(p)) e xy & [p e z & g'(p)=f(p) | ~p e z & g'(p)=g'(p)]
U Spec, 835
837 [(p,g'(p)) e k => (p,g'(p)) e xy & [p e z & g'(p)=f(p) | ~p e z & g'(p)=g'(p)]]
& [(p,g'(p)) e xy & [p e z & g'(p)=f(p) | ~p e z & g'(p)=g'(p)] => (p,g'(p)) e k]
Iff-And, 836
838 (p,g'(p)) e k => (p,g'(p)) e xy & [p e z & g'(p)=f(p) | ~p e z & g'(p)=g'(p)]
Split, 837
839 (p,g'(p)) e xy & [p e z & g'(p)=f(p) | ~p e z & g'(p)=g'(p)] => (p,g'(p)) e k
Split, 837
840 ALL(c2):[(p,c2) e xy <=> p e x & c2 e y]
U Spec, 604
841 (p,g'(p)) e xy <=> p e x & g'(p) e y
U Spec, 840
842 [(p,g'(p)) e xy => p e x & g'(p) e y]
& [p e x & g'(p) e y => (p,g'(p)) e xy]
Iff-And, 841
843 (p,g'(p)) e xy => p e x & g'(p) e y
Split, 842
844 p e x & g'(p) e y => (p,g'(p)) e xy
Split, 842
845 p e cx(z) => g'(p) e cy(imgF(z))
U Spec, 580
846 p e x => [p e cx(z) <=> ~p e z]
U Spec, 467
847 p e cx(z) <=> ~p e z
Detach, 846, 804
848 [p e cx(z) => ~p e z] & [~p e z => p e cx(z)]
Iff-And, 847
849 p e cx(z) => ~p e z
Split, 848
850 ~p e z => p e cx(z)
Split, 848
851 p e cx(z)
Detach, 850, 834
852 g'(p) e cy(imgF(z))
Detach, 845, 851
853 cy(imgF(z)) e py <=> Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]
U Spec, 28
854 [cy(imgF(z)) e py => Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]]
& [Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y] => cy(imgF(z)) e py]
Iff-And, 853
855 cy(imgF(z)) e py => Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]
Split, 854
856 Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y] => cy(imgF(z)) e py
Split, 854
857 Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]
Detach, 855, 461
858 Set(cy(imgF(z)))
Split, 857
859 ALL(d):[d e cy(imgF(z)) => d e y]
Split, 857
860 g'(p) e cy(imgF(z)) => g'(p) e y
U Spec, 859
861 g'(p) e y
Detach, 860, 852
862 p e x & g'(p) e y
Join, 804, 861
863 (p,g'(p)) e xy
Detach, 844, 862
864 g'(p)=g'(p)
Reflex
865 ~p e z & g'(p)=g'(p)
Join, 834, 864
866 p e z & g'(p)=f(p) | ~p e z & g'(p)=g'(p)
Arb Or, 865
867 (p,g'(p)) e xy
& [p e z & g'(p)=f(p) | ~p e z & g'(p)=g'(p)]
Join, 863, 866
868 (p,g'(p)) e k
Detach, 839, 867
869 ALL(d):[d=k(p) <=> (p,d) e k]
U Spec, 789
870 g'(p)=k(p) <=> (p,g'(p)) e k
U Spec, 869
871 [g'(p)=k(p) => (p,g'(p)) e k]
& [(p,g'(p)) e k => g'(p)=k(p)]
Iff-And, 870
872 g'(p)=k(p) => (p,g'(p)) e k
Split, 871
873 (p,g'(p)) e k => g'(p)=k(p)
Split, 871
874 g'(p)=k(p)
Detach, 873, 868
875 k(p)=g'(p)
Sym, 874
As Required:
876 ~p e z => k(p)=g'(p)
4 Conclusion, 834
877 [p e z => k(p)=f(p)] & [~p e z => k(p)=g'(p)]
Join, 833, 876
As Required:
878 ALL(a):[a e x
=> [a e z => k(a)=f(a)] & [~a e z => k(a)=g'(a)]]
4 Conclusion, 804
Apply definition of Injection
879 ALL(a):ALL(b):[Injection(f,a,b) <=> ALL(c):ALL(d):[c e a & d e a => [f(c)=f(d) => c=d]]]
U Spec, 2
880 ALL(b):[Injection(f,x,b) <=> ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]]
U Spec, 879
881 Injection(f,x,y) <=> ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]
U Spec, 880
882 [Injection(f,x,y) => ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]]
& [ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]] => Injection(f,x,y)]
Iff-And, 881
883 Injection(f,x,y) => ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]
Split, 882
884 ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]] => Injection(f,x,y)
Split, 882
f is an injection on x
885 ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]
Detach, 883, 16
Apply definition of Subset
886 ALL(b):[Subset(z,b) <=> ALL(c):[c e z => c e b]]
U Spec, 1
887 Subset(z,x) <=> ALL(c):[c e z => c e x]
U Spec, 886
888 [Subset(z,x) => ALL(c):[c e z => c e x]]
& [ALL(c):[c e z => c e x] => Subset(z,x)]
Iff-And, 887
889 Subset(z,x) => ALL(c):[c e z => c e x]
Split, 888
890 ALL(c):[c e z => c e x] => Subset(z,x)
Split, 888
z is a subset of x
891 ALL(c):[c e z => c e x]
Detach, 889, 400
Prove: ALL(a):ALL(b):[a e x & b e x => [k(a)=k(b) => a=b]] (i.e. k is injective)
Suppose...
892 p e x & q e x
Premise
893 p e x
Split, 892
894 q e x
Split, 892
895 p e x
=> [p e z => k(p)=f(p)] & [~p e z => k(p)=g'(p)]
U Spec, 878
896 [p e z => k(p)=f(p)] & [~p e z => k(p)=g'(p)]
Detach, 895, 893
897 p e z => k(p)=f(p)
Split, 896
898 ~p e z => k(p)=g'(p)
Split, 896
899 q e x
=> [q e z => k(q)=f(q)] & [~q e z => k(q)=g'(q)]
U Spec, 878
900 [q e z => k(q)=f(q)] & [~q e z => k(q)=g'(q)]
Detach, 899, 894
901 q e z => k(q)=f(q)
Split, 900
902 ~q e z => k(q)=g'(q)
Split, 900
2 cases:
903 p e z | ~p e z
Or Not
2 sub-cases:
904 q e z | ~q e z
Or Not
Prove: k(p)=k(q) => p=q
Suppose...
905 k(p)=k(q)
Premise
Case 1
Suppose...
906 p e z
Premise
907 k(p)=f(p)
Detach, 897, 906
908 f(p)=k(q)
Substitute, 907, 905
Sub-case 1
Suppose...
909 q e z
Premise
910 k(q)=f(q)
Detach, 901, 909
911 f(p)=f(q)
Substitute, 910, 908
912 ALL(d):[p e x & d e x => [f(p)=f(d) => p=d]]
U Spec, 885
913 q e x
=> [q e z => k(q)=f(q)] & [~q e z => k(q)=g'(q)]
U Spec, 878
914 [q e z => k(q)=f(q)] & [~q e z => k(q)=g'(q)]
Detach, 913, 894
915 q e z => k(q)=f(q)
Split, 914
916 ~q e z => k(q)=g'(q)
Split, 914
917 k(q)=f(q)
Detach, 915, 909
918 f(p)=f(q)
Substitute, 917, 908
919 p e x & q e x => [f(p)=f(q) => p=q]
U Spec, 912
920 p e z => p e x
U Spec, 891
921 p e x
Detach, 920, 906
922 q e z => q e x
U Spec, 891
923 q e x
Detach, 922, 909
924 p e x & q e x
Join, 921, 923
925 f(p)=f(q) => p=q
Detach, 919, 924
926 p=q
Detach, 925, 918
Sub-case 1
As Required:
927 q e z => p=q
4 Conclusion, 909
Sub-case 2
Suppose...
928 ~q e z
Premise
929 k(q)=g'(q)
Detach, 902, 928
930 q e cx(z) => g'(q) e cy(imgF(z))
U Spec, 580
931 q e x => [q e cx(z) <=> ~q e z]
U Spec, 467
932 q e cx(z) <=> ~q e z
Detach, 931, 894
933 [q e cx(z) => ~q e z] & [~q e z => q e cx(z)]
Iff-And, 932
934 q e cx(z) => ~q e z
Split, 933
935 ~q e z => q e cx(z)
Split, 933
936 q e cx(z)
Detach, 935, 928
937 g'(q) e cy(imgF(z))
Detach, 930, 936
938 k(q) e cy(imgF(z))
Substitute, 929, 937
939 z e px
=> ALL(c):[c e imgF(z) <=> EXIST(d):[d e z & f(d)=c]]
U Spec, 51
940 ALL(c):[c e imgF(z) <=> EXIST(d):[d e z & f(d)=c]]
Detach, 939, 414
941 k(p) e imgF(z) <=> EXIST(d):[d e z & f(d)=k(p)]
U Spec, 940
942 [k(p) e imgF(z) => EXIST(d):[d e z & f(d)=k(p)]]
& [EXIST(d):[d e z & f(d)=k(p)] => k(p) e imgF(z)]
Iff-And, 941
943 k(p) e imgF(z) => EXIST(d):[d e z & f(d)=k(p)]
Split, 942
944 EXIST(d):[d e z & f(d)=k(p)] => k(p) e imgF(z)
Split, 942
945 f(p)=k(p)
Sym, 907
946 p e z & f(p)=k(p)
Join, 906, 945
947 EXIST(d):[d e z & f(d)=k(p)]
E Gen, 946
948 k(p) e imgF(z)
Detach, 944, 947
949 k(p) e cy(imgF(z))
Substitute, 905, 938
950 k(p) e y => [k(p) e cy(imgF(z)) <=> ~k(p) e imgF(z)]
U Spec, 463
951 p e x => k(p) e y
U Spec, 803
952 k(p) e y
Detach, 951, 893
953 k(p) e cy(imgF(z)) <=> ~k(p) e imgF(z)
Detach, 950, 952
954 [k(p) e cy(imgF(z)) => ~k(p) e imgF(z)]
& [~k(p) e imgF(z) => k(p) e cy(imgF(z))]
Iff-And, 953
955 k(p) e cy(imgF(z)) => ~k(p) e imgF(z)
Split, 954
956 ~k(p) e imgF(z) => k(p) e cy(imgF(z))
Split, 954
957 ~k(p) e imgF(z)
Detach, 955, 949
958 ~~k(p) e imgF(z) => p=q
Arb Cons, 957
959 k(p) e imgF(z) => p=q
Rem DNeg, 958
960 p=q
Detach, 959, 948
Sub-case 2
As Required:
961 ~q e z => p=q
4 Conclusion, 928
962 [q e z => p=q] & [~q e z => p=q]
Join, 927, 961
963 p=q
Cases, 904, 962
Case 1
As Required:
964 p e z => p=q
4 Conclusion, 906
Case 2
Prove: ~p e z => p=q
Suppose...
965 ~p e z
Premise
966 k(p)=g'(p)
Detach, 898, 965
Sub-case 1
Prove: q e z => p=q
Suppose...
967 q e z
Premise
968 k(q)=f(q)
Detach, 901, 967
969 p e cx(z) => g'(p) e cy(imgF(z))
U Spec, 580
970 p e x => [p e cx(z) <=> ~p e z]
U Spec, 467
971 p e cx(z) <=> ~p e z
Detach, 970, 893
972 [p e cx(z) => ~p e z] & [~p e z => p e cx(z)]
Iff-And, 971
973 p e cx(z) => ~p e z
Split, 972
974 ~p e z => p e cx(z)
Split, 972
975 p e cx(z)
Detach, 974, 965
976 g'(p) e cy(imgF(z))
Detach, 969, 975
977 k(p) e cy(imgF(z))
Substitute, 966, 976
978 q e imgF(z) <=> EXIST(d):[d e z & f(d)=q]
U Spec, 459
979 f(q) e imgF(z) <=> EXIST(d):[d e z & f(d)=f(q)]
U Spec, 459
980 [f(q) e imgF(z) => EXIST(d):[d e z & f(d)=f(q)]]
& [EXIST(d):[d e z & f(d)=f(q)] => f(q) e imgF(z)]
Iff-And, 979
981 f(q) e imgF(z) => EXIST(d):[d e z & f(d)=f(q)]
Split, 980
982 EXIST(d):[d e z & f(d)=f(q)] => f(q) e imgF(z)
Split, 980
983 f(q)=f(q)
Reflex
984 q e z & f(q)=f(q)
Join, 967, 983
985 EXIST(d):[d e z & f(d)=f(q)]
E Gen, 984
986 f(q) e imgF(z)
Detach, 982, 985
987 k(q) e imgF(z)
Substitute, 968, 986
988 k(q) e y => [k(q) e cy(imgF(z)) <=> ~k(q) e imgF(z)]
U Spec, 463
989 q e x => k(q) e y
U Spec, 803
990 k(q) e y
Detach, 989, 894
991 k(q) e cy(imgF(z)) <=> ~k(q) e imgF(z)
Detach, 988, 990
992 [k(q) e cy(imgF(z)) => ~k(q) e imgF(z)]
& [~k(q) e imgF(z) => k(q) e cy(imgF(z))]
Iff-And, 991
993 k(q) e cy(imgF(z)) => ~k(q) e imgF(z)
Split, 992
994 ~k(q) e imgF(z) => k(q) e cy(imgF(z))
Split, 992
995 k(q) e cy(imgF(z))
Substitute, 905, 977
996 ~k(q) e imgF(z)
Detach, 993, 995
997 ~~k(q) e imgF(z) => p=q
Arb Cons, 996
998 k(q) e imgF(z) => p=q
Rem DNeg, 997
999 p=q
Detach, 998, 987
Sub-case 1
As Required:
1000 q e z => p=q
4 Conclusion, 967
Sub-case 2
Prove: ~q e z => p=q
Suppose...
1001 ~q e z
Premise
1002 k(q)=g'(q)
Detach, 902, 1001
1003 g'(p)=k(q)
Substitute, 966, 905
1004 g'(p)=g'(q)
Substitute, 1002, 1003
1005 ALL(b):[p e cx(z) & b e cx(z) => [g'(p)=g'(b) => p=b]]
U Spec, 595
1006 p e cx(z) & q e cx(z) => [g'(p)=g'(q) => p=q]
U Spec, 1005
1007 p e x => [p e cx(z) <=> ~p e z]
U Spec, 467
1008 p e cx(z) <=> ~p e z
Detach, 1007, 893
1009 [p e cx(z) => ~p e z] & [~p e z => p e cx(z)]
Iff-And, 1008
1010 p e cx(z) => ~p e z
Split, 1009
1011 ~p e z => p e cx(z)
Split, 1009
1012 p e cx(z)
Detach, 1011, 965
1013 q e x => [q e cx(z) <=> ~q e z]
U Spec, 467
1014 q e cx(z) <=> ~q e z
Detach, 1013, 894
1015 [q e cx(z) => ~q e z] & [~q e z => q e cx(z)]
Iff-And, 1014
1016 q e cx(z) => ~q e z
Split, 1015
1017 ~q e z => q e cx(z)
Split, 1015
1018 q e cx(z)
Detach, 1017, 1001
1019 p e cx(z) & q e cx(z)
Join, 1012, 1018
1020 g'(p)=g'(q) => p=q
Detach, 1006, 1019
1021 p=q
Detach, 1020, 1004
Sub-case 2
As Required:
1022 ~q e z => p=q
4 Conclusion, 1001
1023 [q e z => p=q] & [~q e z => p=q]
Join, 1000, 1022
1024 p=q
Cases, 904, 1023
Case 2
As Required:
1025 ~p e z => p=q
4 Conclusion, 965
1026 [p e z => p=q] & [~p e z => p=q]
Join, 964, 1025
1027 p=q
Cases, 903, 1026
As Required:
1028 k(p)=k(q) => p=q
4 Conclusion, 905
k is injective
1029 ALL(a):ALL(b):[a e x & b e x => [k(a)=k(b) => a=b]]
4 Conclusion, 892
1030 p e imgF(z)
Premise
1031 z e px
=> ALL(c):[c e imgF(z) <=> EXIST(d):[d e z & f(d)=c]]
U Spec, 51
1032 ALL(c):[c e imgF(z) <=> EXIST(d):[d e z & f(d)=c]]
Detach, 1031, 414
1033 p e imgF(z) <=> EXIST(d):[d e z & f(d)=p]
U Spec, 1032
1034 [p e imgF(z) => EXIST(d):[d e z & f(d)=p]]
& [EXIST(d):[d e z & f(d)=p] => p e imgF(z)]
Iff-And, 1033
1035 p e imgF(z) => EXIST(d):[d e z & f(d)=p]
Split, 1034
1036 EXIST(d):[d e z & f(d)=p] => p e imgF(z)
Split, 1034
1037 EXIST(d):[d e z & f(d)=p]
Detach, 1035, 1030
f: z -> imgF(z) is surjective
1038 ALL(a):[a e imgF(z) => EXIST(d):[d e z & f(d)=a]]
4 Conclusion, 1030
1039 Set(z) & Set(imgF(z))
& ALL(a):[a e z => f(a) e imgF(z)]
& ALL(a):[a e imgF(z) => EXIST(d):[d e z & f(d)=a]]
Join, 511, 1038
1040 Set(z) & Set(imgF(z))
& ALL(a):[a e z => f(a) e imgF(z)]
& ALL(a):[a e imgF(z) => EXIST(d):[d e z & f(d)=a]]
& ALL(a):ALL(b):[a e z & b e z => [f(a)=f(b) => a=b]]
Join, 1039, 506
1041 EXIST(f'):[ALL(a):[a e imgF(z) => f'(a) e z]
& ALL(a):ALL(b):[a e z & b e imgF(z) => [f'(b)=a <=> f(a)=b]]]
Detach, 509, 1040
1042 ALL(a):[a e imgF(z) => f'(a) e z]
& ALL(a):ALL(b):[a e z & b e imgF(z) => [f'(b)=a <=> f(a)=b]]
E Spec, 1041
Define: f' (inverse of f: z -> imgF(z))
**********
1043 ALL(a):[a e imgF(z) => f'(a) e z]
Split, 1042
1044 ALL(a):ALL(b):[a e z & b e imgF(z) => [f'(b)=a <=> f(a)=b]]
Split, 1042
Prove: ALL(a):[aecx(z) => f(a)ecy(imgF(z))] i.e. f: cx(z) -> cy(imgF(z) is well-defined
Suppose...
1045 p e cx(z)
Premise
1046 f(p) e y => [f(p) e cy(imgF(z)) <=> ~f(p) e imgF(z)]
U Spec, 463
1047 p e x => f(p) e y
U Spec, 14
1048 cx(z) e px <=> Set(cx(z)) & ALL(d):[d e cx(z) => d e x]
U Spec, 23
1049 [cx(z) e px => Set(cx(z)) & ALL(d):[d e cx(z) => d e x]]
& [Set(cx(z)) & ALL(d):[d e cx(z) => d e x] => cx(z) e px]
Iff-And, 1048
1050 cx(z) e px => Set(cx(z)) & ALL(d):[d e cx(z) => d e x]
Split, 1049
1051 Set(cx(z)) & ALL(d):[d e cx(z) => d e x] => cx(z) e px
Split, 1049
1052 Set(cx(z)) & ALL(d):[d e cx(z) => d e x]
Detach, 1050, 465
1053 Set(cx(z))
Split, 1052
1054 ALL(d):[d e cx(z) => d e x]
Split, 1052
1055 p e cx(z) => p e x
U Spec, 1054
1056 p e x
Detach, 1055, 1045
1057 f(p) e y
Detach, 1047, 1056
1058 f(p) e cy(imgF(z)) <=> ~f(p) e imgF(z)
Detach, 1046, 1057
1059 [f(p) e cy(imgF(z)) => ~f(p) e imgF(z)]
& [~f(p) e imgF(z) => f(p) e cy(imgF(z))]
Iff-And, 1058
1060 f(p) e cy(imgF(z)) => ~f(p) e imgF(z)
Split, 1059
Sufficient:
1061 ~f(p) e imgF(z) => f(p) e cy(imgF(z))
Split, 1059
Prove: ~f(p) e imgF(z)
Suppose to the contrary...
1062 f(p) e imgF(z)
Premise
1063 f(p) e imgF(z) <=> EXIST(d):[d e z & f(d)=f(p)]
U Spec, 459
1064 [f(p) e imgF(z) => EXIST(d):[d e z & f(d)=f(p)]]
& [EXIST(d):[d e z & f(d)=f(p)] => f(p) e imgF(z)]
Iff-And, 1063
1065 f(p) e imgF(z) => EXIST(d):[d e z & f(d)=f(p)]
Split, 1064
1066 EXIST(d):[d e z & f(d)=f(p)] => f(p) e imgF(z)
Split, 1064
1067 EXIST(d):[d e z & f(d)=f(p)]
Detach, 1065, 1062
1068 q e z & f(q)=f(p)
E Spec, 1067
1069 q e z
Split, 1068
1070 f(q)=f(p)
Split, 1068
1071 ALL(a):ALL(b):[Injection(f,a,b) <=> ALL(c):ALL(d):[c e a & d e a => [f(c)=f(d) => c=d]]]
U Spec, 2
1072 ALL(b):[Injection(f,x,b) <=> ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]]
U Spec, 1071
1073 Injection(f,x,y) <=> ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]
U Spec, 1072
1074 [Injection(f,x,y) => ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]]
& [ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]] => Injection(f,x,y)]
Iff-And, 1073
1075 Injection(f,x,y) => ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]
Split, 1074
1076 ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]] => Injection(f,x,y)
Split, 1074
1077 ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]
Detach, 1075, 16
1078 ALL(d):[p e x & d e x => [f(p)=f(d) => p=d]]
U Spec, 1077
1079 p e x & q e x => [f(p)=f(q) => p=q]
U Spec, 1078
1080 z e px <=> Set(z) & ALL(d):[d e z => d e x]
U Spec, 23
1081 [z e px => Set(z) & ALL(d):[d e z => d e x]]
& [Set(z) & ALL(d):[d e z => d e x] => z e px]
Iff-And, 1080
1082 z e px => Set(z) & ALL(d):[d e z => d e x]
Split, 1081
1083 Set(z) & ALL(d):[d e z => d e x] => z e px
Split, 1081
1084 Set(z) & ALL(d):[d e z => d e x]
Detach, 1082, 414
1085 Set(z)
Split, 1084
1086 ALL(d):[d e z => d e x]
Split, 1084
1087 q e z => q e x
U Spec, 1086
1088 q e x
Detach, 1087, 1069
1089 p e x & q e x
Join, 1056, 1088
1090 f(p)=f(q) => p=q
Detach, 1079, 1089
1091 f(p)=f(q)
Sym, 1070
1092 p=q
Detach, 1090, 1091
1093 p e x => [p e cx(z) <=> ~p e z]
U Spec, 467
1094 p e cx(z) <=> ~p e z
Detach, 1093, 1056
1095 [p e cx(z) => ~p e z] & [~p e z => p e cx(z)]
Iff-And, 1094
1096 p e cx(z) => ~p e z
Split, 1095
1097 ~p e z => p e cx(z)
Split, 1095
1098 ~p e z
Detach, 1096, 1045
1099 ~q e z
Substitute, 1092, 1098
1100 q e z & ~q e z
Join, 1069, 1099
As Required:
1101 ~f(p) e imgF(z)
4 Conclusion, 1062
1102 f(p) e cy(imgF(z))
Detach, 1061, 1101
Define: f: cx(z) -> cy(imgF(z)) (a restriction on f: x -> y)
*******************************
1103 ALL(a):[a e cx(z) => f(a) e cy(imgF(z))]
4 Conclusion, 1045
Suppose...
1104 p e cx(z)
Premise
1105 p e cx(z) => f(p) e cy(imgF(z))
U Spec, 1103
1106 f(p) e cy(imgF(z))
Detach, 1105, 1104
1107 f(p) e y => [f(p) e cy(imgF(z)) <=> ~f(p) e imgF(z)]
U Spec, 463
1108 cy(imgF(z)) e py <=> Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]
U Spec, 28
1109 [cy(imgF(z)) e py => Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]]
& [Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y] => cy(imgF(z)) e py]
Iff-And, 1108
1110 cy(imgF(z)) e py => Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]
Split, 1109
1111 Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y] => cy(imgF(z)) e py
Split, 1109
1112 Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]
Detach, 1110, 461
1113 Set(cy(imgF(z)))
Split, 1112
1114 ALL(d):[d e cy(imgF(z)) => d e y]
Split, 1112
1115 f(p) e cy(imgF(z)) => f(p) e y
U Spec, 1114
1116 f(p) e y
Detach, 1115, 1106
1117 f(p) e cy(imgF(z)) <=> ~f(p) e imgF(z)
Detach, 1107, 1116
1118 [f(p) e cy(imgF(z)) => ~f(p) e imgF(z)]
& [~f(p) e imgF(z) => f(p) e cy(imgF(z))]
Iff-And, 1117
1119 f(p) e cy(imgF(z)) => ~f(p) e imgF(z)
Split, 1118
1120 ~f(p) e imgF(z) => f(p) e cy(imgF(z))
Split, 1118
1121 ~f(p) e imgF(z)
Detach, 1119, 1106
As Required:
1122 ALL(a):[a e cx(z) => ~f(a) e imgF(z)]
4 Conclusion, 1104
1123 ALL(a):[~~f(a) e imgF(z) => ~a e cx(z)]
Contra, 1122
As Required:
1124 ALL(a):[f(a) e imgF(z) => ~a e cx(z)]
Rem DNeg, 1123
Prove: ALL(a):[a e y => EXIST(b):[b e x & k(b)=a]] i.e. k is surjective
Suppose...
1125 p e y
Premise
2 cases:
1126 p e imgF(z) | ~p e imgF(z)
Or Not
Case 1
Prove: p e imgF(z) => EXIST(b):[b e x & p=k(b)]
Suppose...
1127 p e imgF(z)
Premise
1128 ALL(b):[(f'(p),b) e k <=> (f'(p),b) e xy & [f'(p) e z & b=f(f'(p)) | ~f'(p) e z & b=g'(f'(p))]]
U Spec, 608
1129 (f'(p),p) e k <=> (f'(p),p) e xy & [f'(p) e z & p=f(f'(p)) | ~f'(p) e z & p=g'(f'(p))]
U Spec, 1128
1130 [(f'(p),p) e k => (f'(p),p) e xy & [f'(p) e z & p=f(f'(p)) | ~f'(p) e z & p=g'(f'(p))]]
& [(f'(p),p) e xy & [f'(p) e z & p=f(f'(p)) | ~f'(p) e z & p=g'(f'(p))] => (f'(p),p) e k]
Iff-And, 1129
1131 (f'(p),p) e k => (f'(p),p) e xy & [f'(p) e z & p=f(f'(p)) | ~f'(p) e z & p=g'(f'(p))]
Split, 1130
1132 (f'(p),p) e xy & [f'(p) e z & p=f(f'(p)) | ~f'(p) e z & p=g'(f'(p))] => (f'(p),p) e k
Split, 1130
1133 ALL(c2):[(f'(p),c2) e xy <=> f'(p) e x & c2 e y]
U Spec, 604
1134 (f'(p),p) e xy <=> f'(p) e x & p e y
U Spec, 1133
1135 [(f'(p),p) e xy => f'(p) e x & p e y]
& [f'(p) e x & p e y => (f'(p),p) e xy]
Iff-And, 1134
1136 (f'(p),p) e xy => f'(p) e x & p e y
Split, 1135
1137 f'(p) e x & p e y => (f'(p),p) e xy
Split, 1135
1138 p e imgF(z) => f'(p) e z
U Spec, 1043
1139 f'(p) e z
Detach, 1138, 1127
1140 ALL(b):[Subset(z,b) <=> ALL(c):[c e z => c e b]]
U Spec, 1
1141 Subset(z,x) <=> ALL(c):[c e z => c e x]
U Spec, 1140
1142 [Subset(z,x) => ALL(c):[c e z => c e x]]
& [ALL(c):[c e z => c e x] => Subset(z,x)]
Iff-And, 1141
1143 Subset(z,x) => ALL(c):[c e z => c e x]
Split, 1142
1144 ALL(c):[c e z => c e x] => Subset(z,x)
Split, 1142
1145 ALL(c):[c e z => c e x]
Detach, 1143, 400
1146 f'(p) e z => f'(p) e x
U Spec, 1145
1147 f'(p) e x
Detach, 1146, 1139
1148 f'(p) e x & p e y
Join, 1147, 1125
1149 (f'(p),p) e xy
Detach, 1137, 1148
1150 ALL(b):[f'(p) e z & b e imgF(z) => [f'(b)=f'(p) <=> f(f'(p))=b]]
U Spec, 1044
1151 f'(p) e z & p e imgF(z) => [f'(p)=f'(p) <=> f(f'(p))=p]
U Spec, 1150
1152 f'(p) e z & p e imgF(z)
Join, 1139, 1127
1153 f'(p)=f'(p) <=> f(f'(p))=p
Detach, 1151, 1152
1154 [f'(p)=f'(p) => f(f'(p))=p]
& [f(f'(p))=p => f'(p)=f'(p)]
Iff-And, 1153
1155 f'(p)=f'(p) => f(f'(p))=p
Split, 1154
1156 f(f'(p))=p => f'(p)=f'(p)
Split, 1154
1157 f'(p)=f'(p)
Reflex
1158 f(f'(p))=p
Detach, 1155, 1157
1159 p=f(f'(p))
Sym, 1158
1160 f'(p) e z & p=f(f'(p))
Join, 1139, 1159
1161 f'(p) e z & p=f(f'(p)) | ~f'(p) e z & p=g'(f'(p))
Arb Or, 1160
1162 (f'(p),p) e xy
& [f'(p) e z & p=f(f'(p)) | ~f'(p) e z & p=g'(f'(p))]
Join, 1149, 1161
1163 (f'(p),p) e k
Detach, 1132, 1162
1164 ALL(d):[d=k(f'(p)) <=> (f'(p),d) e k]
U Spec, 789
1165 p=k(f'(p)) <=> (f'(p),p) e k
U Spec, 1164
1166 [p=k(f'(p)) => (f'(p),p) e k]
& [(f'(p),p) e k => p=k(f'(p))]
Iff-And, 1165
1167 p=k(f'(p)) => (f'(p),p) e k
Split, 1166
1168 (f'(p),p) e k => p=k(f'(p))
Split, 1166
1169 p=k(f'(p))
Detach, 1168, 1163
1170 f'(p) e x & p=k(f'(p))
Join, 1147, 1169
1171 EXIST(b):[b e x & p=k(b)]
E Gen, 1170
Case 1
As Required:
1172 p e imgF(z) => EXIST(b):[b e x & p=k(b)]
4 Conclusion, 1127
Case 2
Prove: ~p e imgF(z) => EXIST(b):[b e x & p=k(b)]
Suppose...
1173 ~p e imgF(z)
Premise
1174 ALL(b):[(g(p),b) e k <=> (g(p),b) e xy & [g(p) e z & b=f(g(p)) | ~g(p) e z & b=g'(g(p))]]
U Spec, 608
1175 (g(p),p) e k <=> (g(p),p) e xy & [g(p) e z & p=f(g(p)) | ~g(p) e z & p=g'(g(p))]
U Spec, 1174
1176 [(g(p),p) e k => (g(p),p) e xy & [g(p) e z & p=f(g(p)) | ~g(p) e z & p=g'(g(p))]]
& [(g(p),p) e xy & [g(p) e z & p=f(g(p)) | ~g(p) e z & p=g'(g(p))] => (g(p),p) e k]
Iff-And, 1175
1177 (g(p),p) e k => (g(p),p) e xy & [g(p) e z & p=f(g(p)) | ~g(p) e z & p=g'(g(p))]
Split, 1176
1178 (g(p),p) e xy & [g(p) e z & p=f(g(p)) | ~g(p) e z & p=g'(g(p))] => (g(p),p) e k
Split, 1176
1179 ALL(c2):[(g(p),c2) e xy <=> g(p) e x & c2 e y]
U Spec, 604
1180 (g(p),p) e xy <=> g(p) e x & p e y
U Spec, 1179
1181 [(g(p),p) e xy => g(p) e x & p e y]
& [g(p) e x & p e y => (g(p),p) e xy]
Iff-And, 1180
1182 (g(p),p) e xy => g(p) e x & p e y
Split, 1181
1183 g(p) e x & p e y => (g(p),p) e xy
Split, 1181
1184 p e y => g(p) e x
U Spec, 15
1185 g(p) e x
Detach, 1184, 1125
1186 g(p) e x & p e y
Join, 1185, 1125
1187 (g(p),p) e xy
Detach, 1183, 1186
1188 p e cy(imgF(z)) => g(p) e imgG(cy(imgF(z)))
U Spec, 521
1189 p e y => [p e cy(imgF(z)) <=> ~p e imgF(z)]
U Spec, 463
1190 p e cy(imgF(z)) <=> ~p e imgF(z)
Detach, 1189, 1125
1191 [p e cy(imgF(z)) => ~p e imgF(z)]
& [~p e imgF(z) => p e cy(imgF(z))]
Iff-And, 1190
1192 p e cy(imgF(z)) => ~p e imgF(z)
Split, 1191
1193 ~p e imgF(z) => p e cy(imgF(z))
Split, 1191
1194 p e cy(imgF(z))
Detach, 1193, 1173
1195 p e cy(imgF(z)) => g(p) e imgG(cy(imgF(z)))
U Spec, 521
1196 g(p) e imgG(cy(imgF(z)))
Detach, 1195, 1194
1197 g(p) e x => [g(p) e cx(z) <=> ~g(p) e z]
U Spec, 467
1198 p e y => g(p) e x
U Spec, 15
1199 g(p) e x
Detach, 1198, 1125
1200 g(p) e cx(z) <=> ~g(p) e z
Detach, 1197, 1199
1201 [g(p) e cx(z) => ~g(p) e z]
& [~g(p) e z => g(p) e cx(z)]
Iff-And, 1200
Sufficient:
1202 g(p) e cx(z) => ~g(p) e z
Split, 1201
1203 ~g(p) e z => g(p) e cx(z)
Split, 1201
1204 g(p) e imgG(cy(imgF(z))) => ~g(p) e z
Substitute, 448, 1202
1205 ~g(p) e z
Detach, 1204, 1196
1206 ALL(b):[p e cy(imgF(z)) & b e cx(z) => [g'(b)=p <=> g(p)=b]]
U Spec, 581
1207 p e cy(imgF(z)) & g(p) e cx(z) => [g'(g(p))=p <=> g(p)=g(p)]
U Spec, 1206
1208 g(p) e x => [g(p) e cx(z) <=> ~g(p) e z]
U Spec, 467
1209 g(p) e cx(z) <=> ~g(p) e z
Detach, 1208, 1199
1210 [g(p) e cx(z) => ~g(p) e z]
& [~g(p) e z => g(p) e cx(z)]
Iff-And, 1209
1211 g(p) e cx(z) => ~g(p) e z
Split, 1210
1212 ~g(p) e z => g(p) e cx(z)
Split, 1210
1213 g(p) e cx(z)
Detach, 1212, 1205
1214 p e cy(imgF(z)) & g(p) e cx(z)
Join, 1194, 1213
1215 g'(g(p))=p <=> g(p)=g(p)
Detach, 1207, 1214
1216 [g'(g(p))=p => g(p)=g(p)] & [g(p)=g(p) => g'(g(p))=p]
Iff-And, 1215
1217 g'(g(p))=p => g(p)=g(p)
Split, 1216
1218 g(p)=g(p) => g'(g(p))=p
Split, 1216
1219 g(p)=g(p)
Reflex
1220 g'(g(p))=p
Detach, 1218, 1219
1221 p=g'(g(p))
Sym, 1220
1222 ~g(p) e z & p=g'(g(p))
Join, 1205, 1221
1223 g(p) e z & p=f(g(p)) | ~g(p) e z & p=g'(g(p))
Arb Or, 1222
1224 (g(p),p) e xy
& [g(p) e z & p=f(g(p)) | ~g(p) e z & p=g'(g(p))]
Join, 1187, 1223
1225 (g(p),p) e k
Detach, 1178, 1224
1226 ALL(d):[d=k(g(p)) <=> (g(p),d) e k]
U Spec, 789
1227 p=k(g(p)) <=> (g(p),p) e k
U Spec, 1226
1228 [p=k(g(p)) => (g(p),p) e k]
& [(g(p),p) e k => p=k(g(p))]
Iff-And, 1227
1229 p=k(g(p)) => (g(p),p) e k
Split, 1228
1230 (g(p),p) e k => p=k(g(p))
Split, 1228
1231 p=k(g(p))
Detach, 1230, 1225
1232 g(p) e x & p=k(g(p))
Join, 1199, 1231
1233 EXIST(b):[b e x & p=k(b)]
E Gen, 1232
Case 2
As Required:
1234 ~p e imgF(z) => EXIST(b):[b e x & p=k(b)]
4 Conclusion, 1173
1235 [p e imgF(z) => EXIST(b):[b e x & p=k(b)]]
& [~p e imgF(z) => EXIST(b):[b e x & p=k(b)]]
Join, 1172, 1234
1236 EXIST(b):[b e x & p=k(b)]
Cases, 1126, 1235
1237 EXIST(b):[b e x & k(b)=p]
Sym, 1236
k is surjective
As Required:
1238 ALL(a):[a e y => EXIST(b):[b e x & k(b)=a]]
4 Conclusion, 1125
Use Injection, Surjection and Bijection predicates
1239 ALL(a):ALL(b):[Bijection(k,a,b) <=> Injection(k,a,b) & Surjection(k,a,b)]
U Spec, 4
1240 ALL(b):[Bijection(k,x,b) <=> Injection(k,x,b) & Surjection(k,x,b)]
U Spec, 1239
1241 Bijection(k,x,y) <=> Injection(k,x,y) & Surjection(k,x,y)
U Spec, 1240
1242 [Bijection(k,x,y) => Injection(k,x,y) & Surjection(k,x,y)]
& [Injection(k,x,y) & Surjection(k,x,y) => Bijection(k,x,y)]
Iff-And, 1241
1243 Bijection(k,x,y) => Injection(k,x,y) & Surjection(k,x,y)
Split, 1242
1244 Injection(k,x,y) & Surjection(k,x,y) => Bijection(k,x,y)
Split, 1242
1245 ALL(a):ALL(b):[Injection(k,a,b) <=> ALL(c):ALL(d):[c e a & d e a => [k(c)=k(d) => c=d]]]
U Spec, 2
1246 ALL(b):[Injection(k,x,b) <=> ALL(c):ALL(d):[c e x & d e x => [k(c)=k(d) => c=d]]]
U Spec, 1245
1247 Injection(k,x,y) <=> ALL(c):ALL(d):[c e x & d e x => [k(c)=k(d) => c=d]]
U Spec, 1246
1248 [Injection(k,x,y) => ALL(c):ALL(d):[c e x & d e x => [k(c)=k(d) => c=d]]]
& [ALL(c):ALL(d):[c e x & d e x => [k(c)=k(d) => c=d]] => Injection(k,x,y)]
Iff-And, 1247
1249 Injection(k,x,y) => ALL(c):ALL(d):[c e x & d e x => [k(c)=k(d) => c=d]]
Split, 1248
1250 ALL(c):ALL(d):[c e x & d e x => [k(c)=k(d) => c=d]] => Injection(k,x,y)
Split, 1248
1251 Injection(k,x,y)
Detach, 1250, 1029
1252 ALL(a):ALL(b):[Surjection(k,a,b) <=> ALL(c):[c e b => EXIST(d):[d e a & k(d)=c]]]
U Spec, 3
1253 ALL(b):[Surjection(k,x,b) <=> ALL(c):[c e b => EXIST(d):[d e x & k(d)=c]]]
U Spec, 1252
1254 Surjection(k,x,y) <=> ALL(c):[c e y => EXIST(d):[d e x & k(d)=c]]
U Spec, 1253
1255 [Surjection(k,x,y) => ALL(c):[c e y => EXIST(d):[d e x & k(d)=c]]]
& [ALL(c):[c e y => EXIST(d):[d e x & k(d)=c]] => Surjection(k,x,y)]
Iff-And, 1254
1256 Surjection(k,x,y) => ALL(c):[c e y => EXIST(d):[d e x & k(d)=c]]
Split, 1255
1257 ALL(c):[c e y => EXIST(d):[d e x & k(d)=c]] => Surjection(k,x,y)
Split, 1255
1258 Surjection(k,x,y)
Detach, 1257, 1238
1259 Injection(k,x,y) & Surjection(k,x,y)
Join, 1251, 1258
1260 Bijection(k,x,y)
Detach, 1244, 1259
As Required:
1261 ALL(a):[a e x => k(a) e y] & Bijection(k,x,y)
Join, 803, 1260
As Required:
1262 ALL(s1):ALL(s2):ALL(f1):ALL(f2):[Set(s1)
& Set(s2)
& ALL(a):[a e s1 => f1(a) e s2]
& ALL(a):[a e s2 => f2(a) e s1]
& Injection(f1,s1,s2)
& Injection(f2,s2,s1)
=> EXIST(f3):[ALL(a):[a e s1 => f3(a) e s2] & Bijection(f3,s1,s2)]]
4 Conclusion, 11