THEOREM
*******
Here we prove that two definitions of infinite are equivalent given the Peano Axioms.
Definition A: A set S is infinite if and only if there is a function f is defined on it that
is injective but not surjective
Definition B: A set S is infinite if and only if there is an injective function mapping
mapping the set of natural numbers to S.
Informal Outline of Proof
*************************
Let s be a set.
'=>'
Suppose s is infinite by Def A, i.e. there exists function f: s --> s where f is injective but not surjective.
Prove s is infinite by Def B, i.e. there exists a injective function mapping the set of natural numbers (nat) to s.
Since f is not surjective, there exists an element n0 in s that has no pre-image under f.
Construct a subset n of s that satisfies the Peano axioms with the zero being n0, and the successor function being f.
By a previous result, there exists an isomorphism g from nat to n (a subset of s). It is then easy to prove that g
is the required injective function from N to s.
'<='
Suppose s is infinite by Def B, i.e. there exists an injective h function mapping nat to s.
Prove s is infinite by Def A, i.e. there exists a function mapping on s that is injection, but not surjective.
Construct the subset t of s that is the range under f. Prove that t is infinite under Def A. Apply previous result
to show that s, as a superset of t, must also be infinite by Def A.
(This proof was written with the aid of the author's DC Proof 2.0 software available free at http://www.dcproof.com )
PEANO'S AXIOMS
**************
1 Set(nat)
& 0 e nat
& ALL(b):[b e nat => next(b) e nat]
& ALL(b):ALL(c):[b e nat & c e nat => [next(b)=next(c) => b=c]]
& ALL(b):[b e nat => ~next(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e nat]
=> [0 e b
& ALL(c):[c e b => next(c) e b]
=> ALL(c):[c e nat => c e b]]]
Axiom
2 Set(nat)
Split, 1
3 0 e nat
Split, 1
4 ALL(b):[b e nat => next(b) e nat]
Split, 1
5 ALL(b):ALL(c):[b e nat & c e nat => [next(b)=next(c) => b=c]]
Split, 1
6 ALL(b):[b e nat => ~next(b)=0]
Split, 1
7 ALL(b):[Set(b)
& ALL(c):[c e b => c e nat]
=> [0 e b
& ALL(c):[c e b => next(c) e b]
=> ALL(c):[c e nat => c e b]]]
Split, 1
DEFINITIONS
***********
Define: InfiniteA
A set is infinite if and only if there exists a function on that set that is injective but not surjective.
8 ALL(a):[Set(a) => [InfiniteA(a)
<=> EXIST(f):[ALL(b):[b e a => f(b) e a]
& ALL(b):ALL(c):[b e a & c e a => [f(b)=f(c) => b=c]]
& EXIST(b):[b e a & ALL(c):[c e a => ~f(c)=b]]]]]
Axiom
Define: InfiniteB
A set is infinite if and only if here exists an injective function mapping the set of natural numebers (nat)
to that set.
9 ALL(a):[Set(a) => [InfiniteB(a)
<=> EXIST(f):[ALL(b):[b e nat => f(b) e a]
& ALL(b):ALL(c):[b e nat & c e nat => [f(b)=f(c) => b=c]]]]]
Axiom
PREVIOUS RESULTS
****************
The existence of a mapping between two Peano systems (PeanoThm1.htm)
(From previous blog)
10 ALL(n1):ALL(z1):ALL(next1):ALL(n2):ALL(z2):ALL(next2):[Set(n1)
& z1 e n1
& ALL(a):[a e n1 => next1(a) e n1]
& ALL(a):ALL(b):[a e n1 & b e n1 => [next1(a)=next1(b) => a=b]]
& ALL(a):[a e n1 => ~next1(a)=z1]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n1]
=> [z1 e a & ALL(b):[b e a => next1(b) e a]
=> ALL(b):[b e n1 => b e a]]]
& Set(n2)
& z2 e n2
& ALL(a):[a e n2 => next2(a) e n2]
& ALL(a):ALL(b):[a e n2 & b e n2 => [next2(a)=next2(b) => a=b]]
& ALL(a):[a e n2 => ~next2(a)=z2]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n2]
=> [z2 e a & ALL(b):[b e a => next2(b) e a]
=> ALL(b):[b e n2 => b e a]]]
=> EXIST(f1):[ALL(a):[a e n1 => f1(a) e n2] & f1(z1)=z2
& ALL(a):[a e n1 => f1(next1(a))=next2(f1(a))]
& ALL(f2):[ALL(a):[a e n1 => f2(a) e n2]
& f2(z1)=z2
& ALL(a):[a e n1 => f2(next1(a))=next2(f2(a))]
=> ALL(a):[a e n1 => f2(a)=f1(a)]]]]
Axiom
The mapping between Peano system is a bijection (PeanoThm2.htm)
11 ALL(n1):ALL(z1):ALL(next1):ALL(n2):ALL(z2):ALL(next2):[Set(n1)
& z1 e n1
& ALL(a):[a e n1 => next1(a) e n1]
& ALL(a):ALL(b):[a e n1 & b e n1 => [next1(a)=next1(b) => a=b]]
& ALL(a):[a e n1 => ~next1(a)=z1]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n1]
=> [z1 e a & ALL(b):[b e a => next1(b) e a]
=> ALL(b):[b e n1 => b e a]]]
& Set(n2)
& z2 e n2
& ALL(a):[a e n2 => next2(a) e n2]
& ALL(a):ALL(b):[a e n2 & b e n2 => [next2(a)=next2(b) => a=b]]
& ALL(a):[a e n2 => ~next2(a)=z2]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n2]
=> [z2 e a & ALL(b):[b e a => next2(b) e a]
=> ALL(b):[b e n2 => b e a]]]
=> ALL(f1):[ALL(a):[a e n1 => f1(a) e n2]
& f1(z1)=z2
& ALL(a):[a e n1 => f1(next1(a))=next2(f1(a))]
=> ALL(a):[a e n2 => EXIST(b):[b e n1 & f1(b)=a]]
& ALL(a):ALL(b):[a e n1 & b e n1 => [f1(a)=f1(b) => a=b]]]]
Axiom
Infinite subsets (InfiniteSubsets.htm)
12 ALL(a):ALL(b):[Set(a) & Set(b) & ALL(c):[c e a => c e b]
=> [InfiniteA(a) => InfiniteA(b)]]
Axiom
PROOF
*****
Let s be a set
13 Set(s)
Premise
'=>'
Prove: InfiniteA(s) => InfiniteB(s)
Suppose...
14 InfiniteA(s)
Premise
Apply definition of InfiniteA
15 Set(s) => [InfiniteA(s)
<=> EXIST(f):[ALL(b):[b e s => f(b) e s]
& ALL(b):ALL(c):[b e s & c e s => [f(b)=f(c) => b=c]]
& EXIST(b):[b e s & ALL(c):[c e s => ~f(c)=b]]]]
U Spec, 8
16 InfiniteA(s)
<=> EXIST(f):[ALL(b):[b e s => f(b) e s]
& ALL(b):ALL(c):[b e s & c e s => [f(b)=f(c) => b=c]]
& EXIST(b):[b e s & ALL(c):[c e s => ~f(c)=b]]]
Detach, 15, 13
17 [InfiniteA(s) => EXIST(f):[ALL(b):[b e s => f(b) e s]
& ALL(b):ALL(c):[b e s & c e s => [f(b)=f(c) => b=c]]
& EXIST(b):[b e s & ALL(c):[c e s => ~f(c)=b]]]]
& [EXIST(f):[ALL(b):[b e s => f(b) e s]
& ALL(b):ALL(c):[b e s & c e s => [f(b)=f(c) => b=c]]
& EXIST(b):[b e s & ALL(c):[c e s => ~f(c)=b]]] => InfiniteA(s)]
Iff-And, 16
18 InfiniteA(s) => EXIST(f):[ALL(b):[b e s => f(b) e s]
& ALL(b):ALL(c):[b e s & c e s => [f(b)=f(c) => b=c]]
& EXIST(b):[b e s & ALL(c):[c e s => ~f(c)=b]]]
Split, 17
19 EXIST(f):[ALL(b):[b e s => f(b) e s]
& ALL(b):ALL(c):[b e s & c e s => [f(b)=f(c) => b=c]]
& EXIST(b):[b e s & ALL(c):[c e s => ~f(c)=b]]] => InfiniteA(s)
Split, 17
20 EXIST(f):[ALL(b):[b e s => f(b) e s]
& ALL(b):ALL(c):[b e s & c e s => [f(b)=f(c) => b=c]]
& EXIST(b):[b e s & ALL(c):[c e s => ~f(c)=b]]]
Detach, 18, 14
21 ALL(b):[b e s => f(b) e s]
& ALL(b):ALL(c):[b e s & c e s => [f(b)=f(c) => b=c]]
& EXIST(b):[b e s & ALL(c):[c e s => ~f(c)=b]]
E Spec, 20
Apply definition of InfiniteB
22 Set(s) => [InfiniteB(s)
<=> EXIST(f):[ALL(b):[b e nat => f(b) e s]
& ALL(b):ALL(c):[b e nat & c e nat => [f(b)=f(c) => b=c]]]]
U Spec, 9
23 InfiniteB(s)
<=> EXIST(f):[ALL(b):[b e nat => f(b) e s]
& ALL(b):ALL(c):[b e nat & c e nat => [f(b)=f(c) => b=c]]]
Detach, 22, 13
24 [InfiniteB(s) => EXIST(f):[ALL(b):[b e nat => f(b) e s]
& ALL(b):ALL(c):[b e nat & c e nat => [f(b)=f(c) => b=c]]]]
& [EXIST(f):[ALL(b):[b e nat => f(b) e s]
& ALL(b):ALL(c):[b e nat & c e nat => [f(b)=f(c) => b=c]]] => InfiniteB(s)]
Iff-And, 23
25 InfiniteB(s) => EXIST(f):[ALL(b):[b e nat => f(b) e s]
& ALL(b):ALL(c):[b e nat & c e nat => [f(b)=f(c) => b=c]]]
Split, 24
Sufficient: For InfiniteB(s)
26 EXIST(f):[ALL(b):[b e nat => f(b) e s]
& ALL(b):ALL(c):[b e nat & c e nat => [f(b)=f(c) => b=c]]] => InfiniteB(s)
Split, 24
Define: f
*********
27 ALL(b):[b e s => f(b) e s]
Split, 21
28 ALL(b):ALL(c):[b e s & c e s => [f(b)=f(c) => b=c]]
Split, 21
29 EXIST(b):[b e s & ALL(c):[c e s => ~f(c)=b]]
Split, 21
30 n0 e s & ALL(c):[c e s => ~f(c)=n0]
E Spec, 29
Define: n0
**********
31 n0 e s
Split, 30
n0 has no pre-image in s under f
32 ALL(c):[c e s => ~f(c)=n0]
Split, 30
33 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e s & ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> a e b]]]
Subset, 13
34 Set(n) & ALL(a):[a e n <=> a e s & ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> a e b]]
E Spec, 33
Define: n
*********
Informally, n = {n0, f(n0), f(f(n0)), .... }
35 Set(n)
Split, 34
36 ALL(a):[a e n <=> a e s & ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> a e b]]
Split, 34
37 x e n
Premise
38 x e n <=> x e s & ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
U Spec, 36
39 [x e n => x e s & ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]]
& [x e s & ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b] => x e n]
Iff-And, 38
40 x e n => x e s & ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Split, 39
41 x e s & ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b] => x e n
Split, 39
42 x e s & ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Detach, 40, 37
43 x e s
Split, 42
n is a subset of s
44 ALL(a):[a e n => a e s]
4 Conclusion, 37
Prove: n0 e n
Apply definition of n
45 n0 e n <=> n0 e s & ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> n0 e b]
U Spec, 36
46 [n0 e n => n0 e s & ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> n0 e b]]
& [n0 e s & ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> n0 e b] => n0 e n]
Iff-And, 45
47 n0 e n => n0 e s & ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> n0 e b]
Split, 46
Sufficient: For n0 e n
48 n0 e s & ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> n0 e b] => n0 e n
Split, 46
Prove: ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> n0 e b]
Suppose...
49 Set(p)
& n0 e p
& ALL(c):[c e p & c e s => f(c) e p]
Premise
50 Set(p)
Split, 49
51 n0 e p
Split, 49
As Required:
52 ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> n0 e b]
4 Conclusion, 49
53 n0 e s
& ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> n0 e b]
Join, 31, 52
PA1
***
54 n0 e n
Detach, 48, 53
Prove: ALL(a):[a e n => f(a) e n]
Suppose...
55 x e n
Premise
Apply definition of n
56 x e n <=> x e s & ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
U Spec, 36
57 [x e n => x e s & ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]]
& [x e s & ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b] => x e n]
Iff-And, 56
58 x e n => x e s & ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Split, 57
59 x e s & ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b] => x e n
Split, 57
60 x e s & ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Detach, 58, 55
61 x e s
Split, 60
62 ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Split, 60
Apply definition of n
63 f(x) e n <=> f(x) e s & ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> f(x) e b]
U Spec, 36
64 [f(x) e n => f(x) e s & ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> f(x) e b]]
& [f(x) e s & ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> f(x) e b] => f(x) e n]
Iff-And, 63
65 f(x) e n => f(x) e s & ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> f(x) e b]
Split, 64
Sufficient: f(x) e n
66 f(x) e s & ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> f(x) e b] => f(x) e n
Split, 64
67 x e s => f(x) e s
U Spec, 27
68 f(x) e s
Detach, 67, 61
Prove: ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> f(x) e b]
Suppose...
69 Set(p)
& n0 e p
& ALL(c):[c e p & c e s => f(c) e p]
Premise
70 Set(p)
Split, 69
71 n0 e p
Split, 69
72 ALL(c):[c e p & c e s => f(c) e p]
Split, 69
Sufficient: f(x) e p
73 x e p & x e s => f(x) e p
U Spec, 72
74 Set(p)
& n0 e p
& ALL(c):[c e p & c e s => f(c) e p]
=> x e p
U Spec, 62
75 x e p
Detach, 74, 69
76 x e p & x e s
Join, 75, 61
77 f(x) e p
Detach, 73, 76
As Required:
78 ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> f(x) e b]
4 Conclusion, 69
Joining results...
79 f(x) e s
& ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> f(x) e b]
Join, 68, 78
80 f(x) e n
Detach, 66, 79
PA2
***
81 ALL(a):[a e n => f(a) e n]
4 Conclusion, 55
Prove: ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]
Suppose...
82 x e n & y e n
Premise
83 x e n
Split, 82
84 y e n
Split, 82
Prove: f(x)=f(y) => x=y
Suppose...
85 f(x)=f(y)
Premise
Apply definition of f
86 ALL(c):[x e s & c e s => [f(x)=f(c) => x=c]]
U Spec, 28
87 x e s & y e s => [f(x)=f(y) => x=y]
U Spec, 86
88 x e n => x e s
U Spec, 44
89 x e s
Detach, 88, 83
90 y e n => y e s
U Spec, 44
91 y e s
Detach, 90, 84
92 x e s & y e s
Join, 89, 91
93 f(x)=f(y) => x=y
Detach, 87, 92
94 x=y
Detach, 93, 85
As Required:
95 f(x)=f(y) => x=y
4 Conclusion, 85
PA3
***
96 ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]
4 Conclusion, 82
Prove: ALL(a):[a e n => ~f(a)=n0]
Suppose...
97 x e n
Premise
98 x e s => ~f(x)=n0
U Spec, 32
99 x e n => x e s
U Spec, 44
100 x e s
Detach, 99, 97
101 ~f(x)=n0
Detach, 98, 100
PA4
***
102 ALL(a):[a e n => ~f(a)=n0]
4 Conclusion, 97
Prove: ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [n0 e a & ALL(b):[b e a => f(b) e a]
=> ALL(b):[b e n => b e a]]]
Suppose...
103 Set(p) & ALL(b):[b e p => b e n]
Premise
104 Set(p)
Split, 103
105 ALL(b):[b e p => b e n]
Split, 103
Prove: n0 e p & ALL(b):[b e p => f(b) e p]
=> ALL(b):[b e n => b e p]
Suppose...
106 n0 e p & ALL(b):[b e p => f(b) e p]
Premise
107 n0 e p
Split, 106
108 ALL(b):[b e p => f(b) e p]
Split, 106
Prove: ALL(b):[b e n => b e p]
Suppose...
109 x e n
Premise
Apply definition of n
110 x e n <=> x e s & ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
U Spec, 36
111 [x e n => x e s & ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]]
& [x e s & ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b] => x e n]
Iff-And, 110
112 x e n => x e s & ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Split, 111
113 x e s & ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b] => x e n
Split, 111
114 x e s & ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Detach, 112, 109
115 x e s
Split, 114
116 ALL(b):[Set(b)
& n0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Split, 114
Sufficient: For x e p
117 Set(p)
& n0 e p
& ALL(c):[c e p & c e s => f(c) e p]
=> x e p
U Spec, 116
Prove: ALL(c):[c e p & c e s => f(c) e p]
Suppose...
118 y e p & y e s
Premise
119 y e p
Split, 118
120 y e s
Split, 118
121 y e p => f(y) e p
U Spec, 108
122 f(y) e p
Detach, 121, 119
As Required:
123 ALL(c):[c e p & c e s => f(c) e p]
4 Conclusion, 118
124 Set(p) & n0 e p
Join, 104, 107
125 Set(p) & n0 e p
& ALL(c):[c e p & c e s => f(c) e p]
Join, 124, 123
126 x e p
Detach, 117, 125
As Required:
127 ALL(b):[b e n => b e p]
4 Conclusion, 109
As Required:
128 n0 e p & ALL(b):[b e p => f(b) e p]
=> ALL(b):[b e n => b e p]
4 Conclusion, 106
PA5
***
129 ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [n0 e a & ALL(b):[b e a => f(b) e a]
=> ALL(b):[b e n => b e a]]]
4 Conclusion, 103
Establish the existence of an isomorphism between the two Peano systems (nat,0,next)
and (n,n0,f)
Apply previous result
130 ALL(z1):ALL(next1):ALL(n2):ALL(z2):ALL(next2):[Set(nat)
& z1 e nat
& ALL(a):[a e nat => next1(a) e nat]
& ALL(a):ALL(b):[a e nat & b e nat => [next1(a)=next1(b) => a=b]]
& ALL(a):[a e nat => ~next1(a)=z1]
& ALL(a):[Set(a) & ALL(b):[b e a => b e nat]
=> [z1 e a & ALL(b):[b e a => next1(b) e a]
=> ALL(b):[b e nat => b e a]]]
& Set(n2)
& z2 e n2
& ALL(a):[a e n2 => next2(a) e n2]
& ALL(a):ALL(b):[a e n2 & b e n2 => [next2(a)=next2(b) => a=b]]
& ALL(a):[a e n2 => ~next2(a)=z2]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n2]
=> [z2 e a & ALL(b):[b e a => next2(b) e a]
=> ALL(b):[b e n2 => b e a]]]
=> EXIST(f1):[ALL(a):[a e nat => f1(a) e n2] & f1(z1)=z2
& ALL(a):[a e nat => f1(next1(a))=next2(f1(a))]
& ALL(f2):[ALL(a):[a e nat => f2(a) e n2]
& f2(z1)=z2
& ALL(a):[a e nat => f2(next1(a))=next2(f2(a))]
=> ALL(a):[a e nat => f2(a)=f1(a)]]]]
U Spec, 10
131 ALL(next1):ALL(n2):ALL(z2):ALL(next2):[Set(nat)
& 0 e nat
& ALL(a):[a e nat => next1(a) e nat]
& ALL(a):ALL(b):[a e nat & b e nat => [next1(a)=next1(b) => a=b]]
& ALL(a):[a e nat => ~next1(a)=0]
& ALL(a):[Set(a) & ALL(b):[b e a => b e nat]
=> [0 e a & ALL(b):[b e a => next1(b) e a]
=> ALL(b):[b e nat => b e a]]]
& Set(n2)
& z2 e n2
& ALL(a):[a e n2 => next2(a) e n2]
& ALL(a):ALL(b):[a e n2 & b e n2 => [next2(a)=next2(b) => a=b]]
& ALL(a):[a e n2 => ~next2(a)=z2]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n2]
=> [z2 e a & ALL(b):[b e a => next2(b) e a]
=> ALL(b):[b e n2 => b e a]]]
=> EXIST(f1):[ALL(a):[a e nat => f1(a) e n2] & f1(0)=z2
& ALL(a):[a e nat => f1(next1(a))=next2(f1(a))]
& ALL(f2):[ALL(a):[a e nat => f2(a) e n2]
& f2(0)=z2
& ALL(a):[a e nat => f2(next1(a))=next2(f2(a))]
=> ALL(a):[a e nat => f2(a)=f1(a)]]]]
U Spec, 130
132 ALL(n2):ALL(z2):ALL(next2):[Set(nat)
& 0 e nat
& ALL(a):[a e nat => next(a) e nat]
& ALL(a):ALL(b):[a e nat & b e nat => [next(a)=next(b) => a=b]]
& ALL(a):[a e nat => ~next(a)=0]
& ALL(a):[Set(a) & ALL(b):[b e a => b e nat]
=> [0 e a & ALL(b):[b e a => next(b) e a]
=> ALL(b):[b e nat => b e a]]]
& Set(n2)
& z2 e n2
& ALL(a):[a e n2 => next2(a) e n2]
& ALL(a):ALL(b):[a e n2 & b e n2 => [next2(a)=next2(b) => a=b]]
& ALL(a):[a e n2 => ~next2(a)=z2]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n2]
=> [z2 e a & ALL(b):[b e a => next2(b) e a]
=> ALL(b):[b e n2 => b e a]]]
=> EXIST(f1):[ALL(a):[a e nat => f1(a) e n2] & f1(0)=z2
& ALL(a):[a e nat => f1(next(a))=next2(f1(a))]
& ALL(f2):[ALL(a):[a e nat => f2(a) e n2]
& f2(0)=z2
& ALL(a):[a e nat => f2(next(a))=next2(f2(a))]
=> ALL(a):[a e nat => f2(a)=f1(a)]]]]
U Spec, 131
133 ALL(z2):ALL(next2):[Set(nat)
& 0 e nat
& ALL(a):[a e nat => next(a) e nat]
& ALL(a):ALL(b):[a e nat & b e nat => [next(a)=next(b) => a=b]]
& ALL(a):[a e nat => ~next(a)=0]
& ALL(a):[Set(a) & ALL(b):[b e a => b e nat]
=> [0 e a & ALL(b):[b e a => next(b) e a]
=> ALL(b):[b e nat => b e a]]]
& Set(n)
& z2 e n
& ALL(a):[a e n => next2(a) e n]
& ALL(a):ALL(b):[a e n & b e n => [next2(a)=next2(b) => a=b]]
& ALL(a):[a e n => ~next2(a)=z2]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [z2 e a & ALL(b):[b e a => next2(b) e a]
=> ALL(b):[b e n => b e a]]]
=> EXIST(f1):[ALL(a):[a e nat => f1(a) e n] & f1(0)=z2
& ALL(a):[a e nat => f1(next(a))=next2(f1(a))]
& ALL(f2):[ALL(a):[a e nat => f2(a) e n]
& f2(0)=z2
& ALL(a):[a e nat => f2(next(a))=next2(f2(a))]
=> ALL(a):[a e nat => f2(a)=f1(a)]]]]
U Spec, 132
134 ALL(next2):[Set(nat)
& 0 e nat
& ALL(a):[a e nat => next(a) e nat]
& ALL(a):ALL(b):[a e nat & b e nat => [next(a)=next(b) => a=b]]
& ALL(a):[a e nat => ~next(a)=0]
& ALL(a):[Set(a) & ALL(b):[b e a => b e nat]
=> [0 e a & ALL(b):[b e a => next(b) e a]
=> ALL(b):[b e nat => b e a]]]
& Set(n)
& n0 e n
& ALL(a):[a e n => next2(a) e n]
& ALL(a):ALL(b):[a e n & b e n => [next2(a)=next2(b) => a=b]]
& ALL(a):[a e n => ~next2(a)=n0]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [n0 e a & ALL(b):[b e a => next2(b) e a]
=> ALL(b):[b e n => b e a]]]
=> EXIST(f1):[ALL(a):[a e nat => f1(a) e n] & f1(0)=n0
& ALL(a):[a e nat => f1(next(a))=next2(f1(a))]
& ALL(f2):[ALL(a):[a e nat => f2(a) e n]
& f2(0)=n0
& ALL(a):[a e nat => f2(next(a))=next2(f2(a))]
=> ALL(a):[a e nat => f2(a)=f1(a)]]]]
U Spec, 133
135 Set(nat)
& 0 e nat
& ALL(a):[a e nat => next(a) e nat]
& ALL(a):ALL(b):[a e nat & b e nat => [next(a)=next(b) => a=b]]
& ALL(a):[a e nat => ~next(a)=0]
& ALL(a):[Set(a) & ALL(b):[b e a => b e nat]
=> [0 e a & ALL(b):[b e a => next(b) e a]
=> ALL(b):[b e nat => b e a]]]
& Set(n)
& n0 e n
& ALL(a):[a e n => f(a) e n]
& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]
& ALL(a):[a e n => ~f(a)=n0]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [n0 e a & ALL(b):[b e a => f(b) e a]
=> ALL(b):[b e n => b e a]]]
=> EXIST(f1):[ALL(a):[a e nat => f1(a) e n] & f1(0)=n0
& ALL(a):[a e nat => f1(next(a))=f(f1(a))]
& ALL(f2):[ALL(a):[a e nat => f2(a) e n]
& f2(0)=n0
& ALL(a):[a e nat => f2(next(a))=f(f2(a))]
=> ALL(a):[a e nat => f2(a)=f1(a)]]]
U Spec, 134
136 Set(nat)
& 0 e nat
& ALL(b):[b e nat => next(b) e nat]
& ALL(b):ALL(c):[b e nat & c e nat => [next(b)=next(c) => b=c]]
& ALL(b):[b e nat => ~next(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e nat]
=> [0 e b
& ALL(c):[c e b => next(c) e b]
=> ALL(c):[c e nat => c e b]]]
& Set(n)
Join, 1, 35
137 Set(nat)
& 0 e nat
& ALL(b):[b e nat => next(b) e nat]
& ALL(b):ALL(c):[b e nat & c e nat => [next(b)=next(c) => b=c]]
& ALL(b):[b e nat => ~next(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e nat]
=> [0 e b
& ALL(c):[c e b => next(c) e b]
=> ALL(c):[c e nat => c e b]]]
& Set(n)
& n0 e n
Join, 136, 54
138 Set(nat)
& 0 e nat
& ALL(b):[b e nat => next(b) e nat]
& ALL(b):ALL(c):[b e nat & c e nat => [next(b)=next(c) => b=c]]
& ALL(b):[b e nat => ~next(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e nat]
=> [0 e b
& ALL(c):[c e b => next(c) e b]
=> ALL(c):[c e nat => c e b]]]
& Set(n)
& n0 e n
& ALL(a):[a e n => f(a) e n]
Join, 137, 81
139 Set(nat)
& 0 e nat
& ALL(b):[b e nat => next(b) e nat]
& ALL(b):ALL(c):[b e nat & c e nat => [next(b)=next(c) => b=c]]
& ALL(b):[b e nat => ~next(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e nat]
=> [0 e b
& ALL(c):[c e b => next(c) e b]
=> ALL(c):[c e nat => c e b]]]
& Set(n)
& n0 e n
& ALL(a):[a e n => f(a) e n]
& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]
Join, 138, 96
140 Set(nat)
& 0 e nat
& ALL(b):[b e nat => next(b) e nat]
& ALL(b):ALL(c):[b e nat & c e nat => [next(b)=next(c) => b=c]]
& ALL(b):[b e nat => ~next(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e nat]
=> [0 e b
& ALL(c):[c e b => next(c) e b]
=> ALL(c):[c e nat => c e b]]]
& Set(n)
& n0 e n
& ALL(a):[a e n => f(a) e n]
& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]
& ALL(a):[a e n => ~f(a)=n0]
Join, 139, 102
141 Set(nat)
& 0 e nat
& ALL(b):[b e nat => next(b) e nat]
& ALL(b):ALL(c):[b e nat & c e nat => [next(b)=next(c) => b=c]]
& ALL(b):[b e nat => ~next(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e nat]
=> [0 e b
& ALL(c):[c e b => next(c) e b]
=> ALL(c):[c e nat => c e b]]]
& Set(n)
& n0 e n
& ALL(a):[a e n => f(a) e n]
& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]
& ALL(a):[a e n => ~f(a)=n0]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [n0 e a & ALL(b):[b e a => f(b) e a]
=> ALL(b):[b e n => b e a]]]
Join, 140, 129
142 EXIST(f1):[ALL(a):[a e nat => f1(a) e n] & f1(0)=n0
& ALL(a):[a e nat => f1(next(a))=f(f1(a))]
& ALL(f2):[ALL(a):[a e nat => f2(a) e n]
& f2(0)=n0
& ALL(a):[a e nat => f2(next(a))=f(f2(a))]
=> ALL(a):[a e nat => f2(a)=f1(a)]]]
Detach, 135, 141
143 ALL(a):[a e nat => g(a) e n] & g(0)=n0
& ALL(a):[a e nat => g(next(a))=f(g(a))]
& ALL(f2):[ALL(a):[a e nat => f2(a) e n]
& f2(0)=n0
& ALL(a):[a e nat => f2(next(a))=f(f2(a))]
=> ALL(a):[a e nat => f2(a)=g(a)]]
E Spec, 142
Define: g
*********
The isomorphism from nat (The Natural Numbers) to n
144 ALL(a):[a e nat => g(a) e n]
Split, 143
145 g(0)=n0
Split, 143
146 ALL(a):[a e nat => g(next(a))=f(g(a))]
Split, 143
147 ALL(f2):[ALL(a):[a e nat => f2(a) e n]
& f2(0)=n0
& ALL(a):[a e nat => f2(next(a))=f(f2(a))]
=> ALL(a):[a e nat => f2(a)=g(a)]]
Split, 143
148 ALL(z1):ALL(next1):ALL(n2):ALL(z2):ALL(next2):[Set(nat)
& z1 e nat
& ALL(a):[a e nat => next1(a) e nat]
& ALL(a):ALL(b):[a e nat & b e nat => [next1(a)=next1(b) => a=b]]
& ALL(a):[a e nat => ~next1(a)=z1]
& ALL(a):[Set(a) & ALL(b):[b e a => b e nat]
=> [z1 e a & ALL(b):[b e a => next1(b) e a]
=> ALL(b):[b e nat => b e a]]]
& Set(n2)
& z2 e n2
& ALL(a):[a e n2 => next2(a) e n2]
& ALL(a):ALL(b):[a e n2 & b e n2 => [next2(a)=next2(b) => a=b]]
& ALL(a):[a e n2 => ~next2(a)=z2]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n2]
=> [z2 e a & ALL(b):[b e a => next2(b) e a]
=> ALL(b):[b e n2 => b e a]]]
=> ALL(f1):[ALL(a):[a e nat => f1(a) e n2]
& f1(z1)=z2
& ALL(a):[a e nat => f1(next1(a))=next2(f1(a))]
=> ALL(a):[a e n2 => EXIST(b):[b e nat & f1(b)=a]]
& ALL(a):ALL(b):[a e nat & b e nat => [f1(a)=f1(b) => a=b]]]]
U Spec, 11
149 ALL(next1):ALL(n2):ALL(z2):ALL(next2):[Set(nat)
& 0 e nat
& ALL(a):[a e nat => next1(a) e nat]
& ALL(a):ALL(b):[a e nat & b e nat => [next1(a)=next1(b) => a=b]]
& ALL(a):[a e nat => ~next1(a)=0]
& ALL(a):[Set(a) & ALL(b):[b e a => b e nat]
=> [0 e a & ALL(b):[b e a => next1(b) e a]
=> ALL(b):[b e nat => b e a]]]
& Set(n2)
& z2 e n2
& ALL(a):[a e n2 => next2(a) e n2]
& ALL(a):ALL(b):[a e n2 & b e n2 => [next2(a)=next2(b) => a=b]]
& ALL(a):[a e n2 => ~next2(a)=z2]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n2]
=> [z2 e a & ALL(b):[b e a => next2(b) e a]
=> ALL(b):[b e n2 => b e a]]]
=> ALL(f1):[ALL(a):[a e nat => f1(a) e n2]
& f1(0)=z2
& ALL(a):[a e nat => f1(next1(a))=next2(f1(a))]
=> ALL(a):[a e n2 => EXIST(b):[b e nat & f1(b)=a]]
& ALL(a):ALL(b):[a e nat & b e nat => [f1(a)=f1(b) => a=b]]]]
U Spec, 148
150 ALL(n2):ALL(z2):ALL(next2):[Set(nat)
& 0 e nat
& ALL(a):[a e nat => next(a) e nat]
& ALL(a):ALL(b):[a e nat & b e nat => [next(a)=next(b) => a=b]]
& ALL(a):[a e nat => ~next(a)=0]
& ALL(a):[Set(a) & ALL(b):[b e a => b e nat]
=> [0 e a & ALL(b):[b e a => next(b) e a]
=> ALL(b):[b e nat => b e a]]]
& Set(n2)
& z2 e n2
& ALL(a):[a e n2 => next2(a) e n2]
& ALL(a):ALL(b):[a e n2 & b e n2 => [next2(a)=next2(b) => a=b]]
& ALL(a):[a e n2 => ~next2(a)=z2]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n2]
=> [z2 e a & ALL(b):[b e a => next2(b) e a]
=> ALL(b):[b e n2 => b e a]]]
=> ALL(f1):[ALL(a):[a e nat => f1(a) e n2]
& f1(0)=z2
& ALL(a):[a e nat => f1(next(a))=next2(f1(a))]
=> ALL(a):[a e n2 => EXIST(b):[b e nat & f1(b)=a]]
& ALL(a):ALL(b):[a e nat & b e nat => [f1(a)=f1(b) => a=b]]]]
U Spec, 149
151 ALL(z2):ALL(next2):[Set(nat)
& 0 e nat
& ALL(a):[a e nat => next(a) e nat]
& ALL(a):ALL(b):[a e nat & b e nat => [next(a)=next(b) => a=b]]
& ALL(a):[a e nat => ~next(a)=0]
& ALL(a):[Set(a) & ALL(b):[b e a => b e nat]
=> [0 e a & ALL(b):[b e a => next(b) e a]
=> ALL(b):[b e nat => b e a]]]
& Set(n)
& z2 e n
& ALL(a):[a e n => next2(a) e n]
& ALL(a):ALL(b):[a e n & b e n => [next2(a)=next2(b) => a=b]]
& ALL(a):[a e n => ~next2(a)=z2]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [z2 e a & ALL(b):[b e a => next2(b) e a]
=> ALL(b):[b e n => b e a]]]
=> ALL(f1):[ALL(a):[a e nat => f1(a) e n]
& f1(0)=z2
& ALL(a):[a e nat => f1(next(a))=next2(f1(a))]
=> ALL(a):[a e n => EXIST(b):[b e nat & f1(b)=a]]
& ALL(a):ALL(b):[a e nat & b e nat => [f1(a)=f1(b) => a=b]]]]
U Spec, 150
152 ALL(next2):[Set(nat)
& 0 e nat
& ALL(a):[a e nat => next(a) e nat]
& ALL(a):ALL(b):[a e nat & b e nat => [next(a)=next(b) => a=b]]
& ALL(a):[a e nat => ~next(a)=0]
& ALL(a):[Set(a) & ALL(b):[b e a => b e nat]
=> [0 e a & ALL(b):[b e a => next(b) e a]
=> ALL(b):[b e nat => b e a]]]
& Set(n)
& n0 e n
& ALL(a):[a e n => next2(a) e n]
& ALL(a):ALL(b):[a e n & b e n => [next2(a)=next2(b) => a=b]]
& ALL(a):[a e n => ~next2(a)=n0]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [n0 e a & ALL(b):[b e a => next2(b) e a]
=> ALL(b):[b e n => b e a]]]
=> ALL(f1):[ALL(a):[a e nat => f1(a) e n]
& f1(0)=n0
& ALL(a):[a e nat => f1(next(a))=next2(f1(a))]
=> ALL(a):[a e n => EXIST(b):[b e nat & f1(b)=a]]
& ALL(a):ALL(b):[a e nat & b e nat => [f1(a)=f1(b) => a=b]]]]
U Spec, 151
153 Set(nat)
& 0 e nat
& ALL(a):[a e nat => next(a) e nat]
& ALL(a):ALL(b):[a e nat & b e nat => [next(a)=next(b) => a=b]]
& ALL(a):[a e nat => ~next(a)=0]
& ALL(a):[Set(a) & ALL(b):[b e a => b e nat]
=> [0 e a & ALL(b):[b e a => next(b) e a]
=> ALL(b):[b e nat => b e a]]]
& Set(n)
& n0 e n
& ALL(a):[a e n => f(a) e n]
& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]
& ALL(a):[a e n => ~f(a)=n0]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [n0 e a & ALL(b):[b e a => f(b) e a]
=> ALL(b):[b e n => b e a]]]
=> ALL(f1):[ALL(a):[a e nat => f1(a) e n]
& f1(0)=n0
& ALL(a):[a e nat => f1(next(a))=f(f1(a))]
=> ALL(a):[a e n => EXIST(b):[b e nat & f1(b)=a]]
& ALL(a):ALL(b):[a e nat & b e nat => [f1(a)=f1(b) => a=b]]]
U Spec, 152
154 Set(nat)
& 0 e nat
& ALL(b):[b e nat => next(b) e nat]
& ALL(b):ALL(c):[b e nat & c e nat => [next(b)=next(c) => b=c]]
& ALL(b):[b e nat => ~next(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e nat]
=> [0 e b
& ALL(c):[c e b => next(c) e b]
=> ALL(c):[c e nat => c e b]]]
& Set(n)
Join, 1, 35
155 Set(nat)
& 0 e nat
& ALL(b):[b e nat => next(b) e nat]
& ALL(b):ALL(c):[b e nat & c e nat => [next(b)=next(c) => b=c]]
& ALL(b):[b e nat => ~next(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e nat]
=> [0 e b
& ALL(c):[c e b => next(c) e b]
=> ALL(c):[c e nat => c e b]]]
& Set(n)
& n0 e n
Join, 154, 54
156 Set(nat)
& 0 e nat
& ALL(b):[b e nat => next(b) e nat]
& ALL(b):ALL(c):[b e nat & c e nat => [next(b)=next(c) => b=c]]
& ALL(b):[b e nat => ~next(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e nat]
=> [0 e b
& ALL(c):[c e b => next(c) e b]
=> ALL(c):[c e nat => c e b]]]
& Set(n)
& n0 e n
& ALL(a):[a e n => f(a) e n]
Join, 155, 81
157 Set(nat)
& 0 e nat
& ALL(b):[b e nat => next(b) e nat]
& ALL(b):ALL(c):[b e nat & c e nat => [next(b)=next(c) => b=c]]
& ALL(b):[b e nat => ~next(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e nat]
=> [0 e b
& ALL(c):[c e b => next(c) e b]
=> ALL(c):[c e nat => c e b]]]
& Set(n)
& n0 e n
& ALL(a):[a e n => f(a) e n]
& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]
Join, 156, 96
158 Set(nat)
& 0 e nat
& ALL(b):[b e nat => next(b) e nat]
& ALL(b):ALL(c):[b e nat & c e nat => [next(b)=next(c) => b=c]]
& ALL(b):[b e nat => ~next(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e nat]
=> [0 e b
& ALL(c):[c e b => next(c) e b]
=> ALL(c):[c e nat => c e b]]]
& Set(n)
& n0 e n
& ALL(a):[a e n => f(a) e n]
& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]
& ALL(a):[a e n => ~f(a)=n0]
Join, 157, 102
159 Set(nat)
& 0 e nat
& ALL(b):[b e nat => next(b) e nat]
& ALL(b):ALL(c):[b e nat & c e nat => [next(b)=next(c) => b=c]]
& ALL(b):[b e nat => ~next(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e nat]
=> [0 e b
& ALL(c):[c e b => next(c) e b]
=> ALL(c):[c e nat => c e b]]]
& Set(n)
& n0 e n
& ALL(a):[a e n => f(a) e n]
& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]
& ALL(a):[a e n => ~f(a)=n0]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [n0 e a & ALL(b):[b e a => f(b) e a]
=> ALL(b):[b e n => b e a]]]
Join, 158, 129
160 ALL(f1):[ALL(a):[a e nat => f1(a) e n]
& f1(0)=n0
& ALL(a):[a e nat => f1(next(a))=f(f1(a))]
=> ALL(a):[a e n => EXIST(b):[b e nat & f1(b)=a]]
& ALL(a):ALL(b):[a e nat & b e nat => [f1(a)=f1(b) => a=b]]]
Detach, 153, 159
161 ALL(a):[a e nat => g(a) e n]
& g(0)=n0
& ALL(a):[a e nat => g(next(a))=f(g(a))]
=> ALL(a):[a e n => EXIST(b):[b e nat & g(b)=a]]
& ALL(a):ALL(b):[a e nat & b e nat => [g(a)=g(b) => a=b]]
U Spec, 160
162 ALL(a):[a e nat => g(a) e n] & g(0)=n0
Join, 144, 145
163 ALL(a):[a e nat => g(a) e n] & g(0)=n0
& ALL(a):[a e nat => g(next(a))=f(g(a))]
Join, 162, 146
164 ALL(a):[a e n => EXIST(b):[b e nat & g(b)=a]]
& ALL(a):ALL(b):[a e nat & b e nat => [g(a)=g(b) => a=b]]
Detach, 161, 163
g is surjective
165 ALL(a):[a e n => EXIST(b):[b e nat & g(b)=a]]
Split, 164
g is injective
166 ALL(a):ALL(b):[a e nat & b e nat => [g(a)=g(b) => a=b]]
Split, 164
Prove: ALL(a):[a e nat => g(a) e s]
Suppose...
167 x e nat
Premise
168 x e nat => g(x) e n
U Spec, 144
169 g(x) e n
Detach, 168, 167
170 g(x) e n => g(x) e s
U Spec, 44
171 g(x) e s
Detach, 170, 169
As Required:
172 ALL(a):[a e nat => g(a) e s]
4 Conclusion, 167
173 ALL(a):[a e nat => g(a) e s]
& ALL(a):ALL(b):[a e nat & b e nat => [g(a)=g(b) => a=b]]
Join, 172, 166
174 EXIST(f):[ALL(a):[a e nat => f(a) e s]
& ALL(a):ALL(b):[a e nat & b e nat => [f(a)=f(b) => a=b]]]
E Gen, 173
175 InfiniteB(s)
Detach, 26, 174
As Required:
176 InfiniteA(s) => InfiniteB(s)
4 Conclusion, 14
'<='
Prove: InfiniteB(s) => InfiniteA(s)
Suppose...
177 InfiniteB(s)
Premise
Apply definition of InfiniteB
178 Set(s) => [InfiniteB(s)
<=> EXIST(f):[ALL(b):[b e nat => f(b) e s]
& ALL(b):ALL(c):[b e nat & c e nat => [f(b)=f(c) => b=c]]]]
U Spec, 9
179 InfiniteB(s)
<=> EXIST(f):[ALL(b):[b e nat => f(b) e s]
& ALL(b):ALL(c):[b e nat & c e nat => [f(b)=f(c) => b=c]]]
Detach, 178, 13
180 [InfiniteB(s) => EXIST(f):[ALL(b):[b e nat => f(b) e s]
& ALL(b):ALL(c):[b e nat & c e nat => [f(b)=f(c) => b=c]]]]
& [EXIST(f):[ALL(b):[b e nat => f(b) e s]
& ALL(b):ALL(c):[b e nat & c e nat => [f(b)=f(c) => b=c]]] => InfiniteB(s)]
Iff-And, 179
181 InfiniteB(s) => EXIST(f):[ALL(b):[b e nat => f(b) e s]
& ALL(b):ALL(c):[b e nat & c e nat => [f(b)=f(c) => b=c]]]
Split, 180
182 EXIST(f):[ALL(b):[b e nat => f(b) e s]
& ALL(b):ALL(c):[b e nat & c e nat => [f(b)=f(c) => b=c]]] => InfiniteB(s)
Split, 180
183 EXIST(f):[ALL(b):[b e nat => f(b) e s]
& ALL(b):ALL(c):[b e nat & c e nat => [f(b)=f(c) => b=c]]]
Detach, 181, 177
184 ALL(b):[b e nat => h(b) e s]
& ALL(b):ALL(c):[b e nat & c e nat => [h(b)=h(c) => b=c]]
E Spec, 183
Define: h
*********
h is an injective mapping from nat to s.
185 ALL(b):[b e nat => h(b) e s]
Split, 184
186 ALL(b):ALL(c):[b e nat & c e nat => [h(b)=h(c) => b=c]]
Split, 184
187 Set(s) => [InfiniteA(s)
<=> EXIST(f):[ALL(b):[b e s => f(b) e s]
& ALL(b):ALL(c):[b e s & c e s => [f(b)=f(c) => b=c]]
& EXIST(b):[b e s & ALL(c):[c e s => ~f(c)=b]]]]
U Spec, 8
Apply definition of InfiniteA
188 InfiniteA(s)
<=> EXIST(f):[ALL(b):[b e s => f(b) e s]
& ALL(b):ALL(c):[b e s & c e s => [f(b)=f(c) => b=c]]
& EXIST(b):[b e s & ALL(c):[c e s => ~f(c)=b]]]
Detach, 187, 13
189 [InfiniteA(s) => EXIST(f):[ALL(b):[b e s => f(b) e s]
& ALL(b):ALL(c):[b e s & c e s => [f(b)=f(c) => b=c]]
& EXIST(b):[b e s & ALL(c):[c e s => ~f(c)=b]]]]
& [EXIST(f):[ALL(b):[b e s => f(b) e s]
& ALL(b):ALL(c):[b e s & c e s => [f(b)=f(c) => b=c]]
& EXIST(b):[b e s & ALL(c):[c e s => ~f(c)=b]]] => InfiniteA(s)]
Iff-And, 188
190 InfiniteA(s) => EXIST(f):[ALL(b):[b e s => f(b) e s]
& ALL(b):ALL(c):[b e s & c e s => [f(b)=f(c) => b=c]]
& EXIST(b):[b e s & ALL(c):[c e s => ~f(c)=b]]]
Split, 189
Sufficient: InfiniteA(s)
191 EXIST(f):[ALL(b):[b e s => f(b) e s]
& ALL(b):ALL(c):[b e s & c e s => [f(b)=f(c) => b=c]]
& EXIST(b):[b e s & ALL(c):[c e s => ~f(c)=b]]] => InfiniteA(s)
Split, 189
192 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e s & EXIST(b):[b e nat & h(b)=a]]]
Subset, 13
193 Set(t) & ALL(a):[a e t <=> a e s & EXIST(b):[b e nat & h(b)=a]]
E Spec, 192
Define: t
*********
The range of h
194 Set(t)
Split, 193
195 ALL(a):[a e t <=> a e s & EXIST(b):[b e nat & h(b)=a]]
Split, 193
Apply definition of InfiniteA
196 Set(t) => [InfiniteA(t)
<=> EXIST(f):[ALL(b):[b e t => f(b) e t]
& ALL(b):ALL(c):[b e t & c e t => [f(b)=f(c) => b=c]]
& EXIST(b):[b e t & ALL(c):[c e t => ~f(c)=b]]]]
U Spec, 8
197 InfiniteA(t)
<=> EXIST(f):[ALL(b):[b e t => f(b) e t]
& ALL(b):ALL(c):[b e t & c e t => [f(b)=f(c) => b=c]]
& EXIST(b):[b e t & ALL(c):[c e t => ~f(c)=b]]]
Detach, 196, 194
198 [InfiniteA(t) => EXIST(f):[ALL(b):[b e t => f(b) e t]
& ALL(b):ALL(c):[b e t & c e t => [f(b)=f(c) => b=c]]
& EXIST(b):[b e t & ALL(c):[c e t => ~f(c)=b]]]]
& [EXIST(f):[ALL(b):[b e t => f(b) e t]
& ALL(b):ALL(c):[b e t & c e t => [f(b)=f(c) => b=c]]
& EXIST(b):[b e t & ALL(c):[c e t => ~f(c)=b]]] => InfiniteA(t)]
Iff-And, 197
199 InfiniteA(t) => EXIST(f):[ALL(b):[b e t => f(b) e t]
& ALL(b):ALL(c):[b e t & c e t => [f(b)=f(c) => b=c]]
& EXIST(b):[b e t & ALL(c):[c e t => ~f(c)=b]]]
Split, 198
Sufficient: InfiniteA(t)
200 EXIST(f):[ALL(b):[b e t => f(b) e t]
& ALL(b):ALL(c):[b e t & c e t => [f(b)=f(c) => b=c]]
& EXIST(b):[b e t & ALL(c):[c e t => ~f(c)=b]]] => InfiniteA(t)
Split, 198
201 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
202 ALL(a2):[Set(t) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e t & c2 e a2]]]
U Spec, 201
203 Set(t) & Set(t) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e t & c2 e t]]
U Spec, 202
204 Set(t) & Set(t)
Join, 194, 194
205 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e t & c2 e t]]
Detach, 203, 204
206 Set'(t2) & ALL(c1):ALL(c2):[(c1,c2) e t2 <=> c1 e t & c2 e t]
E Spec, 205
Define: t2
**********
The Cartesian Product of t with itself
207 Set'(t2)
Split, 206
208 ALL(c1):ALL(c2):[(c1,c2) e t2 <=> c1 e t & c2 e t]
Split, 206
Apply Subset Axiom
209 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & a=h(c) & b=h(d)]]]
Subset, 207
210 Set'(next') & ALL(a):ALL(b):[(a,b) e next' <=> (a,b) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & a=h(c) & b=h(d)]]
E Spec, 209
Define: next'
*************
Analogous to next, the successor function on nat
211 Set'(next')
Split, 210
212 ALL(a):ALL(b):[(a,b) e next' <=> (a,b) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & a=h(c) & b=h(d)]]
Split, 210
Apply Function Axiom
213 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
214 ALL(a):ALL(b):[ALL(c):ALL(d):[(c,d) e next' => c e a & d e b]
& ALL(c):[c e a => EXIST(d):[d e b & (c,d) e next']]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e next' & (c,d2) e next' => d1=d2]
=> ALL(c):ALL(d):[d=next'(c) <=> (c,d) e next']]
U Spec, 213
215 ALL(b):[ALL(c):ALL(d):[(c,d) e next' => c e t & d e b]
& ALL(c):[c e t => EXIST(d):[d e b & (c,d) e next']]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e next' & (c,d2) e next' => d1=d2]
=> ALL(c):ALL(d):[d=next'(c) <=> (c,d) e next']]
U Spec, 214
Sufficient: For functionality of next'
216 ALL(c):ALL(d):[(c,d) e next' => c e t & d e t]
& ALL(c):[c e t => EXIST(d):[d e t & (c,d) e next']]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e next' & (c,d2) e next' => d1=d2]
=> ALL(c):ALL(d):[d=next'(c) <=> (c,d) e next']
U Spec, 215
Prove: ALL(c):ALL(d):[(c,d) e next' => c e t & d e t]
Suppose...
217 (x,y) e next'
Premise
218 ALL(b):[(x,b) e next' <=> (x,b) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & b=h(d)]]
U Spec, 212
219 (x,y) e next' <=> (x,y) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & y=h(d)]
U Spec, 218
220 [(x,y) e next' => (x,y) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & y=h(d)]]
& [(x,y) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & y=h(d)] => (x,y) e next']
Iff-And, 219
221 (x,y) e next' => (x,y) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & y=h(d)]
Split, 220
222 (x,y) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & y=h(d)] => (x,y) e next'
Split, 220
223 (x,y) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & y=h(d)]
Detach, 221, 217
224 (x,y) e t2
Split, 223
225 EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & y=h(d)]
Split, 223
226 ALL(c2):[(x,c2) e t2 <=> x e t & c2 e t]
U Spec, 208
227 (x,y) e t2 <=> x e t & y e t
U Spec, 226
228 [(x,y) e t2 => x e t & y e t]
& [x e t & y e t => (x,y) e t2]
Iff-And, 227
229 (x,y) e t2 => x e t & y e t
Split, 228
230 x e t & y e t => (x,y) e t2
Split, 228
231 x e t & y e t
Detach, 229, 224
Functionality, Part 1
232 ALL(c):ALL(d):[(c,d) e next' => c e t & d e t]
4 Conclusion, 217
Prove: ALL(c):[c e t => EXIST(d):[d e t & (c,d) e next']]
Suppose...
233 x e t
Premise
234 x e t <=> x e s & EXIST(b):[b e nat & h(b)=x]
U Spec, 195
235 [x e t => x e s & EXIST(b):[b e nat & h(b)=x]]
& [x e s & EXIST(b):[b e nat & h(b)=x] => x e t]
Iff-And, 234
236 x e t => x e s & EXIST(b):[b e nat & h(b)=x]
Split, 235
237 x e s & EXIST(b):[b e nat & h(b)=x] => x e t
Split, 235
238 x e s & EXIST(b):[b e nat & h(b)=x]
Detach, 236, 233
239 x e s
Split, 238
240 EXIST(b):[b e nat & h(b)=x]
Split, 238
241 x' e nat & h(x')=x
E Spec, 240
Define: x'
The pre-image of x under h
242 x' e nat
Split, 241
243 h(x')=x
Split, 241
244 x' e nat => next(x') e nat
U Spec, 4
245 next(x') e nat
Detach, 244, 242
246 next(x') e nat => h(next(x')) e s
U Spec, 185
247 h(next(x')) e s
Detach, 246, 245
248 h(next(x')) e t <=> h(next(x')) e s & EXIST(b):[b e nat & h(b)=h(next(x'))]
U Spec, 195
249 [h(next(x')) e t => h(next(x')) e s & EXIST(b):[b e nat & h(b)=h(next(x'))]]
& [h(next(x')) e s & EXIST(b):[b e nat & h(b)=h(next(x'))] => h(next(x')) e t]
Iff-And, 248
250 h(next(x')) e t => h(next(x')) e s & EXIST(b):[b e nat & h(b)=h(next(x'))]
Split, 249
Sufficient: h(next(x')) e t
251 h(next(x')) e s & EXIST(b):[b e nat & h(b)=h(next(x'))] => h(next(x')) e t
Split, 249
252 h(next(x'))=h(next(x'))
Reflex
253 next(x') e nat & h(next(x'))=h(next(x'))
Join, 245, 252
254 EXIST(b):[b e nat & h(b)=h(next(x'))]
E Gen, 253
255 h(next(x')) e s
& EXIST(b):[b e nat & h(b)=h(next(x'))]
Join, 247, 254
256 h(next(x')) e t
Detach, 251, 255
257 ALL(b):[(x,b) e next' <=> (x,b) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & b=h(d)]]
U Spec, 212
258 (x,h(next(x'))) e next' <=> (x,h(next(x'))) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & h(next(x'))=h(d)]
U Spec, 257
259 [(x,h(next(x'))) e next' => (x,h(next(x'))) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & h(next(x'))=h(d)]]
& [(x,h(next(x'))) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & h(next(x'))=h(d)] => (x,h(next(x'))) e next']
Iff-And, 258
260 (x,h(next(x'))) e next' => (x,h(next(x'))) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & h(next(x'))=h(d)]
Split, 259
Sufficient: (x,h(next(x'))) e next'
261 (x,h(next(x'))) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & h(next(x'))=h(d)] => (x,h(next(x'))) e next'
Split, 259
262 ALL(c2):[(x,c2) e t2 <=> x e t & c2 e t]
U Spec, 208
263 (x,h(next(x'))) e t2 <=> x e t & h(next(x')) e t
U Spec, 262
264 [(x,h(next(x'))) e t2 => x e t & h(next(x')) e t]
& [x e t & h(next(x')) e t => (x,h(next(x'))) e t2]
Iff-And, 263
265 (x,h(next(x'))) e t2 => x e t & h(next(x')) e t
Split, 264
266 x e t & h(next(x')) e t => (x,h(next(x'))) e t2
Split, 264
267 x e t & h(next(x')) e t
Join, 233, 256
268 (x,h(next(x'))) e t2
Detach, 266, 267
269 next(x')=next(x')
Reflex
270 h(next(x'))=h(next(x'))
Reflex
271 x=h(x')
Sym, 243
272 x' e nat & next(x') e nat
Join, 242, 245
273 x' e nat & next(x') e nat & next(x')=next(x')
Join, 272, 269
274 x' e nat & next(x') e nat & next(x')=next(x')
& x=h(x')
Join, 273, 271
275 x' e nat & next(x') e nat & next(x')=next(x')
& x=h(x')
& h(next(x'))=h(next(x'))
Join, 274, 270
276 EXIST(d):[x' e nat & d e nat & next(x')=d
& x=h(x')
& h(next(x'))=h(d)]
E Gen, 275
277 EXIST(s):EXIST(d):[s e nat & d e nat & next(s)=d
& x=h(s)
& h(next(x'))=h(d)]
E Gen, 276
278 (x,h(next(x'))) e t2
& EXIST(s):EXIST(d):[s e nat & d e nat & next(s)=d
& x=h(s)
& h(next(x'))=h(d)]
Join, 268, 277
279 (x,h(next(x'))) e next'
Detach, 261, 278
280 h(next(x')) e t & (x,h(next(x'))) e next'
Join, 256, 279
281 EXIST(d):[d e t & (x,d) e next']
E Gen, 280
Functionality, Part 2
282 ALL(c):[c e t => EXIST(d):[d e t & (c,d) e next']]
4 Conclusion, 233
Prove: ALL(c):ALL(d1):ALL(d2):[(c,d1) e next' & (c,d2) e next' => d1=d2]
Suppose...
283 (x,y1) e next' & (x,y2) e next'
Premise
284 (x,y1) e next'
Split, 283
285 (x,y2) e next'
Split, 283
286 ALL(b):[(x,b) e next' <=> (x,b) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & b=h(d)]]
U Spec, 212
287 (x,y1) e next' <=> (x,y1) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & y1=h(d)]
U Spec, 286
288 [(x,y1) e next' => (x,y1) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & y1=h(d)]]
& [(x,y1) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & y1=h(d)] => (x,y1) e next']
Iff-And, 287
289 (x,y1) e next' => (x,y1) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & y1=h(d)]
Split, 288
290 (x,y1) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & y1=h(d)] => (x,y1) e next'
Split, 288
291 (x,y1) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & y1=h(d)]
Detach, 289, 284
292 (x,y1) e t2
Split, 291
293 EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & y1=h(d)]
Split, 291
294 EXIST(d):[u e nat & d e nat & next(u)=d & x=h(u) & y1=h(d)]
E Spec, 293
295 u e nat & v e nat & next(u)=v & x=h(u) & y1=h(v)
E Spec, 294
Define: u, v
296 u e nat
Split, 295
297 v e nat
Split, 295
298 next(u)=v
Split, 295
299 x=h(u)
Split, 295
300 y1=h(v)
Split, 295
301 (x,y2) e next' <=> (x,y2) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & y2=h(d)]
U Spec, 286
302 [(x,y2) e next' => (x,y2) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & y2=h(d)]]
& [(x,y2) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & y2=h(d)] => (x,y2) e next']
Iff-And, 301
303 (x,y2) e next' => (x,y2) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & y2=h(d)]
Split, 302
304 (x,y2) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & y2=h(d)] => (x,y2) e next'
Split, 302
305 (x,y2) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & y2=h(d)]
Detach, 303, 285
306 (x,y2) e t2
Split, 305
307 y1=h(next(u))
Substitute, 298, 300
308 EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & y2=h(d)]
Split, 305
309 EXIST(d):[w e nat & d e nat & next(w)=d & x=h(w) & y2=h(d)]
E Spec, 308
310 w e nat & z e nat & next(w)=z & x=h(w) & y2=h(z)
E Spec, 309
Define: w, z
311 w e nat
Split, 310
312 z e nat
Split, 310
313 next(w)=z
Split, 310
314 x=h(w)
Split, 310
315 y2=h(z)
Split, 310
316 y2=h(next(w))
Substitute, 313, 315
317 h(u)=h(w)
Substitute, 299, 314
318 ALL(c):[u e nat & c e nat => [h(u)=h(c) => u=c]]
U Spec, 186
319 u e nat & w e nat => [h(u)=h(w) => u=w]
U Spec, 318
320 u e nat & w e nat
Join, 296, 311
321 h(u)=h(w) => u=w
Detach, 319, 320
322 u=w
Detach, 321, 317
323 y2=h(next(u))
Substitute, 322, 316
324 y1=y2
Substitute, 323, 307
Functionality, Part 3
325 ALL(c):ALL(d1):ALL(d2):[(c,d1) e next' & (c,d2) e next' => d1=d2]
4 Conclusion, 283
326 ALL(c):ALL(d):[(c,d) e next' => c e t & d e t]
& ALL(c):[c e t => EXIST(d):[d e t & (c,d) e next']]
Join, 232, 282
327 ALL(c):ALL(d):[(c,d) e next' => c e t & d e t]
& ALL(c):[c e t => EXIST(d):[d e t & (c,d) e next']]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e next' & (c,d2) e next' => d1=d2]
Join, 326, 325
next' is a function
328 ALL(c):ALL(d):[d=next'(c) <=> (c,d) e next']
Detach, 216, 327
Prove: ALL(a):[a e t => next'(a) e t]
Suppose...
329 x e t
Premise
330 x e t => EXIST(d):[d e t & (x,d) e next']
U Spec, 282
331 EXIST(d):[d e t & (x,d) e next']
Detach, 330, 329
332 y e t & (x,y) e next'
E Spec, 331
333 y e t
Split, 332
334 (x,y) e next'
Split, 332
335 ALL(d):[d=next'(x) <=> (x,d) e next']
U Spec, 328
336 y=next'(x) <=> (x,y) e next'
U Spec, 335
337 [y=next'(x) => (x,y) e next']
& [(x,y) e next' => y=next'(x)]
Iff-And, 336
338 y=next'(x) => (x,y) e next'
Split, 337
339 (x,y) e next' => y=next'(x)
Split, 337
340 y=next'(x)
Detach, 339, 334
341 next'(x) e t
Substitute, 340, 333
As Required:
342 ALL(a):[a e t => next'(a) e t]
4 Conclusion, 329
Prove: ALL(b):[b e nat & h(b)=a => next'(a)=h(next(b))]]
Suppose...
343 x e t
Premise
Prove: ALL(b):[b e nat & h(b)=x => next'(x)=h(next(b))]
Suppose...
344 x' e nat & h(x')=x
Premise
345 x' e nat
Split, 344
346 h(x')=x
Split, 344
347 ALL(b):[(x,b) e next' <=> (x,b) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & b=h(d)]]
U Spec, 212
348 (x,h(next(x'))) e next' <=> (x,h(next(x'))) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & h(next(x'))=h(d)]
U Spec, 347
349 [(x,h(next(x'))) e next' => (x,h(next(x'))) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & h(next(x'))=h(d)]]
& [(x,h(next(x'))) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & h(next(x'))=h(d)] => (x,h(next(x'))) e next']
Iff-And, 348
350 (x,h(next(x'))) e next' => (x,h(next(x'))) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & h(next(x'))=h(d)]
Split, 349
Sufficient: (x,h(next(x'))) e next'
c=x', d=next(x')
351 (x,h(next(x'))) e t2 & EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d & x=h(c) & h(next(x'))=h(d)] => (x,h(next(x'))) e next'
Split, 349
352 ALL(c2):[(x,c2) e t2 <=> x e t & c2 e t]
U Spec, 208
353 (x,h(next(x'))) e t2 <=> x e t & h(next(x')) e t
U Spec, 352
354 [(x,h(next(x'))) e t2 => x e t & h(next(x')) e t]
& [x e t & h(next(x')) e t => (x,h(next(x'))) e t2]
Iff-And, 353
355 (x,h(next(x'))) e t2 => x e t & h(next(x')) e t
Split, 354
356 x e t & h(next(x')) e t => (x,h(next(x'))) e t2
Split, 354
357 x' e nat => next(x') e nat
U Spec, 4
358 next(x') e nat
Detach, 357, 345
359 next(x') e nat => h(next(x')) e s
U Spec, 185
360 h(next(x')) e s
Detach, 359, 358
361 h(next(x')) e t <=> h(next(x')) e s & EXIST(b):[b e nat & h(b)=h(next(x'))]
U Spec, 195
362 [h(next(x')) e t => h(next(x')) e s & EXIST(b):[b e nat & h(b)=h(next(x'))]]
& [h(next(x')) e s & EXIST(b):[b e nat & h(b)=h(next(x'))] => h(next(x')) e t]
Iff-And, 361
363 h(next(x')) e t => h(next(x')) e s & EXIST(b):[b e nat & h(b)=h(next(x'))]
Split, 362
364 h(next(x')) e s & EXIST(b):[b e nat & h(b)=h(next(x'))] => h(next(x')) e t
Split, 362
365 h(next(x'))=h(next(x'))
Reflex
366 next(x') e nat & h(next(x'))=h(next(x'))
Join, 358, 365
367 EXIST(b):[b e nat & h(b)=h(next(x'))]
E Gen, 366
368 h(next(x')) e s
& EXIST(b):[b e nat & h(b)=h(next(x'))]
Join, 360, 367
369 h(next(x')) e t
Detach, 364, 368
370 x e t & h(next(x')) e t
Join, 343, 369
371 (x,h(next(x'))) e t2
Detach, 356, 370
372 next(x')=next(x')
Reflex
373 x=h(x')
Sym, 346
374 h(next(x'))=h(next(x'))
Reflex
375 x' e nat & next(x') e nat
Join, 345, 358
376 x' e nat & next(x') e nat & next(x')=next(x')
Join, 375, 372
377 x' e nat & next(x') e nat & next(x')=next(x')
& x=h(x')
Join, 376, 373
378 x' e nat & next(x') e nat & next(x')=next(x')
& x=h(x')
& h(next(x'))=h(next(x'))
Join, 377, 374
379 EXIST(d):[x' e nat & d e nat & next(x')=d
& x=h(x')
& h(next(x'))=h(d)]
E Gen, 378
380 EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d
& x=h(c)
& h(next(x'))=h(d)]
E Gen, 379
381 (x,h(next(x'))) e t2
& EXIST(c):EXIST(d):[c e nat & d e nat & next(c)=d
& x=h(c)
& h(next(x'))=h(d)]
Join, 371, 380
382 (x,h(next(x'))) e next'
Detach, 351, 381
383 ALL(d):[d=next'(x) <=> (x,d) e next']
U Spec, 328
384 h(next(x'))=next'(x) <=> (x,h(next(x'))) e next'
U Spec, 383
385 [h(next(x'))=next'(x) => (x,h(next(x'))) e next']
& [(x,h(next(x'))) e next' => h(next(x'))=next'(x)]
Iff-And, 384
386 h(next(x'))=next'(x) => (x,h(next(x'))) e next'
Split, 385
387 (x,h(next(x'))) e next' => h(next(x'))=next'(x)
Split, 385
388 h(next(x'))=next'(x)
Detach, 387, 382
389 next'(x)=h(next(x'))
Sym, 388
As Required:
390 ALL(b):[b e nat & h(b)=x => next'(x)=h(next(b))]
4 Conclusion, 344
As Required:
391 ALL(a):[a e t
=> ALL(b):[b e nat & h(b)=a => next'(a)=h(next(b))]]
4 Conclusion, 343
Prove: ALL(b):ALL(c):[b e t & c e t => [next'(b)=next'(c) => b=c]]
Suppose...
392 x e t & y e t
Premise
393 x e t
Split, 392
394 y e t
Split, 392
395 x e t <=> x e s & EXIST(b):[b e nat & h(b)=x]
U Spec, 195
396 [x e t => x e s & EXIST(b):[b e nat & h(b)=x]]
& [x e s & EXIST(b):[b e nat & h(b)=x] => x e t]
Iff-And, 395
397 x e t => x e s & EXIST(b):[b e nat & h(b)=x]
Split, 396
398 x e s & EXIST(b):[b e nat & h(b)=x] => x e t
Split, 396
399 x e s & EXIST(b):[b e nat & h(b)=x]
Detach, 397, 393
400 x e s
Split, 399
401 EXIST(b):[b e nat & h(b)=x]
Split, 399
402 x' e nat & h(x')=x
E Spec, 401
403 x' e nat
Split, 402
404 h(x')=x
Split, 402
405 y e t <=> y e s & EXIST(b):[b e nat & h(b)=y]
U Spec, 195
406 [y e t => y e s & EXIST(b):[b e nat & h(b)=y]]
& [y e s & EXIST(b):[b e nat & h(b)=y] => y e t]
Iff-And, 405
407 y e t => y e s & EXIST(b):[b e nat & h(b)=y]
Split, 406
408 y e s & EXIST(b):[b e nat & h(b)=y] => y e t
Split, 406
409 y e s & EXIST(b):[b e nat & h(b)=y]
Detach, 407, 394
410 y e s
Split, 409
411 EXIST(b):[b e nat & h(b)=y]
Split, 409
412 y' e nat & h(y')=y
E Spec, 411
413 y' e nat
Split, 412
414 h(y')=y
Split, 412
Suppose...
415 next'(x)=next'(y)
Premise
416 x e t
=> ALL(b):[b e nat & h(b)=x => next'(x)=h(next(b))]
U Spec, 391
417 ALL(b):[b e nat & h(b)=x => next'(x)=h(next(b))]
Detach, 416, 393
418 x' e nat & h(x')=x => next'(x)=h(next(x'))
U Spec, 417
419 x' e nat & h(x')=x
Join, 403, 404
420 next'(x)=h(next(x'))
Detach, 418, 419
421 y e t
=> ALL(b):[b e nat & h(b)=y => next'(y)=h(next(b))]
U Spec, 391
422 ALL(b):[b e nat & h(b)=y => next'(y)=h(next(b))]
Detach, 421, 394
423 y' e nat & h(y')=y => next'(y)=h(next(y'))
U Spec, 422
424 y' e nat & h(y')=y
Join, 413, 414
425 next'(y)=h(next(y'))
Detach, 423, 424
426 h(next(x'))=next'(y)
Substitute, 420, 415
427 h(next(x'))=h(next(y'))
Substitute, 425, 426
428 ALL(c):[next(x') e nat & c e nat => [h(next(x'))=h(c) => next(x')=c]]
U Spec, 186
429 next(x') e nat & next(y') e nat => [h(next(x'))=h(next(y')) => next(x')=next(y')]
U Spec, 428
430 x' e nat => next(x') e nat
U Spec, 4
431 next(x') e nat
Detach, 430, 403
432 y' e nat => next(y') e nat
U Spec, 4
433 next(y') e nat
Detach, 432, 413
434 next(x') e nat & next(y') e nat
Join, 431, 433
435 h(next(x'))=h(next(y')) => next(x')=next(y')
Detach, 429, 434
436 next(x')=next(y')
Detach, 435, 427
437 ALL(c):[x' e nat & c e nat => [next(x')=next(c) => x'=c]]
U Spec, 5
438 x' e nat & y' e nat => [next(x')=next(y') => x'=y']
U Spec, 437
439 x' e nat & y' e nat
Join, 403, 413
440 next(x')=next(y') => x'=y'
Detach, 438, 439
441 x'=y'
Detach, 440, 436
442 h(x')=y
Substitute, 441, 414
443 x=y
Substitute, 404, 442
444 next'(x)=next'(y) => x=y
4 Conclusion, 415
As Required:
445 ALL(b):ALL(c):[b e t & c e t => [next'(b)=next'(c) => b=c]]
4 Conclusion, 392
Prove: ~EXIST(a):[a e t & next'(a)=h(0)]
Suppose to the contrary...
446 x e t & next'(x)=h(0)
Premise
447 x e t
Split, 446
448 next'(x)=h(0)
Split, 446
449 x e t <=> x e s & EXIST(b):[b e nat & h(b)=x]
U Spec, 195
450 [x e t => x e s & EXIST(b):[b e nat & h(b)=x]]
& [x e s & EXIST(b):[b e nat & h(b)=x] => x e t]
Iff-And, 449
451 x e t => x e s & EXIST(b):[b e nat & h(b)=x]
Split, 450
452 x e s & EXIST(b):[b e nat & h(b)=x] => x e t
Split, 450
453 x e s & EXIST(b):[b e nat & h(b)=x]
Detach, 451, 447
454 x e s
Split, 453
455 EXIST(b):[b e nat & h(b)=x]
Split, 453
456 x' e nat & h(x')=x
E Spec, 455
457 x' e nat
Split, 456
458 h(x')=x
Split, 456
459 x e t
=> ALL(b):[b e nat & h(b)=x => next'(x)=h(next(b))]
U Spec, 391
460 ALL(b):[b e nat & h(b)=x => next'(x)=h(next(b))]
Detach, 459, 447
461 x' e nat & h(x')=x => next'(x)=h(next(x'))
U Spec, 460
462 x' e nat & h(x')=x
Join, 457, 458
463 next'(x)=h(next(x'))
Detach, 461, 462
464 h(0)=h(next(x'))
Substitute, 448, 463
465 ALL(c):[0 e nat & c e nat => [h(0)=h(c) => 0=c]]
U Spec, 186
466 0 e nat & next(x') e nat => [h(0)=h(next(x')) => 0=next(x')]
U Spec, 465
467 x' e nat => next(x') e nat
U Spec, 4
468 next(x') e nat
Detach, 467, 457
469 0 e nat & next(x') e nat
Join, 3, 468
470 h(0)=h(next(x')) => 0=next(x')
Detach, 466, 469
471 0=next(x')
Detach, 470, 464
472 x' e nat => ~next(x')=0
U Spec, 6
473 ~next(x')=0
Detach, 472, 457
474 next(x')=0
Sym, 471
475 next(x')=0 & ~next(x')=0
Join, 474, 473
As Required:
476 ~EXIST(a):[a e t & next'(a)=h(0)]
4 Conclusion, 446
477 ~~ALL(a):~[a e t & next'(a)=h(0)]
Quant, 476
478 ALL(a):~[a e t & next'(a)=h(0)]
Rem DNeg, 477
479 ALL(a):~~[a e t => ~next'(a)=h(0)]
Imply-And, 478
480 ALL(a):[a e t => ~next'(a)=h(0)]
Rem DNeg, 479
481 0 e nat => h(0) e s
U Spec, 185
482 h(0) e s
Detach, 481, 3
Apply definition of t
483 h(0) e t <=> h(0) e s & EXIST(b):[b e nat & h(b)=h(0)]
U Spec, 195
484 [h(0) e t => h(0) e s & EXIST(b):[b e nat & h(b)=h(0)]]
& [h(0) e s & EXIST(b):[b e nat & h(b)=h(0)] => h(0) e t]
Iff-And, 483
485 h(0) e t => h(0) e s & EXIST(b):[b e nat & h(b)=h(0)]
Split, 484
486 h(0) e s & EXIST(b):[b e nat & h(b)=h(0)] => h(0) e t
Split, 484
487 h(0)=h(0)
Reflex
488 0 e nat & h(0)=h(0)
Join, 3, 487
489 EXIST(b):[b e nat & h(b)=h(0)]
E Gen, 488
490 h(0) e s & EXIST(b):[b e nat & h(b)=h(0)]
Join, 482, 489
491 h(0) e t
Detach, 486, 490
492 h(0) e t & ALL(a):[a e t => ~next'(a)=h(0)]
Join, 491, 480
493 EXIST(b):[b e t & ALL(a):[a e t => ~next'(a)=b]]
E Gen, 492
Joining results...
494 ALL(a):[a e t => next'(a) e t]
& ALL(b):ALL(c):[b e t & c e t => [next'(b)=next'(c) => b=c]]
Join, 342, 445
495 ALL(a):[a e t => next'(a) e t]
& ALL(b):ALL(c):[b e t & c e t => [next'(b)=next'(c) => b=c]]
& EXIST(b):[b e t & ALL(a):[a e t => ~next'(a)=b]]
Join, 494, 493
496 EXIST(f):[ALL(a):[a e t => f(a) e t]
& ALL(b):ALL(c):[b e t & c e t => [f(b)=f(c) => b=c]]
& EXIST(b):[b e t & ALL(a):[a e t => ~f(a)=b]]]
E Gen, 495
Prove: ALL(a):[a e t => a e s]
Suppose...
497 x e t
Premise
498 x e t <=> x e s & EXIST(b):[b e nat & h(b)=x]
U Spec, 195
499 [x e t => x e s & EXIST(b):[b e nat & h(b)=x]]
& [x e s & EXIST(b):[b e nat & h(b)=x] => x e t]
Iff-And, 498
500 x e t => x e s & EXIST(b):[b e nat & h(b)=x]
Split, 499
501 x e s & EXIST(b):[b e nat & h(b)=x] => x e t
Split, 499
502 x e s & EXIST(b):[b e nat & h(b)=x]
Detach, 500, 497
503 x e s
Split, 502
As Required: t is a subset of s
504 ALL(a):[a e t => a e s]
4 Conclusion, 497
505 InfiniteA(t)
Detach, 200, 496
Apply infinite subsets (previous result)
506 ALL(b):[Set(t) & Set(b) & ALL(c):[c e t => c e b]
=> [InfiniteA(t) => InfiniteA(b)]]
U Spec, 12
507 Set(t) & Set(s) & ALL(c):[c e t => c e s]
=> [InfiniteA(t) => InfiniteA(s)]
U Spec, 506
508 Set(t) & Set(s)
Join, 194, 13
509 Set(t) & Set(s) & ALL(a):[a e t => a e s]
Join, 508, 504
510 InfiniteA(t) => InfiniteA(s)
Detach, 507, 509
511 InfiniteA(s)
Detach, 510, 505
As Required:
512 InfiniteB(s) => InfiniteA(s)
4 Conclusion, 177
Joining results...
513 [InfiniteA(s) => InfiniteB(s)]
& [InfiniteB(s) => InfiniteA(s)]
Join, 176, 512
514 InfiniteA(s) <=> InfiniteB(s)
Iff-And, 513
As Required:
515 ALL(a):[Set(a) => [InfiniteA(a) <=> InfiniteB(a)]]
4 Conclusion, 13