THEOREM
*******
There exists the set of all fisons = {{0}, {0,1}, {0,1,2} ...} and a bijection f: n
--> fisons where n is the set
of natural numbers.
Formally:
EXIST(fisons):EXIST(f):[Set(fisons)
& ALL(a):[a e fisons
<=> Set(a) & ALL(b):[b e a => b e n]
& EXIST(b):[b
e n & ALL(c):[c e n => [c e a <=> c<=b]]]]
& ALL(a):[a e n => f(a) e fisons] (f(x) = {0, 1, 2,
... x})
& ALL(a):[a e fisons => EXIST(b):[b e n & f(b) e fisons]] (f is
surjective)
& ALL(a):ALL(b):[a
e n & b e n =>
[f(a)=f(b) => a=b]]] (f is
injective)
OUTLINE OF PROOF
****************
Lines
5-52 Construct the set of all fisons
53-64 Construct the set f
65-309 Prove f is a function mapping n to the set
of all fisons
310-328 Prove f is surjective
343-408 Prove f is injective
This machine-verified formal
proof was written with the aid of the author's DC Proof 2.0 proof-checker
available at
AXIOMS
******
1 Set(n)
Axiom
Define: <= on n
2 ALL(a):[a e n => a<=a]
Axiom
3 ALL(a):ALL(b):[a e n & b e n => [a<=b & b<=a =>
a=b]]
Axiom
Function Axiom (single
variable)
4 ALL(f):ALL(a):ALL(b):[Set'(f) &
Set(a) & Set(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):[c e a & d e b => [d=f(c) <=> (c,d) e f]]]]
Axiom
PROOF
*****
Construct the set of all fisons
Apply Power Set Axiom
5 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
6 Set(n) => EXIST(b):[Set(b)
&
ALL(c):[c e b <=>
Set(c) & ALL(d):[d e c => d e n]]]
U Spec, 5
7 EXIST(b):[Set(b)
&
ALL(c):[c e b <=>
Set(c) & ALL(d):[d e c => d e n]]]
Detach, 6, 1
Define: pn
Power set of n
8 Set(pn)
&
ALL(c):[c e pn <=> Set(c) & ALL(d):[d e c => d e n]]
E Spec, 7
9 Set(pn)
Split, 8
10 ALL(c):[c e pn <=> Set(c) & ALL(d):[d e c => d e n]]
Split, 8
Apply Subset Axiom
11 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e pn &
EXIST(b):[b e n & ALL(c):[c e n => [c e a <=> c<=b]]]]]
Subset, 9
Define: fisons
12 Set(fisons) & ALL(a):[a e fisons <=> a e pn &
EXIST(b):[b e n & ALL(c):[c e n => [c e a <=> c<=b]]]]
E Spec, 11
13 Set(fisons)
Split, 12
14 ALL(a):[a e fisons <=> a e pn & EXIST(b):[b e n & ALL(c):[c e n => [c e a <=> c<=b]]]]
Split, 12
Suppose...
15 x e fisons
Premise
16 x e fisons <=> x e pn & EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]]
U Spec, 14
17 [x e fisons => x e pn & EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]]]
&
[x e pn & EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]] => x e fisons]
Iff-And, 16
18 x e fisons => x e pn & EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]]
Split, 17
19 x e pn & EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]] => x e fisons
Split, 17
20 x e pn & EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]]
Detach, 18, 15
21 x e pn
Split, 20
22 EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]]
Split, 20
23 x e pn <=> Set(x) & ALL(d):[d e x => d e n]
U Spec, 10
24 [x e pn => Set(x) & ALL(d):[d e x => d e n]]
&
[Set(x) & ALL(d):[d e x => d e n] => x e pn]
Iff-And, 23
25 x e pn => Set(x) & ALL(d):[d e x => d e n]
Split, 24
26 Set(x) & ALL(d):[d e x => d e n] => x e pn
Split, 24
27 Set(x) & ALL(d):[d e x => d e n]
Detach, 25, 21
28 Set(x)
Split, 27
29 ALL(d):[d e x => d e n]
Split, 27
30 ALL(b):[b e x => b e n]
Rename, 29
31 Set(x) & ALL(b):[b e x => b e n]
Join, 28, 30
32 Set(x) & ALL(b):[b e x => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]]
Join, 31, 22
33 ALL(a):[a e fisons
=>
Set(a) & ALL(b):[b e a => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e a <=> c<=b]]]]
4 Conclusion, 15
Prove: ALL(a):[Set(a) & ALL(b):[b e a => b e n]
& EXIST(b):[b e n & ALL(c):[c e n => [c e a <=>
c<=b]]]
=> a e fisons]
Suppose...
34 Set(x) & ALL(b):[b e x => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]]
Premise
35 Set(x)
Split, 34
36 ALL(b):[b e x => b e n]
Split, 34
37 EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]]
Split, 34
38 x e fisons <=> x e pn & EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]]
U Spec, 14
39 [x e fisons => x e pn & EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]]]
&
[x e pn & EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]] => x e fisons]
Iff-And, 38
40 x e fisons => x e pn & EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]]
Split, 39
Sufficient: For x e fisons
41 x e pn & EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]] => x e fisons
Split, 39
42 x e pn <=> Set(x) & ALL(d):[d e x => d e n]
U Spec, 10
43 [x e pn => Set(x) & ALL(d):[d e x => d e n]]
&
[Set(x) & ALL(d):[d e x => d e n] => x e pn]
Iff-And, 42
44 x e pn => Set(x) & ALL(d):[d e x => d e n]
Split, 43
As Required:
45 Set(x) & ALL(d):[d e x => d e n] => x e pn
Split, 43
46 Set(x) & ALL(b):[b e x => b e n]
Join, 35, 36
47 x e pn
Detach, 45, 46
48 x e pn
&
EXIST(b):[b e n & ALL(c):[c e n => [c e x <=> c<=b]]]
Join, 47, 37
49 x e fisons
Detach, 41, 48
As Required:
50 ALL(a):[Set(a) & ALL(b):[b e a => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e a <=> c<=b]]]
=>
a e fisons]
4 Conclusion, 34
51 ALL(a):[[a e fisons
=>
Set(a) & ALL(b):[b e a => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e a <=> c<=b]]]] & [Set(a)
& ALL(b):[b e a => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e a <=> c<=b]]]
=>
a e fisons]]
Join, 33, 50
As Required:
52 ALL(a):[a e fisons
<=>
Set(a) & ALL(b):[b e a => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e a <=> c<=b]]]]
Iff-And, 51
Construct the set f
Apply Cartesian Product Axiom
53 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
54 ALL(a2):[Set(n) & Set(a2) => EXIST(b):[Set'(b) &
ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e a2]]]
U Spec, 53
55 Set(n) & Set(fisons) => EXIST(b):[Set'(b)
& ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e fisons]]
U Spec, 54
56 Set(n) & Set(fisons)
Join, 1, 13
57 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e fisons]]
Detach, 55, 56
Define: nf (n x fisons)
58 Set'(nf) & ALL(c1):ALL(c2):[(c1,c2) e nf <=> c1 e n & c2 e fisons]
E Spec, 57
59 Set'(nf)
Split, 58
60 ALL(c1):ALL(c2):[(c1,c2) e nf <=> c1 e n & c2 e fisons]
Split, 58
Apply Subset Axiom
61 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e nf & ALL(c):[c e n => [c e b <=> c<=a]]]]
Subset, 59
Define: f
62 Set'(f) & ALL(a):ALL(b):[(a,b) e f <=> (a,b) e nf & ALL(c):[c e n => [c e b <=> c<=a]]]
E Spec, 61
63 Set'(f)
Split, 62
64 ALL(a):ALL(b):[(a,b) e f <=> (a,b) e nf & ALL(c):[c e n => [c e b <=> c<=a]]]
Split, 62
Prove f is a function mapping n
to the set of all fisons
Apply the Axiom of
Functionality (one variable)
65 ALL(a):ALL(b):[Set'(f) & Set(a) & Set(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):[c e a & d e b => [d=f(c) <=> (c,d) e f]]]]
U Spec, 4
66 ALL(b):[Set'(f) & Set(n) & Set(b)
=>
[ALL(c):ALL(d):[(c,d) e f => c e n & d e b]
&
ALL(c):[c e n =>
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):[c e n & d e b => [d=f(c) <=> (c,d) e f]]]]
U Spec, 65
67 Set'(f) & Set(n) & Set(fisons)
=>
[ALL(c):ALL(d):[(c,d) e f => c e n & d e fisons]
&
ALL(c):[c e n =>
EXIST(d):[d e fisons & (c,d) e f]]
&
ALL(c):ALL(d1):ALL(d2):[(c,d1) e f & (c,d2) e f => d1=d2]
=>
ALL(c):ALL(d):[c e n & d e fisons => [d=f(c) <=> (c,d) e f]]]
U Spec, 66
68 Set'(f) & Set(n)
Join, 63, 1
69 Set'(f) & Set(n) & Set(fisons)
Join, 68, 13
Sufficient: For functionality
of f
70 ALL(c):ALL(d):[(c,d) e f => c e n & d e fisons]
&
ALL(c):[c e n =>
EXIST(d):[d e fisons & (c,d) e f]]
&
ALL(c):ALL(d1):ALL(d2):[(c,d1) e f & (c,d2) e f => d1=d2]
=>
ALL(c):ALL(d):[c e n & d e fisons => [d=f(c) <=> (c,d) e f]]
Detach, 67, 69
Prove: ALL(c):ALL(d):[(c,d) e f => c e n & d e fisons]
Suppose...
71 (x,y) e f
Premise
72 ALL(b):[(x,b) e f <=> (x,b) e nf & ALL(c):[c e n => [c e b <=> c<=x]]]
U Spec, 64
73 (x,y) e f <=> (x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]]
U Spec, 72
74 [(x,y) e f => (x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]]]
&
[(x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]] => (x,y) e f]
Iff-And, 73
75 (x,y) e f => (x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]]
Split, 74
76 (x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]] => (x,y) e f
Split, 74
77 (x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]]
Detach, 75, 71
78 (x,y) e nf
Split, 77
79 ALL(c):[c e n => [c e y <=> c<=x]]
Split, 77
80 ALL(c2):[(x,c2) e nf <=> x e n & c2 e fisons]
U Spec, 60
81 (x,y) e nf <=> x e n & y e fisons
U Spec, 80
82 [(x,y) e nf => x e n & y e fisons]
&
[x e n & y e fisons => (x,y) e nf]
Iff-And, 81
83 (x,y) e nf => x e n & y e fisons
Split, 82
84 x e n & y e fisons => (x,y) e nf
Split, 82
85 x e n & y e fisons
Detach, 83, 78
Part 1
As Required:
86 ALL(c):ALL(d):[(c,d) e f => c e n & d e fisons]
4 Conclusion, 71
Prove: ALL(c):[c e n => EXIST(d):[d e fisons & (c,d) e f]]
Suppose...
87 x e n
Premise
88 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & a<=x]]
Subset, 1
Define: y
89 Set(y) & ALL(a):[a e y <=> a e n & a<=x]
E Spec, 88
90 Set(y)
Split, 89
91 ALL(a):[a e y <=> a e n & a<=x]
Split, 89
92 y e fisons
<=>
Set(y) & ALL(b):[b e y => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]]
U Spec, 52
93 [y e fisons => Set(y) & ALL(b):[b e y => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]]]
&
[Set(y) & ALL(b):[b e y => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]] => y e fisons]
Iff-And, 92
94 y e fisons => Set(y) & ALL(b):[b e y => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]]
Split, 93
Sufficient: For y e fisons
95 Set(y) & ALL(b):[b e y => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]] => y e fisons
Split, 93
Prove: ALL(b):[b e y => b e n]
Suppose...
96 z e y
Premise
97 z e y <=> z e n & z<=x
U Spec, 91
98 [z e y => z e n & z<=x] & [z e n & z<=x => z e y]
Iff-And, 97
99 z e y => z e n & z<=x
Split, 98
100 z e n & z<=x => z e y
Split, 98
101 z e n & z<=x
Detach, 99, 96
102 z e n
Split, 101
As Required:
103 ALL(b):[b e y => b e n]
4 Conclusion, 96
104 z e n
Premise
105 z e y
Premise
106 z e y <=> z e n & z<=x
U Spec, 91
107 [z e y => z e n & z<=x] & [z e n & z<=x => z e y]
Iff-And, 106
108 z e y => z e n & z<=x
Split, 107
109 z e n & z<=x => z e y
Split, 107
110 z e n & z<=x
Detach, 108, 105
111 z e n
Split, 110
112 z<=x
Split, 110
113 z e y => z<=x
4 Conclusion, 105
114 z<=x
Premise
115 z e y <=> z e n & z<=x
U Spec, 91
116 [z e y => z e n & z<=x] & [z e n & z<=x => z e y]
Iff-And, 115
117 z e y => z e n & z<=x
Split, 116
118 z e n & z<=x => z e y
Split, 116
119 z e n & z<=x
Join, 104, 114
120 z e y
Detach, 118, 119
121 z<=x => z e y
4 Conclusion, 114
122 [z e y => z<=x] & [z<=x => z e y]
Join, 113, 121
123 z e y <=> z<=x
Iff-And, 122
As Required:
124 ALL(c):[c e n => [c e y <=> c<=x]]
4 Conclusion, 104
125 x e n & ALL(c):[c e n => [c e y <=> c<=x]]
Join, 87, 124
126 EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]]
E Gen, 125
127 Set(y) & ALL(b):[b e y => b e n]
Join, 90, 103
128 Set(y) & ALL(b):[b e y => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]]
Join, 127, 126
129 y e fisons
Detach, 95, 128
130 ALL(b):[(x,b) e f <=> (x,b) e nf & ALL(c):[c e n => [c e b <=> c<=x]]]
U Spec, 64
131 ALL(b):[(x,b) e f <=> (x,b) e nf & ALL(c):[c e n => [c e b <=> c<=x]]]
U Spec, 64
132 (x,y) e f <=> (x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]]
U Spec, 131
133 [(x,y) e f => (x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]]]
&
[(x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]] => (x,y) e f]
Iff-And, 132
134 (x,y) e f => (x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]]
Split, 133
Sufficient:
135 (x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]] => (x,y) e f
Split, 133
136 ALL(c2):[(x,c2) e nf <=> x e n & c2 e fisons]
U Spec, 60
137 (x,y) e nf <=> x e n & y e fisons
U Spec, 136
138 [(x,y) e nf => x e n & y e fisons]
&
[x e n & y e fisons => (x,y) e nf]
Iff-And, 137
139 (x,y) e nf => x e n & y e fisons
Split, 138
140 x e n & y e fisons => (x,y) e nf
Split, 138
141 x e n & y e fisons
Join, 87, 129
142 (x,y) e nf
Detach, 140, 141
143 z e n
Premise
144 z e y <=> z e n & z<=x
U Spec, 91
145 [z e y => z e n & z<=x] & [z e n & z<=x => z e y]
Iff-And, 144
146 z e y => z e n & z<=x
Split, 145
147 z e n & z<=x => z e y
Split, 145
148 z e y
Premise
149 z e n & z<=x
Detach, 146, 148
150 z e n
Split, 149
151 z<=x
Split, 149
152 z e y => z<=x
4 Conclusion, 148
153 z<=x
Premise
154 z e n & z<=x
Join, 143, 153
155 z e y
Detach, 147, 154
156 z<=x => z e y
4 Conclusion, 153
157 [z e y => z<=x] & [z<=x => z e y]
Join, 152, 156
158 z e y <=> z<=x
Iff-And, 157
159 ALL(c):[c e n => [c e y <=> c<=x]]
4 Conclusion, 143
160 (x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]]
Join, 142, 159
161 (x,y) e f
Detach, 135, 160
162 y e fisons & (x,y) e f
Join, 129, 161
163 EXIST(d):[d e fisons & (x,d) e f]
E Gen, 162
Part 2
As Required:
164 ALL(c):[c e n =>
EXIST(d):[d e fisons & (c,d) e f]]
4 Conclusion, 87
Prove: ALL(c):ALL(d1):ALL(d2):[(c,d1) e f & (c,d2) e f =>
d1=d2]
Suppose...
165 (x,y1) e f & (x,y2) e f
Premise
166 (x,y1) e f
Split, 165
167 (x,y2) e f
Split, 165
168 ALL(b):[(x,b) e f <=> (x,b) e nf & ALL(c):[c e n => [c e b <=> c<=x]]]
U Spec, 64
169 (x,y1) e f <=> (x,y1) e nf & ALL(c):[c e n => [c e y1 <=> c<=x]]
U Spec, 168
170 [(x,y1) e f => (x,y1) e nf & ALL(c):[c e n => [c e y1 <=> c<=x]]]
&
[(x,y1) e nf & ALL(c):[c e n => [c e y1 <=> c<=x]] => (x,y1) e f]
Iff-And, 169
171 (x,y1) e f => (x,y1) e nf & ALL(c):[c e n => [c e y1 <=> c<=x]]
Split, 170
172 (x,y1) e nf & ALL(c):[c e n => [c e y1 <=> c<=x]] => (x,y1) e f
Split, 170
173 (x,y1) e nf & ALL(c):[c e n => [c e y1 <=> c<=x]]
Detach, 171, 166
174 (x,y1) e nf
Split, 173
175 ALL(c):[c e n => [c e y1 <=> c<=x]]
Split, 173
176 ALL(c2):[(x,c2) e nf <=> x e n & c2 e fisons]
U Spec, 60
177 (x,y1) e nf <=> x e n & y1 e fisons
U Spec, 176
178 [(x,y1) e nf => x e n & y1 e fisons]
&
[x e n & y1 e fisons => (x,y1) e nf]
Iff-And, 177
179 (x,y1) e nf => x e n & y1 e fisons
Split, 178
180 x e n & y1 e fisons => (x,y1) e nf
Split, 178
181 x e n & y1 e fisons
Detach, 179, 174
182 x e n
Split, 181
183 y1 e fisons
Split, 181
184 (x,y2) e f <=> (x,y2) e nf & ALL(c):[c e n => [c e y2 <=> c<=x]]
U Spec, 168
185 [(x,y2) e f => (x,y2) e nf & ALL(c):[c e n => [c e y2 <=> c<=x]]]
&
[(x,y2) e nf & ALL(c):[c e n => [c e y2 <=> c<=x]] => (x,y2) e f]
Iff-And, 184
186 (x,y2) e f => (x,y2) e nf & ALL(c):[c e n => [c e y2 <=> c<=x]]
Split, 185
187 (x,y2) e nf & ALL(c):[c e n => [c e y2 <=> c<=x]] => (x,y2) e f
Split, 185
188 (x,y2) e nf & ALL(c):[c e n => [c e y2 <=> c<=x]]
Detach, 186, 167
189 (x,y2) e nf
Split, 188
190 ALL(c):[c e n => [c e y2 <=> c<=x]]
Split, 188
191 (x,y2) e nf <=> x e n & y2 e fisons
U Spec, 176
192 [(x,y2) e nf => x e n & y2 e fisons]
&
[x e n & y2 e fisons => (x,y2) e nf]
Iff-And, 191
193 (x,y2) e nf => x e n & y2 e fisons
Split, 192
194 x e n & y2 e fisons => (x,y2) e nf
Split, 192
195 x e n & y2 e fisons
Detach, 193, 189
196 x e n
Split, 195
197 y2 e fisons
Split, 195
198 (x,y1) e f <=> (x,y1) e nf & ALL(c):[c e n => [c e y1 <=> c<=x]]
U Spec, 168
199 [(x,y1) e f => (x,y1) e nf & ALL(c):[c e n => [c e y1 <=> c<=x]]]
&
[(x,y1) e nf & ALL(c):[c e n => [c e y1 <=> c<=x]] => (x,y1) e f]
Iff-And, 198
200 (x,y1) e f => (x,y1) e nf & ALL(c):[c e n => [c e y1 <=> c<=x]]
Split, 199
201 (x,y1) e nf & ALL(c):[c e n => [c e y1 <=> c<=x]] => (x,y1) e f
Split, 199
202 (x,y1) e nf & ALL(c):[c e n => [c e y1 <=> c<=x]]
Detach, 200, 166
203 (x,y1) e nf
Split, 202
204 ALL(c):[c e n => [c e y1 <=> c<=x]]
Split, 202
205 ALL(a):ALL(b):[Set(a) & Set(b) =>
[a=b <=> ALL(c):[c e a <=> c e b]]]
Set Equality
206 ALL(b):[Set(y1) & Set(b)
=> [y1=b <=> ALL(c):[c e y1 <=> c e b]]]
U Spec, 205
207 Set(y1) & Set(y2) => [y1=y2 <=> ALL(c):[c e y1 <=> c e y2]]
U Spec, 206
208 y1 e fisons
<=>
Set(y1) & ALL(b):[b e y1 => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y1 <=> c<=b]]]
U Spec, 52
209 [y1 e fisons => Set(y1) & ALL(b):[b e y1 => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y1 <=> c<=b]]]]
&
[Set(y1) & ALL(b):[b e y1 => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y1 <=> c<=b]]] => y1 e fisons]
Iff-And, 208
210 y1 e fisons => Set(y1) & ALL(b):[b e y1 => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y1 <=> c<=b]]]
Split, 209
211 Set(y1) & ALL(b):[b e y1 => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y1 <=> c<=b]]] => y1 e fisons
Split, 209
212 Set(y1) & ALL(b):[b e y1 => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y1 <=> c<=b]]]
Detach, 210, 183
213 Set(y1)
Split, 212
214 ALL(b):[b e y1 => b e n]
Split, 212
215 EXIST(b):[b e n & ALL(c):[c e n => [c e y1 <=> c<=b]]]
Split, 212
216 y2 e fisons
<=>
Set(y2) & ALL(b):[b e y2 => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y2 <=> c<=b]]]
U Spec, 52
217 [y2 e fisons => Set(y2) & ALL(b):[b e y2 => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y2 <=> c<=b]]]]
&
[Set(y2) & ALL(b):[b e y2 => b e n]
& EXIST(b):[b e n & ALL(c):[c e n => [c e y2 <=> c<=b]]] => y2 e fisons]
Iff-And, 216
218 y2 e fisons => Set(y2) & ALL(b):[b e y2 => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y2 <=> c<=b]]]
Split, 217
219 Set(y2) & ALL(b):[b e y2 => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y2 <=> c<=b]]] => y2 e fisons
Split, 217
220 Set(y2) & ALL(b):[b e y2 => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y2 <=> c<=b]]]
Detach, 218, 197
221 Set(y2)
Split, 220
222 ALL(b):[b e y2 => b e n]
Split, 220
223 EXIST(b):[b e n & ALL(c):[c e n => [c e y2 <=> c<=b]]]
Split, 220
224 Set(y1) & Set(y2)
Join, 213, 221
225 y1=y2 <=> ALL(c):[c e y1 <=> c e y2]
Detach, 207, 224
226 [y1=y2 => ALL(c):[c e y1 <=> c e y2]]
&
[ALL(c):[c e y1 <=> c e y2] => y1=y2]
Iff-And, 225
227 y1=y2 => ALL(c):[c e y1 <=> c e y2]
Split, 226
Sufficient: y1=y2
228 ALL(c):[c e y1 <=> c e y2] => y1=y2
Split, 226
Prove: ALL(c):[c e y1 => c e y2]
Suppose...
229 z e y1
Premise
230 z e y1 => z e n
U Spec, 214
231 z e n
Detach, 230, 229
232 z e n => [z e y1 <=> z<=x]
U Spec, 175
233 z e y1 <=> z<=x
Detach, 232, 231
234 [z e y1 => z<=x] & [z<=x => z e y1]
Iff-And, 233
235 z e y1 => z<=x
Split, 234
236 z<=x => z e y1
Split, 234
237 z<=x
Detach, 235, 229
238 z e n => [z e y2 <=> z<=x]
U Spec, 190
239 z e y2 <=> z<=x
Detach, 238, 231
240 [z e y2 => z<=x] & [z<=x => z e y2]
Iff-And, 239
241 z e y2 => z<=x
Split, 240
242 z<=x => z e y2
Split, 240
243 z e y2
Detach, 242, 237
As Required:
244 ALL(c):[c e y1 => c e y2]
4 Conclusion, 229
Prove: ALL(c):[c e y2 => c e y1]
Suppose...
245 z e y2
Premise
246 z e y2 => z e n
U Spec, 222
247 z e n
Detach, 246, 245
248 z e n => [z e y2 <=> z<=x]
U Spec, 190
249 z e y2 <=> z<=x
Detach, 248, 247
250 [z e y2 => z<=x] & [z<=x => z e y2]
Iff-And, 249
251 z e y2 => z<=x
Split, 250
252 z<=x => z e y2
Split, 250
253 z<=x
Detach, 251, 245
254 z e n => [z e y1 <=> z<=x]
U Spec, 204
255 z e y1 <=> z<=x
Detach, 254, 247
256 [z e y1 => z<=x] & [z<=x => z e y1]
Iff-And, 255
257 z e y1 => z<=x
Split, 256
258 z<=x => z e y1
Split, 256
259 z e y1
Detach, 258, 253
As Required:
260 ALL(c):[c e y2 => c e y1]
4 Conclusion, 245
261 ALL(c):[[c e y1 => c e y2] & [c e y2 => c e y1]]
Join, 244, 260
262 ALL(c):[c e y1 <=> c e y2]
Iff-And, 261
263 y1=y2
Detach, 228, 262
Part 3
As Required:
264 ALL(c):ALL(d1):ALL(d2):[(c,d1) e f & (c,d2) e f => d1=d2]
4 Conclusion, 165
265 ALL(c):ALL(d):[(c,d) e f => c e n & d e fisons]
&
ALL(c):[c e n =>
EXIST(d):[d e fisons & (c,d) e f]]
Join, 86, 164
266 ALL(c):ALL(d):[(c,d) e f => c e n & d e fisons]
&
ALL(c):[c e n =>
EXIST(d):[d e fisons & (c,d) e f]]
&
ALL(c):ALL(d1):ALL(d2):[(c,d1) e f & (c,d2) e f => d1=d2]
Join, 265, 264
As Required:
f is a function mapping the set
n to the set of fisons
267 ALL(c):ALL(d):[c e n & d e fisons => [d=f(c) <=> (c,d) e f]]
Detach, 70, 266
268 x e n
Premise
269 x e n => EXIST(d):[d e fisons & (x,d) e f]
U Spec, 164
270 EXIST(d):[d e fisons & (x,d) e f]
Detach, 269, 268
271 y e fisons & (x,y) e f
E Spec, 270
272 y e fisons
Split, 271
273 (x,y) e f
Split, 271
274 ALL(d):[x e n & d e fisons => [d=f(x) <=> (x,d) e f]]
U Spec, 267
275 x e n & y e fisons => [y=f(x) <=> (x,y) e f]
U Spec, 274
276 x e n & y e fisons
Join, 268, 272
277 y=f(x) <=> (x,y) e f
Detach, 275, 276
278 [y=f(x) => (x,y) e f] & [(x,y) e f => y=f(x)]
Iff-And, 277
279 y=f(x) => (x,y) e f
Split, 278
280 (x,y) e f => y=f(x)
Split, 278
281 y=f(x)
Detach, 280, 273
282 f(x) e fisons
Substitute, 281,
272
As Required:
283 ALL(a):[a e n => f(a) e fisons]
4 Conclusion, 268
Prove: ALL(a):[a e n
=> f(a) e fisons
& ALL(c):[c e n => [c e f(a) <=> c<=a]]]
Suppose...
284 x e n
Premise
285 x e n => EXIST(d):[d e fisons & (x,d) e f]
U Spec, 164
286 EXIST(d):[d e fisons & (x,d) e f]
Detach, 285, 284
287 y e fisons & (x,y) e f
E Spec, 286
288 y e fisons
Split, 287
289 (x,y) e f
Split, 287
290 ALL(b):[(x,b) e f <=> (x,b) e nf & ALL(c):[c e n => [c e b <=> c<=x]]]
U Spec, 64
291 (x,y) e f <=> (x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]]
U Spec, 290
292 [(x,y) e f => (x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]]]
&
[(x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]] => (x,y) e f]
Iff-And, 291
293 (x,y) e f => (x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]]
Split, 292
294 (x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]] => (x,y) e f
Split, 292
295 (x,y) e nf & ALL(c):[c e n => [c e y <=> c<=x]]
Detach, 293, 289
296 (x,y) e nf
Split, 295
297 ALL(c):[c e n => [c e y <=> c<=x]]
Split, 295
298 ALL(d):[x e n & d e fisons => [d=f(x) <=> (x,d) e f]]
U Spec, 267
299 x e n & y e fisons => [y=f(x) <=> (x,y) e f]
U Spec, 298
300 x e n & y e fisons
Join, 284, 288
301 y=f(x) <=> (x,y) e f
Detach, 299, 300
302 [y=f(x) => (x,y) e f] & [(x,y) e f => y=f(x)]
Iff-And, 301
303 y=f(x) => (x,y) e f
Split, 302
304 (x,y) e f => y=f(x)
Split, 302
305 y=f(x)
Detach, 304, 289
306 ALL(c):[c e n => [c e f(x) <=> c<=x]]
Substitute, 305,
297
307 f(x) e fisons
Substitute, 305,
288
308 f(x) e fisons
&
ALL(c):[c e n => [c e f(x) <=> c<=x]]
Join, 307, 306
As Required:
309 ALL(a):[a e n
=>
f(a) e fisons
&
ALL(c):[c e n => [c e f(a) <=> c<=a]]]
4 Conclusion, 284
Prove: f is surjective
Suppose...
310 y e fisons
Premise
311 y e fisons
<=>
Set(y) & ALL(b):[b e y => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]]
U Spec, 52
312 [y e fisons => Set(y) & ALL(b):[b e y => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]]]
&
[Set(y) & ALL(b):[b e y => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]] => y e fisons]
Iff-And, 311
313 y e fisons => Set(y) & ALL(b):[b e y => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]]
Split, 312
314 Set(y) & ALL(b):[b e y => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]] => y e fisons
Split, 312
315 Set(y) & ALL(b):[b e y => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]]
Detach, 313, 310
316 Set(y)
Split, 315
317 ALL(b):[b e y => b e n]
Split, 315
318 EXIST(b):[b e n & ALL(c):[c e n => [c e y <=> c<=b]]]
Split, 315
319 z e n & ALL(c):[c e n => [c e y <=> c<=z]]
E Spec, 318
Define: z
320 z e n
Split, 319
321 ALL(c):[c e n => [c e y <=> c<=z]]
Split, 319
322 z e n
=>
f(z) e fisons
&
ALL(c):[c e n => [c e f(z) <=> c<=z]]
U Spec, 309
323 f(z) e fisons
&
ALL(c):[c e n => [c e f(z) <=> c<=z]]
Detach, 322, 320
324 f(z) e fisons
Split, 323
325 ALL(c):[c e n => [c e f(z) <=> c<=z]]
Split, 323
326 z e n & f(z) e fisons
Join, 320, 324
327 EXIST(b):[b e n & f(b) e fisons]
E Gen, 326
f is surjective
As Required:
328 ALL(a):[a e fisons => EXIST(b):[b e n & f(b) e fisons]]
4 Conclusion, 310
Prove: ALL(a):[a e n => a e f(a)]
Suppose...
329 x e n
Premise
330 x e n
=>
f(x) e fisons
&
ALL(c):[c e n => [c e f(x) <=> c<=x]]
U Spec, 309
331 f(x) e fisons
&
ALL(c):[c e n => [c e f(x) <=> c<=x]]
Detach, 330, 329
332 f(x) e fisons
Split, 331
333 ALL(c):[c e n => [c e f(x) <=> c<=x]]
Split, 331
334 x e n => [x e f(x) <=> x<=x]
U Spec, 333
335 x e f(x) <=> x<=x
Detach, 334, 329
336 [x e f(x) => x<=x] & [x<=x => x e f(x)]
Iff-And, 335
337 x e f(x) => x<=x
Split, 336
338 x<=x => x e f(x)
Split, 336
339 x e n => x<=x
U Spec, 2
340 x<=x
Detach, 339, 329
341 x e f(x)
Detach, 338, 340
As Required:
342 ALL(a):[a e n => a e f(a)]
4 Conclusion, 329
Prove: f is injective
Suppose...
343 x1 e n & x2 e n
Premise
344 x1 e n
Split, 343
345 x2 e n
Split, 343
346 x1 e n => x1 e f(x1)
U Spec, 342
347 x1 e f(x1)
Detach, 346, 344
348 x2 e n => x2 e f(x2)
U Spec, 342
349 x2 e f(x2)
Detach, 348, 345
350 x1 e n
=>
f(x1) e fisons
&
ALL(c):[c e n => [c e f(x1) <=> c<=x1]]
U Spec, 309
351 f(x1) e fisons
&
ALL(c):[c e n => [c e f(x1) <=> c<=x1]]
Detach, 350, 344
352 f(x1) e fisons
Split, 351
353 ALL(c):[c e n => [c e f(x1) <=> c<=x1]]
Split, 351
354 x2 e n
=>
f(x2) e fisons
&
ALL(c):[c e n => [c e f(x2) <=> c<=x2]]
U Spec, 309
355 f(x2) e fisons
&
ALL(c):[c e n => [c e f(x2) <=> c<=x2]]
Detach, 354, 345
356 f(x2) e fisons
Split, 355
357 ALL(c):[c e n => [c e f(x2) <=> c<=x2]]
Split, 355
Prove: f(x1)=f(x2) => x1=x2
Suppose...
358 f(x1)=f(x2)
Premise
359 ALL(c):[c e n => [c e f(x1) <=> c<=x2]]
Substitute, 358,
357
360 x1 e n => [x1 e f(x1) <=> x1<=x2]
U Spec, 359
361 x1 e f(x1) <=> x1<=x2
Detach, 360, 344
362 [x1 e f(x1) => x1<=x2] & [x1<=x2 => x1 e f(x1)]
Iff-And, 361
363 x1 e f(x1) => x1<=x2
Split, 362
364 x1<=x2 => x1 e f(x1)
Split, 362
365 x1<=x2
Detach, 363, 347
366 x2 e n => [x2 e f(x1) <=> x2<=x1]
U Spec, 353
367 x2 e f(x1) <=> x2<=x1
Detach, 366, 345
368 [x2 e f(x1) => x2<=x1] & [x2<=x1 => x2 e f(x1)]
Iff-And, 367
369 x2 e f(x1) => x2<=x1
Split, 368
370 x2<=x1 => x2 e f(x1)
Split, 368
371 ALL(a):ALL(b):[Set(a) & Set(b) =>
[a=b <=> ALL(c):[c e a <=> c e b]]]
Set Equality
372 ALL(b):[Set(f(x1)) & Set(b)
=> [f(x1)=b <=> ALL(c):[c e f(x1) <=> c e b]]]
U Spec, 371
373 Set(f(x1)) & Set(f(x2)) => [f(x1)=f(x2) <=> ALL(c):[c e f(x1) <=> c e f(x2)]]
U Spec, 372
374 f(x1) e fisons
<=>
Set(f(x1)) & ALL(b):[b e f(x1) => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e f(x1) <=> c<=b]]]
U Spec, 52
375 [f(x1) e fisons => Set(f(x1)) & ALL(b):[b e f(x1) => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e f(x1) <=> c<=b]]]]
&
[Set(f(x1)) & ALL(b):[b e f(x1) => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e f(x1) <=> c<=b]]] => f(x1) e fisons]
Iff-And, 374
376 f(x1) e fisons => Set(f(x1)) & ALL(b):[b e f(x1) => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e f(x1) <=> c<=b]]]
Split, 375
377 Set(f(x1)) & ALL(b):[b e f(x1) => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e f(x1) <=> c<=b]]] => f(x1) e fisons
Split, 375
378 Set(f(x1)) & ALL(b):[b e f(x1) => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e f(x1) <=> c<=b]]]
Detach, 376, 352
379 Set(f(x1))
Split, 378
380 ALL(b):[b e f(x1) => b e n]
Split, 378
381 EXIST(b):[b e n & ALL(c):[c e n => [c e f(x1) <=> c<=b]]]
Split, 378
382 f(x2) e fisons
<=>
Set(f(x2)) & ALL(b):[b e f(x2) => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e f(x2) <=> c<=b]]]
U Spec, 52
383 [f(x2) e fisons => Set(f(x2)) & ALL(b):[b e f(x2) => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e f(x2) <=> c<=b]]]]
&
[Set(f(x2)) & ALL(b):[b e f(x2) => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e f(x2) <=> c<=b]]] => f(x2) e fisons]
Iff-And, 382
384 f(x2) e fisons => Set(f(x2)) & ALL(b):[b e f(x2) => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e f(x2) <=> c<=b]]]
Split, 383
385 Set(f(x2)) & ALL(b):[b e f(x2) => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e f(x2) <=> c<=b]]] => f(x2) e fisons
Split, 383
386 Set(f(x2)) & ALL(b):[b e f(x2) => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e f(x2) <=> c<=b]]]
Detach, 384, 356
387 Set(f(x2))
Split, 386
388 ALL(b):[b e f(x2) => b e n]
Split, 386
389 EXIST(b):[b e n & ALL(c):[c e n => [c e f(x2) <=> c<=b]]]
Split, 386
390 Set(f(x1)) & Set(f(x2))
Join, 379, 387
391 f(x1)=f(x2) <=>
ALL(c):[c e f(x1) <=> c e f(x2)]
Detach, 373, 390
392 [f(x1)=f(x2) =>
ALL(c):[c e f(x1) <=> c e f(x2)]]
&
[ALL(c):[c e f(x1) <=> c e f(x2)] => f(x1)=f(x2)]
Iff-And, 391
393 f(x1)=f(x2) =>
ALL(c):[c e f(x1) <=> c e f(x2)]
Split, 392
394 ALL(c):[c e f(x1) <=> c e f(x2)] => f(x1)=f(x2)
Split, 392
395 ALL(c):[c e f(x1) <=> c e f(x2)]
Detach, 393, 358
396 x2 e f(x1) <=> x2 e f(x2)
U Spec, 395
397 [x2 e f(x1) => x2 e f(x2)] & [x2 e f(x2) => x2 e f(x1)]
Iff-And, 396
398 x2 e f(x1) => x2 e f(x2)
Split, 397
399 x2 e f(x2) => x2 e f(x1)
Split, 397
400 x2 e f(x1)
Detach, 399, 349
401 x2<=x1
Detach, 369, 400
402 ALL(b):[x1 e n & b e n => [x1<=b &
b<=x1 => x1=b]]
U Spec, 3
403 x1 e n & x2 e n => [x1<=x2 & x2<=x1 => x1=x2]
U Spec, 402
404 x1<=x2 & x2<=x1 => x1=x2
Detach, 403, 343
405 x1<=x2 & x2<=x1
Join, 365, 401
406 x1=x2
Detach, 404, 405
As Required:
407 f(x1)=f(x2) => x1=x2
4 Conclusion, 358
f is injective
As Required:
408 ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]
4 Conclusion, 343
409 Set(fisons)
&
ALL(a):[a e fisons
<=>
Set(a) & ALL(b):[b e a => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e a <=> c<=b]]]]
Join, 13, 52
410 Set(fisons)
&
ALL(a):[a e fisons
<=>
Set(a) & ALL(b):[b e a => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e a <=> c<=b]]]]
&
ALL(a):[a e n => f(a) e fisons]
Join, 409, 283
411 Set(fisons)
&
ALL(a):[a e fisons
<=>
Set(a) & ALL(b):[b e a => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e a <=> c<=b]]]]
&
ALL(a):[a e n => f(a) e fisons]
&
ALL(a):[a e fisons => EXIST(b):[b e n & f(b) e fisons]]
Join, 410, 328
412 Set(fisons)
&
ALL(a):[a e fisons
<=>
Set(a) & ALL(b):[b e a => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e a <=> c<=b]]]]
&
ALL(a):[a e n => f(a) e fisons]
&
ALL(a):[a e fisons => EXIST(b):[b e n & f(b) e fisons]]
&
ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]
Join, 411, 408
413 EXIST(f):[Set(fisons)
&
ALL(a):[a e fisons
<=>
Set(a) & ALL(b):[b e a => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e a <=> c<=b]]]]
&
ALL(a):[a e n => f(a) e fisons]
&
ALL(a):[a e fisons => EXIST(b):[b e n & f(b) e fisons]]
&
ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]]
E Gen, 412
As Required:
414 EXIST(fisons):EXIST(f):[Set(fisons)
&
ALL(a):[a e fisons
<=>
Set(a) & ALL(b):[b e a => b e n]
&
EXIST(b):[b e n & ALL(c):[c e n => [c e a <=> c<=b]]]]
&
ALL(a):[a e n => f(a) e fisons]
&
ALL(a):[a e fisons => EXIST(b):[b e n & f(b) e fisons]]
&
ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]]
E Gen, 413