THEOREM
*******
Suppose...
s =
an arbitrary set
ps = the power set of s
i =
{0, 1}
fsi = the set of all functions f: s --> i
There exists a bijection g: fsi
--> ps such that
g(f) = {x e s : f(x)=1}
OUTLINE OF PROOF
****************
Lines
1-7 Axioms
8-21 Establish properties of i
22-39 Construct fsi
40-93 Prove each element of fsi is a function
94-106 Construct g
107-321 Prove g is a function g(f) = {x e s : f(x)=1}
322-600 Prove g is surjective
600-983 Prove g is injective
This machine verified, formal
proof was written with the aid of the author's DC Proof 2.0 freeware available
at http://www.dcproof.com
Axiom of functionality for 1 variable
1 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
Let s be an arbitrary set
2 Set(s)
Axiom
Let ps be the power set of s
3 Set(ps)
Axiom
4 ALL(a):[a e ps <=>
Set(a) & ALL(b):[b e a => b e s]]
Axiom
Define: i {0, 1}
5 Set(i)
Axiom
6 ALL(a):[a e i <=> a=0 | a=1]
Axiom
7 ~0=1
Axiom
Prove: 0 e i
8 0 e i <=> 0=0 | 0=1
U Spec, 6
9 [0 e i => 0=0 | 0=1] & [0=0 | 0=1 => 0 e i]
Iff-And, 8
10 0 e i => 0=0 | 0=1
Split, 9
11 0=0 | 0=1 => 0 e i
Split, 9
12 0=0
Reflex
13 0=0 | 0=1
Arb Or, 12
14 0 e i
Detach, 11, 13
Prove: 1 e i
15 1 e i <=> 1=0 | 1=1
U Spec, 6
16 [1 e i => 1=0 | 1=1] & [1=0 | 1=1 => 1 e i]
Iff-And, 15
17 1 e i => 1=0 | 1=1
Split, 16
18 1=0 | 1=1 => 1 e i
Split, 16
19 1=1
Reflex
20 1=0 | 1=1
Arb Or, 19
21 1 e i
Detach, 18, 20
Construct fsi
Apply the Cartesian Product
Axiom
22 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
23 ALL(a2):[Set(s) & Set(a2) => EXIST(b):[Set'(b) &
ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e s & c2 e a2]]]
U Spec, 22
24 Set(s) & Set(i) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e s & c2 e i]]
U Spec, 23
25 Set(s) & Set(i)
Join, 2, 5
26 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e s & c2 e i]]
Detach, 24, 25
27 Set'(si) & ALL(c1):ALL(c2):[(c1,c2) e si <=> c1 e s & c2 e i]
E Spec, 26
Define: si (s x i)
**********
28 Set'(si)
Split, 27
29 ALL(c1):ALL(c2):[(c1,c2) e si <=> c1 e s & c2 e i]
Split, 27
30 ALL(a):[Set'(a) => EXIST(b):[Set(b)
&
ALL(c):[c e b <=>
Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e a]]]]
Power Set
31 Set'(si) => EXIST(b):[Set(b)
&
ALL(c):[c e b <=>
Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e si]]]
U Spec, 30
32 EXIST(b):[Set(b)
&
ALL(c):[c e b <=>
Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e si]]]
Detach, 31, 28
33 Set(psi)
&
ALL(c):[c e psi <=>
Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e si]]
E Spec, 32
Define: psi (power set of si)
***********
34 Set(psi)
Split, 33
35 ALL(c):[c e psi <=>
Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e si]]
Split, 33
36 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e psi & [ALL(b):[b e s =>
EXIST(c):[c e i & (b,c) e a]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e a & (b,d) e a => c=d]]]]
Subset, 34
37 Set(fsi) & ALL(a):[a e fsi <=> a e psi & [ALL(b):[b e s => EXIST(c):[c e i & (b,c) e a]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e a & (b,d) e a => c=d]]]
E Spec, 36
Define: fsi (set of all functions mapping s to i)
***********
38 Set(fsi)
Split, 37
39 ALL(a):[a e fsi <=> a e psi & [ALL(b):[b e s =>
EXIST(c):[c e i & (b,c) e a]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e a & (b,d) e a => c=d]]]
Split, 37
Suppose...
40 f e fsi
Premise
41 f e fsi <=> f e psi & [ALL(b):[b e s => EXIST(c):[c e i & (b,c) e f]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e f & (b,d) e f => c=d]]
U Spec, 39
42 [f e fsi => f e psi & [ALL(b):[b e s => EXIST(c):[c e i & (b,c) e f]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e f & (b,d) e f => c=d]]]
&
[f e psi & [ALL(b):[b e s => EXIST(c):[c e i & (b,c) e f]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e f & (b,d) e f => c=d]] => f e fsi]
Iff-And, 41
43 f e fsi => f e psi & [ALL(b):[b e s => EXIST(c):[c e i & (b,c) e f]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e f & (b,d) e f => c=d]]
Split, 42
44 f e psi & [ALL(b):[b e s => EXIST(c):[c e i & (b,c) e f]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e f & (b,d) e f => c=d]] => f e fsi
Split, 42
45 f e psi & [ALL(b):[b e s => EXIST(c):[c e i & (b,c) e f]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e f & (b,d) e f => c=d]]
Detach, 43, 40
46 f e psi
Split, 45
47 ALL(b):[b e s => EXIST(c):[c e i & (b,c) e f]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e f & (b,d) e f => c=d]
Split, 45
48 ALL(b):[b e s =>
EXIST(c):[c e i & (b,c) e f]]
Split, 47
49 ALL(b):ALL(c):ALL(d):[(b,c) e f & (b,d) e f => c=d]
Split, 47
50 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, 1
51 ALL(b):[Set'(f) & Set(s) & Set(b)
=>
[ALL(c):ALL(d):[(c,d) e f => c e s & d e b]
&
ALL(c):[c e s =>
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 s & d e b => [d=f(c) <=> (c,d) e f]]]]
U Spec, 50
52 Set'(f) & Set(s) & Set(i)
=>
[ALL(c):ALL(d):[(c,d) e f => c e s & d e i]
&
ALL(c):[c e s =>
EXIST(d):[d e i & (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 s & d e i => [d=f(c) <=> (c,d) e f]]]
U Spec, 51
53 f e psi <=> Set'(f) & ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e si]
U Spec, 35
54 [f e psi => Set'(f) & ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e si]]
&
[Set'(f) & ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e si] => f e psi]
Iff-And, 53
55 f e psi => Set'(f) & ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e si]
Split, 54
56 Set'(f) & ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e si] => f e psi
Split, 54
57 Set'(f) & ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e si]
Detach, 55, 46
Define: f
58 Set'(f)
Split, 57
59 ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e si]
Split, 57
60 Set'(f) & Set(s)
Join, 58, 2
61 Set'(f) & Set(s) & Set(i)
Join, 60, 5
Sufficient: For functionality of f
62 ALL(c):ALL(d):[(c,d) e f => c e s & d e i]
&
ALL(c):[c e s =>
EXIST(d):[d e i & (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 s & d e i => [d=f(c) <=> (c,d) e f]]
Detach, 52, 61
63 (x,y) e f
Premise
64 ALL(d2):[(x,d2) e f => (x,d2) e si]
U Spec, 59
65 (x,y) e f => (x,y) e si
U Spec, 64
66 (x,y) e si
Detach, 65, 63
67 ALL(c2):[(x,c2) e si <=> x e s & c2 e i]
U Spec, 29
68 (x,y) e si <=> x e s & y e i
U Spec, 67
69 [(x,y) e si => x e s & y e i]
&
[x e s & y e i => (x,y) e si]
Iff-And, 68
70 (x,y) e si => x e s & y e i
Split, 69
71 x e s & y e i => (x,y) e si
Split, 69
72 x e s & y e i
Detach, 70, 66
Functionality - Part 1
73 ALL(c):ALL(d):[(c,d) e f => c e s & d e i]
4 Conclusion, 63
74 ALL(c):ALL(d):[(c,d) e f => c e s & d e i]
&
ALL(b):[b e s =>
EXIST(c):[c e i & (b,c) e f]]
Join, 73, 48
75 ALL(c):ALL(d):[(c,d) e f => c e s & d e i]
&
ALL(b):[b e s =>
EXIST(c):[c e i & (b,c) e f]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e f & (b,d) e f => c=d]
Join, 74, 49
f is a function
As Required:
76 ALL(c):ALL(d):[c e s & d e i => [d=f(c) <=> (c,d) e f]]
Detach, 62, 75
77 x e s
Premise
78 x e s => EXIST(c):[c e i & (x,c) e f]
U Spec, 48
79 EXIST(c):[c e i & (x,c) e f]
Detach, 78, 77
80 y e i & (x,y) e f
E Spec, 79
81 y e i
Split, 80
82 (x,y) e f
Split, 80
83 ALL(d):[x e s & d e i => [d=f(x) <=> (x,d) e f]]
U Spec, 76
84 x e s & y e i => [y=f(x) <=> (x,y) e f]
U Spec, 83
85 x e s & y e i
Join, 77, 81
86 y=f(x) <=> (x,y) e f
Detach, 84, 85
87 [y=f(x) => (x,y) e f] & [(x,y) e f => y=f(x)]
Iff-And, 86
88 y=f(x) => (x,y) e f
Split, 87
89 (x,y) e f => y=f(x)
Split, 87
90 y=f(x)
Detach, 89, 82
91 f(x) e i
Substitute, 90,
81
As Required:
92 ALL(a):[a e s => f(a) e i]
4 Conclusion, 77
Every element f of fsi is a
function f: s --> i
As Required:
93 ALL(f):[f e fsi => ALL(a):[a e s => f(a) e i]]
4 Conclusion, 40
94 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
95 ALL(a2):[Set(fsi) & Set(a2) => EXIST(b):[Set'(b)
& ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e fsi & c2 e a2]]]
U Spec, 94
96 Set(fsi) & Set(ps) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e fsi & c2 e ps]]
U Spec, 95
97 Set(fsi) & Set(ps)
Join, 38, 3
98 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e fsi & c2 e ps]]
Detach, 96, 97
99 Set'(fps) & ALL(c1):ALL(c2):[(c1,c2) e fps <=> c1 e fsi & c2 e ps]
E Spec, 98
Define: fps (fsi x ps)
***********
100 Set'(fps)
Split, 99
101 ALL(c1):ALL(c2):[(c1,c2) e fps <=> c1 e fsi & c2 e ps]
Split, 99
102 ALL(a):[Set'(a) => EXIST(b):[Set(b)
&
ALL(c):[c e b <=>
Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e a]]]]
Power Set
103 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e fps & ALL(c):[c e s => [c e b <=> a(c)=1]]]]
Subset, 100
104 Set'(g) & ALL(a):ALL(b):[(a,b) e g <=> (a,b) e fps & ALL(c):[c e s => [c e b <=> a(c)=1]]]
E Spec, 103
Define: g
*********
105 Set'(g)
Split, 104
106 ALL(a):ALL(b):[(a,b) e g <=> (a,b) e fps & ALL(c):[c e s => [c e b <=> a(c)=1]]]
Split, 104
107 ALL(a):ALL(b):[Set'(g) & Set(a) & Set(b)
=>
[ALL(c):ALL(d):[(c,d) e g => c e a & d e b]
&
ALL(c):[c e a =>
EXIST(d):[d e b & (c,d) e g]]
&
ALL(c):ALL(d1):ALL(d2):[(c,d1) e g & (c,d2) e g => d1=d2]
=>
ALL(c):ALL(d):[c e a & d e b => [d=g(c) <=> (c,d) e g]]]]
U Spec, 1
108 ALL(b):[Set'(g) & Set(fsi) & Set(b)
=>
[ALL(c):ALL(d):[(c,d) e g => c e fsi & d e b]
&
ALL(c):[c e fsi =>
EXIST(d):[d e b & (c,d) e g]]
&
ALL(c):ALL(d1):ALL(d2):[(c,d1) e g & (c,d2) e g => d1=d2]
=>
ALL(c):ALL(d):[c e fsi & d e b => [d=g(c) <=> (c,d) e g]]]]
U Spec, 107
109 Set'(g) & Set(fsi) & Set(ps)
=>
[ALL(c):ALL(d):[(c,d) e g => c e fsi & d e ps]
&
ALL(c):[c e fsi =>
EXIST(d):[d e ps & (c,d) e g]]
&
ALL(c):ALL(d1):ALL(d2):[(c,d1) e g & (c,d2) e g => d1=d2]
=>
ALL(c):ALL(d):[c e fsi & d e ps => [d=g(c) <=> (c,d) e g]]]
U Spec, 108
110 Set'(g) & Set(fsi)
Join, 105, 38
111 Set'(g) & Set(fsi) & Set(ps)
Join, 110, 3
Sufficient: For functionality
of g
112 ALL(c):ALL(d):[(c,d) e g => c e fsi & d e ps]
&
ALL(c):[c e fsi =>
EXIST(d):[d e ps & (c,d) e g]]
&
ALL(c):ALL(d1):ALL(d2):[(c,d1) e g & (c,d2) e g => d1=d2]
=>
ALL(c):ALL(d):[c e fsi & d e ps => [d=g(c) <=> (c,d) e g]]
Detach, 109, 111
Suppose...
113 (x,y) e g
Premise
114 ALL(b):[(x,b) e g <=> (x,b) e fps & ALL(c):[c e s => [c e b <=> x(c)=1]]]
U Spec, 106
115 (x,y) e g <=> (x,y) e fps & ALL(c):[c e s => [c e y <=> x(c)=1]]
U Spec, 114
116 [(x,y) e g => (x,y) e fps & ALL(c):[c e s => [c e y <=> x(c)=1]]]
&
[(x,y) e fps & ALL(c):[c e s => [c e y <=> x(c)=1]] => (x,y) e g]
Iff-And, 115
117 (x,y) e g => (x,y) e fps & ALL(c):[c e s => [c e y <=> x(c)=1]]
Split, 116
118 (x,y) e fps & ALL(c):[c e s => [c e y <=> x(c)=1]] => (x,y) e g
Split, 116
119 (x,y) e fps & ALL(c):[c e s => [c e y <=> x(c)=1]]
Detach, 117, 113
120 (x,y) e fps
Split, 119
121 ALL(c):[c e s => [c e y <=> x(c)=1]]
Split, 119
122 ALL(c2):[(x,c2) e fps <=> x e fsi & c2 e ps]
U Spec, 101
123 (x,y) e fps <=> x e fsi & y e ps
U Spec, 122
124 [(x,y) e fps => x e fsi & y e ps]
&
[x e fsi & y e ps => (x,y) e fps]
Iff-And, 123
125 (x,y) e fps => x e fsi & y e ps
Split, 124
126 x e fsi & y e ps => (x,y) e fps
Split, 124
127 x e fsi & y e ps
Detach, 125, 120
Functionality - Part 1
128 ALL(c):ALL(d):[(c,d) e g => c e fsi & d e ps]
4 Conclusion, 113
Suppose...
129 f e fsi
Premise
130 f e fsi => ALL(a):[a e s => f(a) e i]
U Spec, 93
131 ALL(a):[a e s => f(a) e i]
Detach, 130, 129
132 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e s & f(a)=1]]
Subset, 2
133 Set(q) & ALL(a):[a e q <=> a e s & f(a)=1]
E Spec, 132
Define: q
*********
134 Set(q)
Split, 133
135 ALL(a):[a e q <=> a e s & f(a)=1]
Split, 133
136 q e ps <=> Set(q) & ALL(b):[b e q => b e s]
U Spec, 4
137 [q e ps => Set(q) & ALL(b):[b e q => b e s]]
&
[Set(q) & ALL(b):[b e q => b e s] => q e ps]
Iff-And, 136
138 q e ps => Set(q) & ALL(b):[b e q => b e s]
Split, 137
Sufficient:
139 Set(q) & ALL(b):[b e q => b e s] => q e ps
Split, 137
140 x e q
Premise
141 x e q <=> x e s & f(x)=1
U Spec, 135
142 [x e q => x e s & f(x)=1] & [x e s & f(x)=1 => x e q]
Iff-And, 141
143 x e q => x e s & f(x)=1
Split, 142
144 x e s & f(x)=1 => x e q
Split, 142
145 x e s & f(x)=1
Detach, 143, 140
146 x e s
Split, 145
147 ALL(b):[b e q => b e s]
4 Conclusion, 140
148 Set(q) & ALL(b):[b e q => b e s]
Join, 134, 147
As Required:
149 q e ps
Detach, 139, 148
150 ALL(b):[(f,b) e g <=> (f,b) e fps & ALL(c):[c e s => [c e b <=> f(c)=1]]]
U Spec, 106
151 (f,q) e g <=> (f,q) e fps & ALL(c):[c e s => [c e q <=> f(c)=1]]
U Spec, 150
152 [(f,q) e g => (f,q) e fps & ALL(c):[c e s => [c e q <=> f(c)=1]]]
&
[(f,q) e fps & ALL(c):[c e s => [c e q <=> f(c)=1]] => (f,q) e g]
Iff-And, 151
153 (f,q) e g => (f,q) e fps & ALL(c):[c e s => [c e q <=> f(c)=1]]
Split, 152
Sufficient:
154 (f,q) e fps & ALL(c):[c e s => [c e q <=> f(c)=1]] => (f,q) e g
Split, 152
155 ALL(c2):[(f,c2) e fps <=> f e fsi & c2 e ps]
U Spec, 101
156 (f,q) e fps <=> f e fsi & q e ps
U Spec, 155
157 [(f,q) e fps => f e fsi & q e ps]
&
[f e fsi & q e ps => (f,q) e fps]
Iff-And, 156
158 (f,q) e fps => f e fsi & q e ps
Split, 157
Sufficient:
159 f e fsi & q e ps => (f,q) e fps
Split, 157
160 f e fsi & q e ps
Join, 129, 149
As Required:
161 (f,q) e fps
Detach, 159, 160
162 x e s
Premise
163 x e q
Premise
164 x e q <=> x e s & f(x)=1
U Spec, 135
165 [x e q => x e s & f(x)=1] & [x e s & f(x)=1 => x e q]
Iff-And, 164
166 x e q => x e s & f(x)=1
Split, 165
167 x e s & f(x)=1 => x e q
Split, 165
168 x e s & f(x)=1
Detach, 166, 163
169 x e s
Split, 168
170 f(x)=1
Split, 168
171 x e q => f(x)=1
4 Conclusion, 163
172 f(x)=1
Premise
173 x e q <=> x e s & f(x)=1
U Spec, 135
174 [x e q => x e s & f(x)=1] & [x e s & f(x)=1 => x e q]
Iff-And, 173
175 x e q => x e s & f(x)=1
Split, 174
176 x e s & f(x)=1 => x e q
Split, 174
177 x e s & f(x)=1
Join, 162, 172
178 x e q
Detach, 176, 177
179 f(x)=1 => x e q
4 Conclusion, 172
180 [x e q => f(x)=1] & [f(x)=1 => x e q]
Join, 171, 179
181 x e q <=> f(x)=1
Iff-And, 180
As Required:
182 ALL(c):[c e s => [c e q <=> f(c)=1]]
4 Conclusion, 162
183 (f,q) e fps
&
ALL(c):[c e s => [c e q <=> f(c)=1]]
Join, 161, 182
184 (f,q) e g
Detach, 154, 183
185 q e ps & (f,q) e g
Join, 149, 184
As Required:
186 EXIST(d):[d e ps & (f,d) e g]
E Gen, 185
Functionality - Part 2
187 ALL(c):[c e fsi =>
EXIST(d):[d e ps & (c,d) e g]]
4 Conclusion, 129
Suppose...
188 (x,y1) e g & (x,y2) e g
Premise
189 (x,y1) e g
Split, 188
190 (x,y2) e g
Split, 188
191 ALL(b):[(x,b) e g <=> (x,b) e fps & ALL(c):[c e s => [c e b <=> x(c)=1]]]
U Spec, 106
192 (x,y1) e g <=> (x,y1) e fps & ALL(c):[c e s => [c e y1 <=> x(c)=1]]
U Spec, 191
193 [(x,y1) e g => (x,y1) e fps & ALL(c):[c e s => [c e y1 <=> x(c)=1]]]
&
[(x,y1) e fps & ALL(c):[c e s => [c e y1 <=> x(c)=1]] => (x,y1) e g]
Iff-And, 192
194 (x,y1) e g => (x,y1) e fps & ALL(c):[c e s => [c e y1 <=> x(c)=1]]
Split, 193
195 (x,y1) e fps & ALL(c):[c e s => [c e y1 <=> x(c)=1]] => (x,y1) e g
Split, 193
196 (x,y1) e fps & ALL(c):[c e s => [c e y1 <=> x(c)=1]]
Detach, 194, 189
197 (x,y1) e fps
Split, 196
198 ALL(c):[c e s => [c e y1 <=> x(c)=1]]
Split, 196
199 (x,y2) e g <=> (x,y2) e fps & ALL(c):[c e s => [c e y2 <=> x(c)=1]]
U Spec, 191
200 [(x,y2) e g => (x,y2) e fps & ALL(c):[c e s => [c e y2 <=> x(c)=1]]]
&
[(x,y2) e fps & ALL(c):[c e s => [c e y2 <=> x(c)=1]] => (x,y2) e g]
Iff-And, 199
201 (x,y2) e g => (x,y2) e fps & ALL(c):[c e s => [c e y2 <=> x(c)=1]]
Split, 200
202 (x,y2) e fps & ALL(c):[c e s => [c e y2 <=> x(c)=1]] => (x,y2) e g
Split, 200
203 (x,y2) e fps & ALL(c):[c e s => [c e y2 <=> x(c)=1]]
Detach, 201, 190
204 (x,y2) e fps
Split, 203
205 ALL(c):[c e s => [c e y2 <=> x(c)=1]]
Split, 203
206 ALL(a):ALL(b):[Set(a) & Set(b) =>
[a=b <=> ALL(c):[c e a <=> c e b]]]
Set Equality
207 ALL(b):[Set(y1) & Set(b)
=> [y1=b <=> ALL(c):[c e y1 <=> c e b]]]
U Spec, 206
208 Set(y1) & Set(y2) => [y1=y2 <=> ALL(c):[c e y1 <=> c e y2]]
U Spec, 207
209 ALL(c2):[(x,c2) e fps <=> x e fsi & c2 e ps]
U Spec, 101
210 (x,y1) e fps <=> x e fsi & y1 e ps
U Spec, 209
211 [(x,y1) e fps => x e fsi & y1 e ps]
&
[x e fsi & y1 e ps => (x,y1) e fps]
Iff-And, 210
212 (x,y1) e fps => x e fsi & y1 e ps
Split, 211
213 x e fsi & y1 e ps => (x,y1) e fps
Split, 211
214 x e fsi & y1 e ps
Detach, 212, 197
215 x e fsi
Split, 214
216 y1 e ps
Split, 214
217 y1 e ps <=> Set(y1) & ALL(b):[b e y1 => b e s]
U Spec, 4
218 [y1 e ps => Set(y1) & ALL(b):[b e y1 => b e s]]
&
[Set(y1) & ALL(b):[b e y1 => b e s] => y1 e ps]
Iff-And, 217
219 y1 e ps => Set(y1) & ALL(b):[b e y1 => b e s]
Split, 218
220 Set(y1) & ALL(b):[b e y1 => b e s] => y1 e ps
Split, 218
221 Set(y1) & ALL(b):[b e y1 => b e s]
Detach, 219, 216
222 Set(y1)
Split, 221
223 ALL(b):[b e y1 => b e s]
Split, 221
224 (x,y2) e fps <=> x e fsi & y2 e ps
U Spec, 209
225 [(x,y2) e fps => x e fsi & y2 e ps]
&
[x e fsi & y2 e ps => (x,y2) e fps]
Iff-And, 224
226 (x,y2) e fps => x e fsi & y2 e ps
Split, 225
227 x e fsi & y2 e ps => (x,y2) e fps
Split, 225
228 x e fsi & y2 e ps
Detach, 226, 204
229 x e fsi
Split, 228
230 y2 e ps
Split, 228
231 y2 e ps <=> Set(y2) & ALL(b):[b e y2 => b e s]
U Spec, 4
232 [y2 e ps => Set(y2) & ALL(b):[b e y2 => b e s]]
&
[Set(y2) & ALL(b):[b e y2 => b e s] => y2 e ps]
Iff-And, 231
233 y2 e ps => Set(y2) & ALL(b):[b e y2 => b e s]
Split, 232
234 Set(y2) & ALL(b):[b e y2 => b e s] => y2 e ps
Split, 232
235 Set(y2) & ALL(b):[b e y2 => b e s]
Detach, 233, 230
236 Set(y2)
Split, 235
237 ALL(b):[b e y2 => b e s]
Split, 235
238 Set(y1) & Set(y2)
Join, 222, 236
239 y1=y2 <=> ALL(c):[c e y1 <=> c e y2]
Detach, 208, 238
240 [y1=y2 => ALL(c):[c e y1 <=> c e y2]]
&
[ALL(c):[c e y1 <=> c e y2] => y1=y2]
Iff-And, 239
241 y1=y2 => ALL(c):[c e y1 <=> c e y2]
Split, 240
Sufficient:
242 ALL(c):[c e y1 <=> c e y2] => y1=y2
Split, 240
Suppose...
243 t e y1
Premise
244 t e s => [t e y1 <=> x(t)=1]
U Spec, 198
245 t e y1 => t e s
U Spec, 223
246 t e s
Detach, 245, 243
247 t e y1 <=> x(t)=1
Detach, 244, 246
248 [t e y1 => x(t)=1] & [x(t)=1 => t e y1]
Iff-And, 247
249 t e y1 => x(t)=1
Split, 248
250 x(t)=1 => t e y1
Split, 248
251 x(t)=1
Detach, 249, 243
252 t e s => [t e y2 <=> x(t)=1]
U Spec, 205
253 t e y2 <=> x(t)=1
Detach, 252, 246
254 [t e y2 => x(t)=1] & [x(t)=1 => t e y2]
Iff-And, 253
255 t e y2 => x(t)=1
Split, 254
256 x(t)=1 => t e y2
Split, 254
257 t e y2
Detach, 256, 251
258 ALL(c):[c e y1 => c e y2]
4 Conclusion, 243
259 t e y2
Premise
260 t e s => [t e y2 <=> x(t)=1]
U Spec, 205
261 t e y2 => t e s
U Spec, 237
262 t e s
Detach, 261, 259
263 t e y2 <=> x(t)=1
Detach, 260, 262
264 [t e y2 => x(t)=1] & [x(t)=1 => t e y2]
Iff-And, 263
265 t e y2 => x(t)=1
Split, 264
266 x(t)=1 => t e y2
Split, 264
267 x(t)=1
Detach, 265, 259
268 t e s => [t e y1 <=> x(t)=1]
U Spec, 198
269 t e y1 <=> x(t)=1
Detach, 268, 262
270 [t e y1 => x(t)=1] & [x(t)=1 => t e y1]
Iff-And, 269
271 t e y1 => x(t)=1
Split, 270
272 x(t)=1 => t e y1
Split, 270
273 t e y1
Detach, 272, 267
274 ALL(c):[c e y2 => c e y1]
4 Conclusion, 259
275 ALL(c):[[c e y1 => c e y2] & [c e y2 => c e y1]]
Join, 258, 274
276 ALL(c):[c e y1 <=> c e y2]
Iff-And, 275
277 y1=y2
Detach, 242, 276
Functionality - Part 3
278 ALL(c):ALL(d1):ALL(d2):[(c,d1) e g & (c,d2) e g => d1=d2]
4 Conclusion, 188
279 ALL(c):ALL(d):[(c,d) e g => c e fsi & d e ps]
&
ALL(c):[c e fsi =>
EXIST(d):[d e ps & (c,d) e g]]
Join, 128, 187
280 ALL(c):ALL(d):[(c,d) e g => c e fsi & d e ps]
&
ALL(c):[c e fsi =>
EXIST(d):[d e ps & (c,d) e g]]
&
ALL(c):ALL(d1):ALL(d2):[(c,d1) e g & (c,d2) e g => d1=d2]
Join, 279, 278
g is a function
As Required:
281 ALL(c):ALL(d):[c e fsi & d e ps => [d=g(c) <=> (c,d) e g]]
Detach, 112, 280
282 f e fsi
Premise
283 f e fsi => EXIST(d):[d e ps & (f,d) e g]
U Spec, 187
284 EXIST(d):[d e ps & (f,d) e g]
Detach, 283, 282
285 x e ps & (f,x) e g
E Spec, 284
286 x e ps
Split, 285
287 (f,x) e g
Split, 285
288 ALL(d):[f e fsi & d e ps => [d=g(f) <=> (f,d) e g]]
U Spec, 281
289 f e fsi & x e ps => [x=g(f) <=> (f,x) e g]
U Spec, 288
290 f e fsi & x e ps
Join, 282, 286
291 x=g(f) <=> (f,x) e g
Detach, 289, 290
292 [x=g(f) => (f,x) e g] & [(f,x) e g => x=g(f)]
Iff-And, 291
293 x=g(f) => (f,x) e g
Split, 292
294 (f,x) e g => x=g(f)
Split, 292
295 x=g(f)
Detach, 294, 287
296 g(f) e ps
Substitute, 295,
286
As Required:
297 ALL(f):[f e fsi => g(f) e ps]
4 Conclusion, 282
Suppose...
298 f e fsi
Premise
299 f e fsi => EXIST(d):[d e ps & (f,d) e g]
U Spec, 187
300 EXIST(d):[d e ps & (f,d) e g]
Detach, 299, 298
301 x e ps & (f,x) e g
E Spec, 300
302 x e ps
Split, 301
303 (f,x) e g
Split, 301
304 ALL(d):[f e fsi & d e ps => [d=g(f) <=> (f,d) e g]]
U Spec, 281
305 f e fsi & x e ps => [x=g(f) <=> (f,x) e g]
U Spec, 304
306 f e fsi & x e ps
Join, 298, 302
307 x=g(f) <=> (f,x) e g
Detach, 305, 306
308 [x=g(f) => (f,x) e g] & [(f,x) e g => x=g(f)]
Iff-And, 307
309 x=g(f) => (f,x) e g
Split, 308
310 (f,x) e g => x=g(f)
Split, 308
311 x=g(f)
Detach, 310, 303
312 ALL(b):[(f,b) e g <=> (f,b) e fps & ALL(c):[c e s => [c e b <=> f(c)=1]]]
U Spec, 106
313 (f,x) e g <=> (f,x) e fps & ALL(c):[c e s => [c e x <=> f(c)=1]]
U Spec, 312
314 [(f,x) e g => (f,x) e fps & ALL(c):[c e s => [c e x <=> f(c)=1]]]
&
[(f,x) e fps & ALL(c):[c e s => [c e x <=> f(c)=1]] => (f,x) e g]
Iff-And, 313
315 (f,x) e g => (f,x) e fps & ALL(c):[c e s => [c e x <=> f(c)=1]]
Split, 314
316 (f,x) e fps & ALL(c):[c e s => [c e x <=> f(c)=1]] => (f,x) e g
Split, 314
317 (f,x) e fps & ALL(c):[c e s => [c e x <=> f(c)=1]]
Detach, 315, 303
318 (f,x) e fps
Split, 317
319 ALL(c):[c e s => [c e x <=> f(c)=1]]
Split, 317
320 ALL(c):[c e s => [c e g(f) <=> f(c)=1]]
Substitute, 311,
319
As Required:
321 ALL(f):[f e fsi => ALL(c):[c e s => [c e g(f) <=> f(c)=1]]]
4 Conclusion, 298
Prove: g is surjective i.e. ALL(a):[a e ps => EXIST(f):[f e fsi &
g(f)=a] (f defined below)
x x
Suppose x is a subset of s (find the pre-image of s under g)
322 x e ps
Premise
323 x e ps <=> Set(x) & ALL(b):[b e x => b e s]
U Spec, 4
324 [x e ps => Set(x) & ALL(b):[b e x => b e s]]
&
[Set(x) & ALL(b):[b e x => b e s] => x e ps]
Iff-And, 323
325 x e ps => Set(x) & ALL(b):[b e x => b e s]
Split, 324
326 Set(x) & ALL(b):[b e x => b e s] => x e ps
Split, 324
327 Set(x) & ALL(b):[b e x => b e s]
Detach, 325, 322
328 Set(x)
Split, 327
329 ALL(b):[b e x => b e s]
Split, 327
330 EXIST(sub):[Set'(sub) &
ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e si & [a e x & b=1 | ~a e x & b=0]]]
Subset, 28
331 Set'(f) & ALL(a):ALL(b):[(a,b) e f <=> (a,b) e si & [a e x & b=1 | ~a e x & b=0]]
E Spec, 330
Define: f
(the supposed pre-image of x under g)
*********
f: s --> {0,
1}
f(a) = 1 if a e x, 0 otherwise
332 Set'(f)
Split, 331
333 ALL(a):ALL(b):[(a,b) e f <=> (a,b) e si & [a e x & b=1 | ~a e x & b=0]]
Split, 331
334 f e fsi => ALL(c):[c e s => [c e g(f) <=> f(c)=1]]
U Spec, 321
335 f e fsi <=> f e psi & [ALL(b):[b e s => EXIST(c):[c e i & (b,c) e f]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e f & (b,d) e f => c=d]]
U Spec, 39
336 [f e fsi => f e psi & [ALL(b):[b e s => EXIST(c):[c e i & (b,c) e f]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e f & (b,d) e f => c=d]]]
&
[f e psi & [ALL(b):[b e s => EXIST(c):[c e i & (b,c) e f]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e f & (b,d) e f => c=d]] => f e fsi]
Iff-And, 335
337 f e fsi => f e psi & [ALL(b):[b e s => EXIST(c):[c e i & (b,c) e f]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e f & (b,d) e f => c=d]]
Split, 336
Sufficient: For f e fsi
338 f e psi & [ALL(b):[b e s => EXIST(c):[c e i & (b,c) e f]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e f & (b,d) e f => c=d]] => f e fsi
Split, 336
339 f e psi <=> Set'(f) & ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e si]
U Spec, 35
340 [f e psi => Set'(f) & ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e si]]
&
[Set'(f) & ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e si] => f e psi]
Iff-And, 339
341 f e psi => Set'(f) & ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e si]
Split, 340
Sufficient: For f e psi
342 Set'(f) & ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e si] => f e psi
Split, 340
343 (t,u) e f
Premise
344 ALL(b):[(t,b) e f <=> (t,b) e si & [t e x & b=1 | ~t e x & b=0]]
U Spec, 333
345 (t,u) e f <=> (t,u) e si & [t e x & u=1 | ~t e x & u=0]
U Spec, 344
346 [(t,u) e f => (t,u) e si & [t e x & u=1 | ~t e x & u=0]]
&
[(t,u) e si & [t e x & u=1 | ~t e x & u=0] => (t,u) e f]
Iff-And, 345
347 (t,u) e f => (t,u) e si & [t e x & u=1 | ~t e x & u=0]
Split, 346
348 (t,u) e si & [t e x & u=1 | ~t e x & u=0] => (t,u) e f
Split, 346
349 (t,u) e si & [t e x & u=1 | ~t e x & u=0]
Detach, 347, 343
350 (t,u) e si
Split, 349
351 ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e si]
4 Conclusion, 343
352 Set'(f)
&
ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e si]
Join, 332, 351
As Required:
353 f e psi
Detach, 342, 352
Suppose...
354 t e s
Premise
Two cases:
355 t e x | ~t e x
Or Not
Case 1
356 t e x
Premise
357 1 e i <=> 1=0 | 1=1
U Spec, 6
358 [1 e i => 1=0 | 1=1] & [1=0 | 1=1 => 1 e i]
Iff-And, 357
359 1 e i => 1=0 | 1=1
Split, 358
360 1=0 | 1=1 => 1 e i
Split, 358
361 1=1
Reflex
362 1=0 | 1=1
Arb Or, 361
363 1 e i
Detach, 360, 362
364 ALL(b):[(t,b) e f <=> (t,b) e si & [t e x & b=1 | ~t e x & b=0]]
U Spec, 333
365 (t,1) e f <=> (t,1) e si & [t e x & 1=1 | ~t e x & 1=0]
U Spec, 364
366 [(t,1) e f => (t,1) e si & [t e x & 1=1 | ~t e x & 1=0]]
&
[(t,1) e si & [t e x & 1=1 | ~t e x & 1=0] => (t,1) e f]
Iff-And, 365
367 (t,1) e f => (t,1) e si & [t e x & 1=1 | ~t e x & 1=0]
Split, 366
Sufficient: For (t,1) e f
368 (t,1) e si & [t e x & 1=1 | ~t e x & 1=0] => (t,1) e f
Split, 366
369 ALL(c2):[(t,c2) e si <=> t e s & c2 e i]
U Spec, 29
370 (t,1) e si <=> t e s & 1 e i
U Spec, 369
371 [(t,1) e si => t e s & 1 e i]
&
[t e s & 1 e i => (t,1) e si]
Iff-And, 370
372 (t,1) e si => t e s & 1 e i
Split, 371
373 t e s & 1 e i => (t,1) e si
Split, 371
374 t e s & 1 e i
Join, 354, 363
375 (t,1) e si
Detach, 373, 374
376 1=1
Reflex
377 t e x & 1=1
Join, 356, 376
378 t e x & 1=1 | ~t e x & 1=0
Arb Or, 377
379 (t,1) e si & [t e x & 1=1 | ~t e x & 1=0]
Join, 375, 378
380 (t,1) e f
Detach, 368, 379
381 1 e i & (t,1) e f
Join, 363, 380
382 EXIST(c):[c e i & (t,c) e f]
E Gen, 381
383 t e x => EXIST(c):[c e i & (t,c) e f]
4 Conclusion, 356
Case 2
384 ~t e x
Premise
385 0 e i <=> 0=0 | 0=1
U Spec, 6
386 [0 e i => 0=0 | 0=1] & [0=0 | 0=1 => 0 e i]
Iff-And, 385
387 0 e i => 0=0 | 0=1
Split, 386
388 0=0 | 0=1 => 0 e i
Split, 386
389 0=0
Reflex
390 0=0 | 0=1
Arb Or, 389
391 0 e i
Detach, 388, 390
392 ALL(b):[(t,b) e f <=> (t,b) e si & [t e x & b=1 | ~t e x & b=0]]
U Spec, 333
393 (t,0) e f <=> (t,0) e si & [t e x & 0=1 | ~t e x & 0=0]
U Spec, 392
394 [(t,0) e f => (t,0) e si & [t e x & 0=1 | ~t e x & 0=0]]
&
[(t,0) e si & [t e x & 0=1 | ~t e x & 0=0] => (t,0) e f]
Iff-And, 393
395 (t,0) e f => (t,0) e si & [t e x & 0=1 | ~t e x & 0=0]
Split, 394
Sufficient:
396 (t,0) e si & [t e x & 0=1 | ~t e x & 0=0] => (t,0) e f
Split, 394
397 ALL(c2):[(t,c2) e si <=> t e s & c2 e i]
U Spec, 29
398 (t,0) e si <=> t e s & 0 e i
U Spec, 397
399 [(t,0) e si => t e s & 0 e i]
&
[t e s & 0 e i => (t,0) e si]
Iff-And, 398
400 (t,0) e si => t e s & 0 e i
Split, 399
Sufficient:
401 t e s & 0 e i => (t,0) e si
Split, 399
402 t e s & 0 e i
Join, 354, 391
403 (t,0) e si
Detach, 401, 402
404 0=0
Reflex
405 ~t e x & 0=0
Join, 384, 404
406 t e x & 0=1 | ~t e x & 0=0
Arb Or, 405
407 (t,0) e si & [t e x & 0=1 | ~t e x & 0=0]
Join, 403, 406
408 (t,0) e f
Detach, 396, 407
409 0 e i & (t,0) e f
Join, 391, 408
410 EXIST(c):[c e i & (t,c) e f]
E Gen, 409
As Required:
411 ~t e x => EXIST(c):[c e i & (t,c) e f]
4 Conclusion, 384
412 [t e x => EXIST(c):[c e i & (t,c) e f]]
&
[~t e x => EXIST(c):[c e i & (t,c) e f]]
Join, 383, 411
413 EXIST(c):[c e i & (t,c) e f]
Cases, 355, 412
As Required:
414 ALL(b):[b e s => EXIST(c):[c e i & (b,c) e f]]
4 Conclusion, 354
Suppose...
415 (t,u1) e f & (t,u2) e f
Premise
416 (t,u1) e f
Split, 415
417 (t,u2) e f
Split, 415
418 ALL(b):[(t,b) e f <=> (t,b) e si & [t e x & b=1 | ~t e x & b=0]]
U Spec, 333
419 (t,u1) e f <=> (t,u1) e si & [t e x & u1=1 | ~t e x & u1=0]
U Spec, 418
420 [(t,u1) e f => (t,u1) e si & [t e x & u1=1 | ~t e x & u1=0]]
&
[(t,u1) e si & [t e x & u1=1 | ~t e x & u1=0] => (t,u1) e f]
Iff-And, 419
421 (t,u1) e f => (t,u1) e si & [t e x & u1=1 | ~t e x & u1=0]
Split, 420
422 (t,u1) e si & [t e x & u1=1 | ~t e x & u1=0] => (t,u1) e f
Split, 420
423 (t,u1) e si & [t e x & u1=1 | ~t e x & u1=0]
Detach, 421, 416
424 (t,u1) e si
Split, 423
425 t e x & u1=1 | ~t e x & u1=0
Split, 423
426 ~[t e x & u1=1] => ~t e x & u1=0
Imply-Or, 425
427 ~[~t e x & u1=0] => ~~[t e x & u1=1]
Contra, 426
428 ~[~t e x & u1=0] => t e x & u1=1
Rem DNeg, 427
429 ~[t e x & u1=1] => ~~[~t e x & u1=0]
Contra, 428
430 ~[t e x & u1=1] => ~t e x & u1=0
Rem DNeg, 429
431 (t,u2) e f <=> (t,u2) e si & [t e x & u2=1 | ~t e x & u2=0]
U Spec, 418
432 [(t,u2) e f => (t,u2) e si & [t e x & u2=1 | ~t e x & u2=0]]
&
[(t,u2) e si & [t e x & u2=1 | ~t e x & u2=0] => (t,u2) e f]
Iff-And, 431
433 (t,u2) e f => (t,u2) e si & [t e x & u2=1 | ~t e x & u2=0]
Split, 432
434 (t,u2) e si & [t e x & u2=1 | ~t e x & u2=0] => (t,u2) e f
Split, 432
435 (t,u2) e si & [t e x & u2=1 | ~t e x & u2=0]
Detach, 433, 417
436 (t,u2) e si
Split, 435
437 t e x & u2=1 | ~t e x & u2=0
Split, 435
438 ~[t e x & u2=1] => ~t e x & u2=0
Imply-Or, 437
439 ~[~t e x & u2=0] => ~~[t e x & u2=1]
Contra, 438
440 ~[~t e x & u2=0] => t e x & u2=1
Rem DNeg, 439
441 ~[t e x & u2=1] => ~~[~t e x & u2=0]
Contra, 440
442 ~[t e x & u2=1] => ~t e x & u2=0
Rem DNeg, 441
Two cases:
443 t e x | ~t e x
Or Not
Case 1
444 t e x
Premise
445 ~t e x & u1=0
Premise
446 ~t e x
Split, 445
447 u1=0
Split, 445
448 t e x & ~t e x
Join, 444, 446
449 ~[~t e x & u1=0]
4 Conclusion, 445
450 t e x & u1=1
Detach, 428, 449
451 t e x
Split, 450
452 u1=1
Split, 450
453 ~t e x & u2=0
Premise
454 ~t e x
Split, 453
455 u2=0
Split, 453
456 t e x & ~t e x
Join, 451, 454
457 ~[~t e x & u2=0]
4 Conclusion, 453
458 t e x & u2=1
Detach, 440, 457
459 t e x
Split, 458
460 u2=1
Split, 458
461 u1=u2
Substitute, 460,
452
462 t e x => u1=u2
4 Conclusion, 444
Case 2
463 ~t e x
Premise
464 t e x & u1=1
Premise
465 t e x
Split, 464
466 u1=1
Split, 464
467 t e x & ~t e x
Join, 465, 463
468 ~[t e x & u1=1]
4 Conclusion, 464
469 ~t e x & u1=0
Detach, 430, 468
470 ~t e x
Split, 469
471 u1=0
Split, 469
472 t e x & u2=1
Premise
473 t e x
Split, 472
474 u2=1
Split, 472
475 t e x & ~t e x
Join, 473, 463
476 ~[t e x & u2=1]
4 Conclusion, 472
477 ~t e x & u2=0
Detach, 442, 476
478 ~t e x
Split, 477
479 u2=0
Split, 477
480 u1=u2
Substitute, 479,
471
481 ~t e x => u1=u2
4 Conclusion, 463
482 [t e x => u1=u2] & [~t e x => u1=u2]
Join, 462, 481
483 u1=u2
Cases, 443, 482
As Required:
484 ALL(b):ALL(c):ALL(d):[(b,c) e f & (b,d) e f => c=d]
4 Conclusion, 415
485 ALL(b):[b e s =>
EXIST(c):[c e i & (b,c) e f]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e f & (b,d) e f => c=d]
Join, 414, 484
486 f e psi
&
[ALL(b):[b e s =>
EXIST(c):[c e i & (b,c) e f]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e f & (b,d) e f => c=d]]
Join, 353, 485
As Required:
487 f e fsi
Detach, 338, 486
488 f e fsi => ALL(c):[c e s => [c e g(f) <=> f(c)=1]]
U Spec, 321
489 ALL(b):[(f,b) e g <=> (f,b) e fps & ALL(c):[c e s => [c e b <=> f(c)=1]]]
U Spec, 106
490 (f,x) e g <=> (f,x) e fps & ALL(c):[c e s => [c e x <=> f(c)=1]]
U Spec, 489
491 [(f,x) e g => (f,x) e fps & ALL(c):[c e s => [c e x <=> f(c)=1]]]
&
[(f,x) e fps & ALL(c):[c e s => [c e x <=> f(c)=1]] => (f,x) e g]
Iff-And, 490
492 (f,x) e g => (f,x) e fps & ALL(c):[c e s => [c e x <=> f(c)=1]]
Split, 491
Sufficient: For (f,x) e g
493 (f,x) e fps & ALL(c):[c e s => [c e x <=> f(c)=1]] => (f,x) e g
Split, 491
494 ALL(c2):[(f,c2) e fps <=> f e fsi & c2 e ps]
U Spec, 101
495 (f,x) e fps <=> f e fsi & x e ps
U Spec, 494
496 [(f,x) e fps => f e fsi & x e ps]
&
[f e fsi & x e ps => (f,x) e fps]
Iff-And, 495
497 (f,x) e fps => f e fsi & x e ps
Split, 496
498 f e fsi & x e ps => (f,x) e fps
Split, 496
499 f e fsi & x e ps
Join, 487, 322
As Required:
500 (f,x) e fps
Detach, 498, 499
501 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, 1
502 ALL(b):[Set'(f) & Set(s) & Set(b)
=>
[ALL(c):ALL(d):[(c,d) e f => c e s & d e b]
&
ALL(c):[c e s =>
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 s & d e b => [d=f(c) <=> (c,d) e f]]]]
U Spec, 501
503 Set'(f) & Set(s) & Set(i)
=>
[ALL(c):ALL(d):[(c,d) e f => c e s & d e i]
&
ALL(c):[c e s =>
EXIST(d):[d e i & (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 s & d e i => [d=f(c) <=> (c,d) e f]]]
U Spec, 502
504 Set'(f) & Set(s)
Join, 332, 2
505 Set'(f) & Set(s) & Set(i)
Join, 504, 5
Sufficient: For functionality of f
506 ALL(c):ALL(d):[(c,d) e f => c e s & d e i]
&
ALL(c):[c e s =>
EXIST(d):[d e i & (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 s & d e i => [d=f(c) <=> (c,d) e f]]
Detach, 503, 505
507 (u,v) e f
Premise
508 ALL(b):[(u,b) e f <=> (u,b) e si & [u e x & b=1 | ~u e x & b=0]]
U Spec, 333
509 (u,v) e f <=> (u,v) e si & [u e x & v=1 | ~u e x & v=0]
U Spec, 508
510 [(u,v) e f => (u,v) e si & [u e x & v=1 | ~u e x & v=0]]
&
[(u,v) e si & [u e x & v=1 | ~u e x & v=0] => (u,v) e f]
Iff-And, 509
511 (u,v) e f => (u,v) e si & [u e x & v=1 | ~u e x & v=0]
Split, 510
512 (u,v) e si & [u e x & v=1 | ~u e x & v=0] => (u,v) e f
Split, 510
513 (u,v) e si & [u e x & v=1 | ~u e x & v=0]
Detach, 511, 507
514 (u,v) e si
Split, 513
515 u e x & v=1 | ~u e x & v=0
Split, 513
516 ALL(c2):[(u,c2) e si <=> u e s & c2 e i]
U Spec, 29
517 (u,v) e si <=> u e s & v e i
U Spec, 516
518 [(u,v) e si => u e s & v e i]
& [u e s & v e i => (u,v) e si]
Iff-And, 517
519 (u,v) e si => u e s & v e i
Split, 518
520 u e s & v e i => (u,v) e si
Split, 518
521 u e s & v e i
Detach, 519, 514
Part 1
522 ALL(c):ALL(d):[(c,d) e f => c e s & d e i]
4 Conclusion, 507
523 ALL(c):ALL(d):[(c,d) e f => c e s & d e i]
&
ALL(b):[b e s =>
EXIST(c):[c e i & (b,c) e f]]
Join, 522, 414
524 ALL(c):ALL(d):[(c,d) e f => c e s & d e i]
&
ALL(b):[b e s =>
EXIST(c):[c e i & (b,c) e f]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e f & (b,d) e f => c=d]
Join, 523, 484
f is a function
As Required:
525 ALL(c):ALL(d):[c e s & d e i => [d=f(c) <=> (c,d) e f]]
Detach, 506, 524
526 t e s
Premise
527 t e x
Premise
528 ALL(b):[(t,b) e f <=> (t,b) e si & [t e x & b=1 | ~t e x & b=0]]
U Spec, 333
529 (t,1) e f <=> (t,1) e si & [t e x & 1=1 | ~t e x & 1=0]
U Spec, 528
530 [(t,1) e f => (t,1) e si & [t e x & 1=1 | ~t e x & 1=0]]
&
[(t,1) e si & [t e x & 1=1 | ~t e x & 1=0] => (t,1) e f]
Iff-And, 529
531 (t,1) e f => (t,1) e si & [t e x & 1=1 | ~t e x & 1=0]
Split, 530
532 (t,1) e si & [t e x & 1=1 | ~t e x & 1=0] => (t,1) e f
Split, 530
533 ALL(c2):[(t,c2) e si <=> t e s & c2 e i]
U Spec, 29
534 (t,1) e si <=> t e s & 1 e i
U Spec, 533
535 [(t,1) e si => t e s & 1 e i]
&
[t e s & 1 e i => (t,1) e si]
Iff-And, 534
536 (t,1) e si => t e s & 1 e i
Split, 535
537 t e s & 1 e i => (t,1) e si
Split, 535
538 t e s & 1 e i
Join, 526, 21
539 (t,1) e si
Detach, 537, 538
540 1=1
Reflex
541 t e x & 1=1
Join, 527, 540
542 t e x & 1=1 | ~t e x & 1=0
Arb Or, 541
543 (t,1) e si & [t e x & 1=1 | ~t e x & 1=0]
Join, 539, 542
544 (t,1) e f
Detach, 532, 543
545 ALL(d):[t e s & d e i => [d=f(t) <=> (t,d) e f]]
U Spec, 525
546 t e s & 1 e i => [1=f(t) <=> (t,1) e f]
U Spec, 545
547 t e s & 1 e i
Join, 526, 21
548 1=f(t) <=> (t,1) e f
Detach, 546, 547
549 [1=f(t) => (t,1) e f] & [(t,1) e f => 1=f(t)]
Iff-And, 548
550 1=f(t) => (t,1) e f
Split, 549
551 (t,1) e f => 1=f(t)
Split, 549
552 1=f(t)
Detach, 551, 544
553 f(t)=1
Sym, 552
554 t e x => f(t)=1
4 Conclusion, 527
Suppose...
555 f(t)=1
Premise
556 ALL(b):[(t,b) e f <=> (t,b) e si & [t e x & b=1 | ~t e x & b=0]]
U Spec, 333
557 (t,1) e f <=> (t,1) e si & [t e x & 1=1 | ~t e x & 1=0]
U Spec, 556
558 [(t,1) e f => (t,1) e si & [t e x & 1=1 | ~t e x & 1=0]]
&
[(t,1) e si & [t e x & 1=1 | ~t e x & 1=0] => (t,1) e f]
Iff-And, 557
559 (t,1) e f => (t,1) e si & [t e x & 1=1 | ~t e x & 1=0]
Split, 558
560 (t,1) e si & [t e x & 1=1 | ~t e x & 1=0] => (t,1) e f
Split, 558
561 ALL(d):[t e s & d e i => [d=f(t) <=> (t,d) e f]]
U Spec, 525
562 t e s & 1 e i => [1=f(t) <=> (t,1) e f]
U Spec, 561
563 t e s & 1 e i
Join, 526, 21
564 1=f(t) <=> (t,1) e f
Detach, 562, 563
565 [1=f(t) => (t,1) e f] & [(t,1) e f => 1=f(t)]
Iff-And, 564
566 1=f(t) => (t,1) e f
Split, 565
567 (t,1) e f => 1=f(t)
Split, 565
568 f(t)=1 => (t,1) e f
Sym, 566
569 (t,1) e f
Detach, 568, 555
570 (t,1) e si & [t e x & 1=1 | ~t e x & 1=0]
Detach, 559, 569
571 (t,1) e si
Split, 570
572 t e x & 1=1 | ~t e x & 1=0
Split, 570
573 ~[t e x & 1=1] => ~t e x & 1=0
Imply-Or, 572
574 ~[~t e x & 1=0] => ~~[t e x & 1=1]
Contra, 573
575 ~[~t e x & 1=0] => t e x & 1=1
Rem DNeg, 574
576 ~t e x & 1=0
Premise
577 ~t e x
Split, 576
578 1=0
Split, 576
579 0=1
Sym, 578
580 0=1 & ~0=1
Join, 579, 7
581 ~[~t e x & 1=0]
4 Conclusion, 576
582 t e x & 1=1
Detach, 575, 581
583 t e x
Split, 582
584 f(t)=1 => t e x
4 Conclusion, 555
585 [t e x => f(t)=1] & [f(t)=1 => t e x]
Join, 554, 584
586 t e x <=> f(t)=1
Iff-And, 585
587 ALL(c):[c e s => [c e x <=> f(c)=1]]
4 Conclusion, 526
588 (f,x) e fps
&
ALL(c):[c e s => [c e x <=> f(c)=1]]
Join, 500, 587
589 (f,x) e g
Detach, 493, 588
590 ALL(d):[f e fsi & d e ps => [d=g(f) <=> (f,d) e g]]
U Spec, 281
591 f e fsi & x e ps => [x=g(f) <=> (f,x) e g]
U Spec, 590
592 f e fsi & x e ps
Join, 487, 322
593 x=g(f) <=> (f,x) e g
Detach, 591, 592
594 [x=g(f) => (f,x) e g] & [(f,x) e g => x=g(f)]
Iff-And, 593
595 x=g(f) => (f,x) e g
Split, 594
596 (f,x) e g => x=g(f)
Split, 594
597 x=g(f)
Detach, 596, 589
598 g(f)=x
Sym, 597
599 f e fsi & g(f)=x
Join, 487, 598
*******************
g is surjective
*******************
600 ALL(a):[a e ps =>
EXIST(f):[f e fsi & g(f)=a]]
4 Conclusion, 322
Prove: g is injective
Suppose f1 and f2 are such that f1: s --> i and f2: s --> i
601 f1 e fsi & f2 e fsi
Premise
602 f1 e fsi
Split, 601
603 f2 e fsi
Split, 601
604 f1 e fsi <=> f1 e psi & [ALL(b):[b e s => EXIST(c):[c e i & (b,c) e f1]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e f1 & (b,d) e f1 => c=d]]
U Spec, 39
605 [f1 e fsi => f1 e psi & [ALL(b):[b e s => EXIST(c):[c e i & (b,c) e f1]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e f1 & (b,d) e f1 => c=d]]]
&
[f1 e psi & [ALL(b):[b e s => EXIST(c):[c e i & (b,c) e f1]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e f1 & (b,d) e f1 => c=d]] => f1 e fsi]
Iff-And, 604
606 f1 e fsi => f1 e psi & [ALL(b):[b e s => EXIST(c):[c e i & (b,c) e f1]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e f1 & (b,d) e f1 => c=d]]
Split, 605
607 f1 e psi & [ALL(b):[b e s => EXIST(c):[c e i & (b,c) e f1]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e f1 & (b,d) e f1 => c=d]] => f1 e fsi
Split, 605
608 f1 e psi & [ALL(b):[b e s => EXIST(c):[c e i & (b,c) e f1]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e f1 & (b,d) e f1 => c=d]]
Detach, 606, 602
609 f1 e psi
Split, 608
610 ALL(b):[b e s =>
EXIST(c):[c e i & (b,c) e f1]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e f1 & (b,d) e f1 => c=d]
Split, 608
611 ALL(b):[b e s =>
EXIST(c):[c e i & (b,c) e f1]]
Split, 610
612 ALL(b):ALL(c):ALL(d):[(b,c) e f1 & (b,d) e f1 => c=d]
Split, 610
613 f1 e psi <=> Set'(f1) & ALL(d1):ALL(d2):[(d1,d2) e f1 => (d1,d2) e si]
U Spec, 35
614 [f1 e psi => Set'(f1) & ALL(d1):ALL(d2):[(d1,d2) e f1 => (d1,d2) e si]]
&
[Set'(f1) & ALL(d1):ALL(d2):[(d1,d2) e f1 => (d1,d2) e si] => f1 e psi]
Iff-And, 613
615 f1 e psi => Set'(f1) & ALL(d1):ALL(d2):[(d1,d2) e f1 => (d1,d2) e si]
Split, 614
616 Set'(f1) & ALL(d1):ALL(d2):[(d1,d2) e f1 => (d1,d2) e si] => f1 e psi
Split, 614
617 Set'(f1) & ALL(d1):ALL(d2):[(d1,d2) e f1 => (d1,d2) e si]
Detach, 615, 609
618 Set'(f1)
Split, 617
619 ALL(d1):ALL(d2):[(d1,d2) e f1 => (d1,d2) e si]
Split, 617
620 (t,u) e f1
Premise
621 ALL(d2):[(t,d2) e f1 => (t,d2) e si]
U Spec, 619
622 (t,u) e f1 => (t,u) e si
U Spec, 621
623 (t,u) e si
Detach, 622, 620
624 ALL(c2):[(t,c2) e si <=> t e s & c2 e i]
U Spec, 29
625 (t,u) e si <=> t e s & u e i
U Spec, 624
626 [(t,u) e si => t e s & u e i]
&
[t e s & u e i => (t,u) e si]
Iff-And, 625
627 (t,u) e si => t e s & u e i
Split, 626
628 t e s & u e i => (t,u) e si
Split, 626
629 t e s & u e i
Detach, 627, 623
630 ALL(c):ALL(d):[(c,d) e f1 => c e s & d e i]
4 Conclusion, 620
631 ALL(a):ALL(b):[Set'(f1) & Set(a)
& Set(b)
=>
[ALL(c):ALL(d):[(c,d) e f1 => c e a & d e b]
&
ALL(c):[c e a =>
EXIST(d):[d e b & (c,d) e f1]]
&
ALL(c):ALL(d1):ALL(d2):[(c,d1) e f1 & (c,d2) e f1 => d1=d2]
=>
ALL(c):ALL(d):[c e a & d e b => [d=f1(c) <=> (c,d) e f1]]]]
U Spec, 1
632 ALL(b):[Set'(f1) & Set(s) & Set(b)
=>
[ALL(c):ALL(d):[(c,d) e f1 => c e s & d e b]
&
ALL(c):[c e s =>
EXIST(d):[d e b & (c,d) e f1]]
&
ALL(c):ALL(d1):ALL(d2):[(c,d1) e f1 & (c,d2) e f1 => d1=d2]
=>
ALL(c):ALL(d):[c e s & d e b => [d=f1(c) <=> (c,d) e f1]]]]
U Spec, 631
633 Set'(f1) & Set(s) & Set(i)
=>
[ALL(c):ALL(d):[(c,d) e f1 => c e s & d e i]
&
ALL(c):[c e s =>
EXIST(d):[d e i & (c,d) e f1]]
&
ALL(c):ALL(d1):ALL(d2):[(c,d1) e f1 & (c,d2) e f1 => d1=d2]
=>
ALL(c):ALL(d):[c e s & d e i => [d=f1(c) <=> (c,d) e f1]]]
U Spec, 632
634 Set'(f1) & Set(s)
Join, 618, 2
635 Set'(f1) & Set(s) & Set(i)
Join, 634, 5
636 ALL(c):ALL(d):[(c,d) e f1 => c e s & d e i]
&
ALL(c):[c e s =>
EXIST(d):[d e i & (c,d) e f1]]
&
ALL(c):ALL(d1):ALL(d2):[(c,d1) e f1 & (c,d2) e f1 => d1=d2]
=>
ALL(c):ALL(d):[c e s & d e i => [d=f1(c) <=> (c,d) e f1]]
Detach, 633, 635
637 ALL(c):ALL(d):[(c,d) e f1 => c e s & d e i]
&
ALL(b):[b e s =>
EXIST(c):[c e i & (b,c) e f1]]
Join, 630, 611
638 ALL(c):ALL(d):[(c,d) e f1 => c e s & d e i]
&
ALL(b):[b e s =>
EXIST(c):[c e i & (b,c) e f1]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e f1 & (b,d) e f1 => c=d]
Join, 637, 612
f1 is a function
639 ALL(c):ALL(d):[c e s & d e i => [d=f1(c) <=>
(c,d) e f1]]
Detach, 636, 638
640 t e s
Premise
641 t e s => EXIST(c):[c e i & (t,c) e f1]
U Spec, 611
642 EXIST(c):[c e i & (t,c) e f1]
Detach, 641, 640
643 u e i & (t,u) e f1
E Spec, 642
644 u e i
Split, 643
645 (t,u) e f1
Split, 643
646 ALL(d):[t e s & d e i => [d=f1(t) <=> (t,d) e f1]]
U Spec, 639
647 t e s & u e i => [u=f1(t) <=> (t,u) e f1]
U Spec, 646
648 t e s & u e i
Join, 640, 644
649 u=f1(t) <=> (t,u) e f1
Detach, 647, 648
650 [u=f1(t) => (t,u) e f1] & [(t,u) e f1 => u=f1(t)]
Iff-And, 649
651 u=f1(t) => (t,u) e f1
Split, 650
652 (t,u) e f1 => u=f1(t)
Split, 650
653 u=f1(t)
Detach, 652, 645
654 f1(t) e i
Substitute, 653,
644
f1: s --> i
655 ALL(a):[a e s => f1(a) e i]
4 Conclusion, 640
656 f2 e fsi <=> f2 e psi & [ALL(b):[b e s => EXIST(c):[c e i & (b,c) e f2]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e f2 & (b,d) e f2 => c=d]]
U Spec, 39
657 [f2 e fsi => f2 e psi & [ALL(b):[b e s => EXIST(c):[c e i & (b,c) e f2]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e f2 & (b,d) e f2 => c=d]]]
&
[f2 e psi & [ALL(b):[b e s => EXIST(c):[c e i & (b,c) e f2]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e f2 & (b,d) e f2 => c=d]] => f2 e fsi]
Iff-And, 656
658 f2 e fsi => f2 e psi & [ALL(b):[b e s => EXIST(c):[c e i & (b,c) e f2]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e f2 & (b,d) e f2 => c=d]]
Split, 657
659 f2 e psi & [ALL(b):[b e s => EXIST(c):[c e i & (b,c) e f2]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e f2 & (b,d) e f2 => c=d]] => f2 e fsi
Split, 657
660 f2 e psi & [ALL(b):[b e s => EXIST(c):[c e i & (b,c) e f2]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e f2 & (b,d) e f2 => c=d]]
Detach, 658, 603
661 f2 e psi
Split, 660
662 ALL(b):[b e s =>
EXIST(c):[c e i & (b,c) e f2]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e f2 & (b,d) e f2 => c=d]
Split, 660
663 ALL(b):[b e s =>
EXIST(c):[c e i & (b,c) e f2]]
Split, 662
664 ALL(b):ALL(c):ALL(d):[(b,c) e f2 & (b,d) e f2 => c=d]
Split, 662
665 f2 e psi <=> Set'(f2) & ALL(d1):ALL(d2):[(d1,d2) e f2 => (d1,d2) e si]
U Spec, 35
666 [f2 e psi => Set'(f2) & ALL(d1):ALL(d2):[(d1,d2) e f2 => (d1,d2) e si]]
&
[Set'(f2) & ALL(d1):ALL(d2):[(d1,d2) e f2 => (d1,d2) e si] => f2 e psi]
Iff-And, 665
667 f2 e psi => Set'(f2) & ALL(d1):ALL(d2):[(d1,d2) e f2 => (d1,d2) e si]
Split, 666
668 Set'(f2) & ALL(d1):ALL(d2):[(d1,d2) e f2 => (d1,d2) e si] => f2 e psi
Split, 666
669 Set'(f2) & ALL(d1):ALL(d2):[(d1,d2) e f2 => (d1,d2) e si]
Detach, 667, 661
670 Set'(f2)
Split, 669
671 ALL(d1):ALL(d2):[(d1,d2) e f2 => (d1,d2) e si]
Split, 669
672 ALL(a):ALL(b):[Set'(f2) & Set(a)
& Set(b)
=>
[ALL(c):ALL(d):[(c,d) e f2 => c e a & d e b]
&
ALL(c):[c e a =>
EXIST(d):[d e b & (c,d) e f2]]
&
ALL(c):ALL(d1):ALL(d2):[(c,d1) e f2 & (c,d2) e f2 => d1=d2]
=>
ALL(c):ALL(d):[c e a & d e b => [d=f2(c) <=> (c,d) e f2]]]]
U Spec, 1
673 ALL(b):[Set'(f2) & Set(s) & Set(b)
=>
[ALL(c):ALL(d):[(c,d) e f2 => c e s & d e b]
&
ALL(c):[c e s =>
EXIST(d):[d e b & (c,d) e f2]]
&
ALL(c):ALL(d1):ALL(d2):[(c,d1) e f2 & (c,d2) e f2 => d1=d2]
=>
ALL(c):ALL(d):[c e s & d e b => [d=f2(c) <=> (c,d) e f2]]]]
U Spec, 672
674 Set'(f2) & Set(s) & Set(i)
=>
[ALL(c):ALL(d):[(c,d) e f2 => c e s & d e i]
&
ALL(c):[c e s =>
EXIST(d):[d e i & (c,d) e f2]]
&
ALL(c):ALL(d1):ALL(d2):[(c,d1) e f2 & (c,d2) e f2 => d1=d2]
=>
ALL(c):ALL(d):[c e s & d e i => [d=f2(c) <=> (c,d) e f2]]]
U Spec, 673
675 Set'(f2) & Set(s)
Join, 670, 2
676 Set'(f2) & Set(s) & Set(i)
Join, 675, 5
Sufficient:
677 ALL(c):ALL(d):[(c,d) e f2 => c e s & d e i]
&
ALL(c):[c e s =>
EXIST(d):[d e i & (c,d) e f2]]
&
ALL(c):ALL(d1):ALL(d2):[(c,d1) e f2 & (c,d2) e f2 => d1=d2]
=>
ALL(c):ALL(d):[c e s & d e i => [d=f2(c) <=> (c,d) e f2]]
Detach, 674, 676
678 (t,u) e f2
Premise
679 ALL(d2):[(t,d2) e f2 => (t,d2) e si]
U Spec, 671
680 (t,u) e f2 => (t,u) e si
U Spec, 679
681 (t,u) e si
Detach, 680, 678
682 ALL(c2):[(t,c2) e si <=> t e s & c2 e i]
U Spec, 29
683 (t,u) e si <=> t e s & u e i
U Spec, 682
684 [(t,u) e si => t e s & u e i]
&
[t e s & u e i => (t,u) e si]
Iff-And, 683
685 (t,u) e si => t e s & u e i
Split, 684
686 t e s & u e i => (t,u) e si
Split, 684
687 t e s & u e i
Detach, 685, 681
688 ALL(c):ALL(d):[(c,d) e f2 => c e s & d e i]
4 Conclusion, 678
689 ALL(c):ALL(d):[(c,d) e f2 => c e s & d e i]
&
ALL(b):[b e s =>
EXIST(c):[c e i & (b,c) e f2]]
Join, 688, 663
690 ALL(c):ALL(d):[(c,d) e f2 => c e s & d e i]
&
ALL(b):[b e s =>
EXIST(c):[c e i & (b,c) e f2]]
&
ALL(b):ALL(c):ALL(d):[(b,c) e f2 & (b,d) e f2 => c=d]
Join, 689, 664
f2 is a function
691 ALL(c):ALL(d):[c e s & d e i => [d=f2(c) <=>
(c,d) e f2]]
Detach, 677, 690
692 t e s
Premise
693 t e s => EXIST(c):[c e i & (t,c) e f2]
U Spec, 663
694 EXIST(c):[c e i & (t,c) e f2]
Detach, 693, 692
695 u e i & (t,u) e f2
E Spec, 694
696 u e i
Split, 695
697 (t,u) e f2
Split, 695
698 ALL(d):[t e s & d e i => [d=f2(t) <=> (t,d) e f2]]
U Spec, 691
699 t e s & u e i => [u=f2(t) <=> (t,u) e f2]
U Spec, 698
700 t e s & u e i
Join, 692, 696
701 u=f2(t) <=> (t,u) e f2
Detach, 699, 700
702 [u=f2(t) => (t,u) e f2] & [(t,u) e f2 => u=f2(t)]
Iff-And, 701
703 u=f2(t) => (t,u) e f2
Split, 702
704 (t,u) e f2 => u=f2(t)
Split, 702
705 u=f2(t)
Detach, 704, 697
706 f2(t) e i
Substitute, 705,
696
f2: s --> i
707 ALL(a):[a e s => f2(a) e i]
4 Conclusion, 692
f1: s --> i and
f2: s --> i
Suppose....
708 g(f1)=g(f2)
Premise
709 ALL(a):ALL(b):[Set'(a) & Set'(b)
=> [a=b
<=>
ALL(c1):ALL(c2):[(c1,c2) e a <=>
(c1,c2) e b]]]
Set Equality
710 ALL(b):[Set'(f1) & Set'(b)
=> [f1=b
<=>
ALL(c1):ALL(c2):[(c1,c2) e f1 <=>
(c1,c2) e b]]]
U Spec, 709
711 Set'(f1) & Set'(f2) => [f1=f2
<=>
ALL(c1):ALL(c2):[(c1,c2) e f1 <=>
(c1,c2) e f2]]
U Spec, 710
712 Set'(f1) & Set'(f2)
Join, 618, 670
713 f1=f2
<=>
ALL(c1):ALL(c2):[(c1,c2) e f1 <=>
(c1,c2) e f2]
Detach, 711, 712
714 [f1=f2 => ALL(c1):ALL(c2):[(c1,c2) e f1 <=> (c1,c2) e f2]]
&
[ALL(c1):ALL(c2):[(c1,c2) e f1 <=> (c1,c2) e f2] => f1=f2]
Iff-And, 713
715 f1=f2 => ALL(c1):ALL(c2):[(c1,c2) e f1 <=> (c1,c2) e f2]
Split, 714
Sufficient: For f1=f2
716 ALL(c1):ALL(c2):[(c1,c2) e f1 <=> (c1,c2) e f2] => f1=f2
Split, 714
717 f1 e fsi => ALL(c):[c e s => [c e g(f1) <=> f1(c)=1]]
U Spec, 321
718 ALL(c):[c e s => [c e g(f1) <=> f1(c)=1]]
Detach, 717, 602
719 f2 e fsi => ALL(c):[c e s => [c e g(f2) <=> f2(c)=1]]
U Spec, 321
720 ALL(c):[c e s => [c e g(f2) <=> f2(c)=1]]
Detach, 719, 603
721 ALL(c):[c e s => [c e g(f1) <=> f2(c)=1]]
Substitute, 708,
720
Suppose...
722 t e s
Premise
723 t e s => [t e g(f1) <=> f1(t)=1]
U Spec, 718
724 t e g(f1) <=> f1(t)=1
Detach, 723, 722
725 [t e g(f1) => f1(t)=1] & [f1(t)=1 => t e g(f1)]
Iff-And, 724
726 t e g(f1) => f1(t)=1
Split, 725
727 f1(t)=1 => t e g(f1)
Split, 725
728 t e s => [t e g(f1) <=> f2(t)=1]
U Spec, 721
729 t e g(f1) <=> f2(t)=1
Detach, 728, 722
730 [t e g(f1) => f2(t)=1] & [f2(t)=1 => t e g(f1)]
Iff-And, 729
731 t e g(f1) => f2(t)=1
Split, 730
732 f2(t)=1 => t e g(f1)
Split, 730
733 f1(t)=1
Premise
734 t e g(f1)
Detach, 727, 733
735 f2(t)=1
Detach, 731, 734
736 f1(t)=1 => f2(t)=1
4 Conclusion, 733
737 f2(t)=1
Premise
738 t e g(f1)
Detach, 732, 737
739 f1(t)=1
Detach, 726, 738
740 f2(t)=1 => f1(t)=1
4 Conclusion, 737
741 ALL(d):[t e s & d e i => [d=f1(t) <=> (t,d) e f1]]
U Spec, 639
742 t e s & 1 e i => [1=f1(t) <=> (t,1) e f1]
U Spec, 741
743 t e s & 1 e i
Join, 722, 21
744 1=f1(t) <=> (t,1) e f1
Detach, 742, 743
745 [1=f1(t) => (t,1) e f1] & [(t,1) e f1 => 1=f1(t)]
Iff-And, 744
746 1=f1(t) => (t,1) e f1
Split, 745
747 f1(t)=1 => (t,1) e f1
Sym, 746
748 (t,1) e f1 => 1=f1(t)
Split, 745
749 (t,1) e f1 => f1(t)=1
Sym, 748
750 ALL(d):[t e s & d e i => [d=f2(t) <=> (t,d) e f2]]
U Spec, 691
751 t e s & 1 e i => [1=f2(t) <=> (t,1) e f2]
U Spec, 750
752 1=f2(t) <=> (t,1) e f2
Detach, 751, 743
753 [1=f2(t) => (t,1) e f2] & [(t,1) e f2 => 1=f2(t)]
Iff-And, 752
754 1=f2(t) => (t,1) e f2
Split, 753
755 f2(t)=1 => (t,1) e f2
Sym, 754
756 (t,1) e f2 => 1=f2(t)
Split, 753
757 (t,1) e f2 => f2(t)=1
Sym, 756
758 (t,1) e f1
Premise
759 f1(t)=1
Detach, 749, 758
760 f2(t)=1
Detach, 736, 759
761 (t,1) e f2
Detach, 755, 760
762 (t,1) e f1 => (t,1) e f2
4 Conclusion, 758
763 (t,1) e f2
Premise
764 f2(t)=1
Detach, 757, 763
765 f1(t)=1
Detach, 740, 764
766 (t,1) e f1
Detach, 747, 765
767 (t,1) e f2 => (t,1) e f1
4 Conclusion, 763
768 [(t,1) e f1 => (t,1) e f2]
&
[(t,1) e f2 => (t,1) e f1]
Join, 762, 767
769 (t,1) e f1 <=> (t,1) e f2
Iff-And, 768
770 ALL(a):[a e s => [(a,1) e f1 <=> (a,1) e f2]]
4 Conclusion, 722
771 f1 e fsi => ALL(c):[c e s => [c e g(f1) <=> f1(c)=1]]
U Spec, 321
772 ALL(c):[c e s => [c e g(f1) <=> f1(c)=1]]
Detach, 771, 602
773 f2 e fsi => ALL(c):[c e s => [c e g(f2) <=> f2(c)=1]]
U Spec, 321
774 ALL(c):[c e s => [c e g(f2) <=> f2(c)=1]]
Detach, 773, 603
775 ALL(c):[c e s => [c e g(f1) <=> f2(c)=1]]
Substitute, 708,
774
776 t e s
Premise
777 t e s => [t e g(f1) <=> f1(t)=1]
U Spec, 772
778 t e g(f1) <=> f1(t)=1
Detach, 777, 776
779 [t e g(f1) => f1(t)=1] & [f1(t)=1 => t e g(f1)]
Iff-And, 778
780 t e g(f1) => f1(t)=1
Split, 779
781 f1(t)=1 => t e g(f1)
Split, 779
782 t e s => [t e g(f1) <=> f2(t)=1]
U Spec, 775
783 t e g(f1) <=> f2(t)=1
Detach, 782, 776
784 [t e g(f1) => f2(t)=1] & [f2(t)=1 => t e g(f1)]
Iff-And, 783
785 t e g(f1) => f2(t)=1
Split, 784
786 f2(t)=1 => t e g(f1)
Split, 784
787 f1(t)=1
Premise
788 t e g(f1)
Detach, 781, 787
789 f2(t)=1
Detach, 785, 788
790 f1(t)=f2(t)
Substitute, 789,
787
791 f1(t)=1 => f1(t)=f2(t)
4 Conclusion, 787
792 f1(t)=1
Premise
793 t e g(f1)
Detach, 781, 792
794 f2(t)=1
Detach, 785, 793
795 f1(t)=1 => f2(t)=1
4 Conclusion, 792
796 f2(t)=1
Premise
797 t e g(f1)
Detach, 786, 796
798 f1(t)=1
Detach, 780, 797
799 f2(t)=1 => f1(t)=1
4 Conclusion, 796
800 [f1(t)=1 => f2(t)=1] & [f2(t)=1 => f1(t)=1]
Join, 795, 799
801 f1(t)=1 <=> f2(t)=1
Iff-And, 800
802 ALL(a):[a e s => [f1(a)=1 <=> f2(a)=1]]
4 Conclusion, 776
Suppose...
803 t e s & u e i
Premise
804 t e s
Split, 803
805 u e i
Split, 803
806 u e i <=> u=0 | u=1
U Spec, 6
807 [u e i => u=0 | u=1] & [u=0 | u=1 => u e i]
Iff-And, 806
808 u e i => u=0 | u=1
Split, 807
809 u=0 | u=1 => u e i
Split, 807
Two cases:
810 u=0 | u=1
Detach, 808, 805
811 (t,u) e f1
Premise
812 ALL(d):[t e s & d e i => [d=f1(t) <=> (t,d) e f1]]
U Spec, 639
813 t e s & u e i => [u=f1(t) <=> (t,u) e f1]
U Spec, 812
814 u=f1(t) <=> (t,u) e f1
Detach, 813, 803
815 [u=f1(t) => (t,u) e f1] & [(t,u) e f1 => u=f1(t)]
Iff-And, 814
816 u=f1(t) => (t,u) e f1
Split, 815
817 (t,u) e f1 => u=f1(t)
Split, 815
818 u=f1(t)
Detach, 817, 811
Case 1
819 u=1
Premise
820 1=f1(t)
Substitute, 819,
818
821 f1(t)=1
Sym, 820
822 t e s => [f1(t)=1 <=> f2(t)=1]
U Spec, 802
823 f1(t)=1 <=> f2(t)=1
Detach, 822, 804
824 [f1(t)=1 => f2(t)=1] & [f2(t)=1 => f1(t)=1]
Iff-And, 823
825 f1(t)=1 => f2(t)=1
Split, 824
826 f2(t)=1 => f1(t)=1
Split, 824
827 f2(t)=1
Detach, 825, 821
828 ALL(d):[t e s & d e i => [d=f2(t) <=> (t,d) e f2]]
U Spec, 691
829 t e s & 1 e i => [1=f2(t) <=> (t,1) e f2]
U Spec, 828
830 t e s & 1 e i
Join, 804, 21
831 1=f2(t) <=> (t,1) e f2
Detach, 829, 830
832 [1=f2(t) => (t,1) e f2] & [(t,1) e f2 => 1=f2(t)]
Iff-And, 831
833 1=f2(t) => (t,1) e f2
Split, 832
834 (t,1) e f2 => 1=f2(t)
Split, 832
835 f2(t)=1 => (t,1) e f2
Sym, 833
836 (t,1) e f2
Detach, 835, 827
837 (t,u) e f2
Substitute, 819,
836
838 u=1 => (t,u) e f2
4 Conclusion, 819
Case 2
839 u=0
Premise
840 0=f1(t)
Substitute, 839,
818
841 f1(t)=1
Premise
842 0=1
Substitute, 841,
840
843 0=1 & ~0=1
Join, 842, 7
844 ~f1(t)=1
4 Conclusion, 841
845 t e s => [f1(t)=1 <=> f2(t)=1]
U Spec, 802
846 f1(t)=1 <=> f2(t)=1
Detach, 845, 804
847 [f1(t)=1 => f2(t)=1] & [f2(t)=1 => f1(t)=1]
Iff-And, 846
848 f1(t)=1 => f2(t)=1
Split, 847
849 f2(t)=1 => f1(t)=1
Split, 847
850 ~f1(t)=1 => ~f2(t)=1
Contra, 849
851 ~f2(t)=1
Detach, 850, 844
852 t e s => f2(t) e i
U Spec, 707
853 f2(t) e i
Detach, 852, 804
854 f2(t) e i <=> f2(t)=0 | f2(t)=1
U Spec, 6
855 [f2(t) e i => f2(t)=0 | f2(t)=1]
&
[f2(t)=0 | f2(t)=1 => f2(t) e i]
Iff-And, 854
856 f2(t) e i => f2(t)=0 | f2(t)=1
Split, 855
857 f2(t)=0 | f2(t)=1 => f2(t) e i
Split, 855
858 f2(t)=0 | f2(t)=1
Detach, 856, 853
859 ~f2(t)=0 => f2(t)=1
Imply-Or, 858
860 ~f2(t)=1 => ~~f2(t)=0
Contra, 859
861 ~f2(t)=1 => f2(t)=0
Rem DNeg, 860
862 f2(t)=0
Detach, 861, 851
863 f2(t)=u
Substitute, 839,
862
864 ALL(d):[t e s & d e i => [d=f2(t) <=> (t,d) e f2]]
U Spec, 691
865 t e s & u e i => [u=f2(t) <=> (t,u) e f2]
U Spec, 864
866 u=f2(t) <=> (t,u) e f2
Detach, 865, 803
867 [u=f2(t) => (t,u) e f2] & [(t,u) e f2 => u=f2(t)]
Iff-And, 866
868 u=f2(t) => (t,u) e f2
Split, 867
869 (t,u) e f2 => u=f2(t)
Split, 867
870 f2(t)=u => (t,u) e f2
Sym, 868
871 (t,u) e f2
Detach, 870, 863
872 u=0 => (t,u) e f2
4 Conclusion, 839
873 [u=0 => (t,u) e f2] & [u=1 => (t,u) e f2]
Join, 872, 838
874 (t,u) e f2
Cases, 810, 873
875 (t,u) e f1 => (t,u) e f2
4 Conclusion, 811
876 (t,u) e f2
Premise
877 ALL(d):[t e s & d e i => [d=f2(t) <=> (t,d) e f2]]
U Spec, 691
878 t e s & u e i => [u=f2(t) <=> (t,u) e f2]
U Spec, 877
879 u=f2(t) <=> (t,u) e f2
Detach, 878, 803
880 [u=f2(t) => (t,u) e f2] & [(t,u) e f2 => u=f2(t)]
Iff-And, 879
881 u=f2(t) => (t,u) e f2
Split, 880
882 (t,u) e f2 => u=f2(t)
Split, 880
883 u=f2(t)
Detach, 882, 876
Case 1
884 u=1
Premise
885 1=f2(t)
Substitute, 884,
883
886 f2(t)=1
Sym, 885
887 t e s => [f1(t)=1 <=> f2(t)=1]
U Spec, 802
888 f1(t)=1 <=> f2(t)=1
Detach, 887, 804
889 [f1(t)=1 => f2(t)=1] & [f2(t)=1 => f1(t)=1]
Iff-And, 888
890 f1(t)=1 => f2(t)=1
Split, 889
891 f2(t)=1 => f1(t)=1
Split, 889
892 f1(t)=1
Detach, 891, 886
893 f1(t)=u
Substitute, 884,
892
894 ALL(d):[t e s & d e i => [d=f1(t) <=> (t,d) e f1]]
U Spec, 639
895 t e s & u e i => [u=f1(t) <=> (t,u) e f1]
U Spec, 894
896 u=f1(t) <=> (t,u) e f1
Detach, 895, 803
897 [u=f1(t) => (t,u) e f1] & [(t,u) e f1 => u=f1(t)]
Iff-And, 896
898 u=f1(t) => (t,u) e f1
Split, 897
899 (t,u) e f1 => u=f1(t)
Split, 897
900 f1(t)=u => (t,u) e f1
Sym, 898
901 (t,u) e f1
Detach, 900, 893
902 u=1 => (t,u) e f1
4 Conclusion, 884
Case 2
903 u=0
Premise
904 0=f2(t)
Substitute, 903,
883
905 f2(t)=1
Premise
906 0=1
Substitute, 905,
904
907 0=1 & ~0=1
Join, 906, 7
908 ~f2(t)=1
4 Conclusion, 905
909 t e s => [f1(t)=1 <=> f2(t)=1]
U Spec, 802
910 f1(t)=1 <=> f2(t)=1
Detach, 909, 804
911 [f1(t)=1 => f2(t)=1] & [f2(t)=1 => f1(t)=1]
Iff-And, 910
912 f1(t)=1 => f2(t)=1
Split, 911
913 f2(t)=1 => f1(t)=1
Split, 911
914 ~f2(t)=1 => ~f1(t)=1
Contra, 912
915 ~f1(t)=1
Detach, 914, 908
916 t e s => f1(t) e i
U Spec, 655
917 f1(t) e i
Detach, 916, 804
918 f1(t) e i <=> f1(t)=0 | f1(t)=1
U Spec, 6
919 [f1(t) e i => f1(t)=0 | f1(t)=1]
&
[f1(t)=0 | f1(t)=1 => f1(t) e i]
Iff-And, 918
920 f1(t) e i => f1(t)=0 | f1(t)=1
Split, 919
921 f1(t)=0 | f1(t)=1 => f1(t) e i
Split, 919
922 f1(t)=0 | f1(t)=1
Detach, 920, 917
923 ~f1(t)=0 => f1(t)=1
Imply-Or, 922
924 ~f1(t)=1 => ~~f1(t)=0
Contra, 923
925 ~f1(t)=1 => f1(t)=0
Rem DNeg, 924
926 f1(t)=0
Detach, 925, 915
927 f1(t)=u
Substitute, 903,
926
928 ALL(d):[t e s & d e i => [d=f1(t) <=> (t,d) e f1]]
U Spec, 639
929 t e s & u e i => [u=f1(t) <=> (t,u) e f1]
U Spec, 928
930 u=f1(t) <=> (t,u) e f1
Detach, 929, 803
931 [u=f1(t) => (t,u) e f1] & [(t,u) e f1 => u=f1(t)]
Iff-And, 930
932 u=f1(t) => (t,u) e f1
Split, 931
933 (t,u) e f1 => u=f1(t)
Split, 931
934 f1(t)=u => (t,u) e f1
Sym, 932
935 (t,u) e f1
Detach, 934, 927
936 u=0 => (t,u) e f1
4 Conclusion, 903
937 [u=0 => (t,u) e f1] & [u=1 => (t,u) e f1]
Join, 936, 902
938 (t,u) e f1
Cases, 810, 937
939 (t,u) e f2 => (t,u) e f1
4 Conclusion, 876
940 [(t,u) e f1 => (t,u) e f2]
&
[(t,u) e f2 => (t,u) e f1]
Join, 875, 939
941 (t,u) e f1 <=> (t,u) e f2
Iff-And, 940
942 ALL(a):ALL(b):[a e s & b e i => [(a,b) e f1 <=> (a,b) e f2]]
4 Conclusion, 803
943 (t,u) e f1
Premise
944 ALL(d2):[(t,d2) e f1 => (t,d2) e si]
U Spec, 619
945 (t,u) e f1 => (t,u) e si
U Spec, 944
946 (t,u) e si
Detach, 945, 943
947 ALL(c2):[(t,c2) e si <=> t e s & c2 e i]
U Spec, 29
948 (t,u) e si <=> t e s & u e i
U Spec, 947
949 [(t,u) e si => t e s & u e i]
&
[t e s & u e i => (t,u) e si]
Iff-And, 948
950 (t,u) e si => t e s & u e i
Split, 949
951 t e s & u e i => (t,u) e si
Split, 949
952 t e s & u e i
Detach, 950, 946
953 ALL(b):[t e s & b e i => [(t,b) e f1 <=> (t,b) e f2]]
U Spec, 942
954 t e s & u e i => [(t,u) e f1 <=> (t,u) e f2]
U Spec, 953
955 (t,u) e f1 <=> (t,u) e f2
Detach, 954, 952
956 [(t,u) e f1 => (t,u) e f2] & [(t,u) e f2 => (t,u) e f1]
Iff-And, 955
957 (t,u) e f1 => (t,u) e f2
Split, 956
958 (t,u) e f2 => (t,u) e f1
Split, 956
959 (t,u) e f2
Detach, 957, 943
960 ALL(a):ALL(b):[(a,b) e f1 => (a,b) e f2]
4 Conclusion, 943
961 (t,u) e f2
Premise
962 ALL(d2):[(t,d2) e f2 => (t,d2) e si]
U Spec, 671
963 (t,u) e f2 => (t,u) e si
U Spec, 962
964 (t,u) e si
Detach, 963, 961
965 ALL(c2):[(t,c2) e si <=> t e s & c2 e i]
U Spec, 29
966 (t,u) e si <=> t e s & u e i
U Spec, 965
967 [(t,u) e si => t e s & u e i]
&
[t e s & u e i => (t,u) e si]
Iff-And, 966
968 (t,u) e si => t e s & u e i
Split, 967
969 t e s & u e i => (t,u) e si
Split, 967
970 t e s & u e i
Detach, 968, 964
971 ALL(b):[t e s & b e i => [(t,b) e f1 <=> (t,b) e f2]]
U Spec, 942
972 t e s & u e i => [(t,u) e f1 <=> (t,u) e f2]
U Spec, 971
973 (t,u) e f1 <=> (t,u) e f2
Detach, 972, 970
974 [(t,u) e f1 => (t,u) e f2] & [(t,u) e f2 => (t,u) e f1]
Iff-And, 973
975 (t,u) e f1 => (t,u) e f2
Split, 974
976 (t,u) e f2 => (t,u) e f1
Split, 974
977 (t,u) e f1
Detach, 976, 961
978 ALL(a):ALL(b):[(a,b) e f2 => (a,b) e f1]
4 Conclusion, 961
979 ALL(a):ALL(b):[[(a,b) e f1 => (a,b) e f2] & [(a,b) e f2 => (a,b) e f1]]
Join, 960, 978
980 ALL(a):ALL(b):[(a,b) e f1 <=> (a,b) e f2]
Iff-And, 979
981 f1=f2
Detach, 716, 980
982 g(f1)=g(f2) => f1=f2
4 Conclusion, 708
******************
g is injective
******************
983 ALL(f1):ALL(f2):[f1 e fsi & f2 e fsi => [g(f1)=g(f2) =>
f1=f2]]
4 Conclusion, 601