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