THEOREM
*******
Given sets x and y we can
construct the set fs consisting of all those function-like subsets of the
Cartesian product of x and y.
For each element f e fs, we can prove the existence of a
unique function g: x --> y such that g(a)=b
<=> (a, b) in f.
ALL(x):ALL(y):[Set(x)
& Set(y)
=> EXIST(fs):[ALL(f):[f
e fs
<=> Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e x & b e y]
& [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[a
e x & b1 e y & b2 e y => [(a,b1) e f &
(a,b2) e f => b1=b2]]]]
& ALL(f):[f e fs => EXIST(g):[ALL(a):[a e x => g(a) e y]
& ALL(a1):ALL(b):[a1
e x & b e y =>
[g(a1)=b <=> (a1,b) e f]]
& ALL(g'):[ALL(a):[a
e x => g'(a) e y]
& ALL(a1):ALL(b):[a1
e x & b e y =>
[g'(a1)=b <=> (a1,b) e f]]
=> ALL(a):[a e x => g'(a)=g(a)]]]]]]
By Dan Christensen
2022-01-06
This machine-verified, formal
proof was written with the aid of the author's DC Proof 2.0 freeware available http://www.dcproof.com
PROOF
*****
Let x and y be sets
1 Set(x) & Set(y)
Premise
2 Set(x)
Split, 1
3 Set(y)
Split, 1
Apply Cartesian Product Axiom
4 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
5 ALL(a2):[Set(x) & Set(a2) => EXIST(b):[Set'(b) &
ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e a2]]]
U Spec, 4
6 Set(x) & Set(y) => EXIST(b):[Set'(b) &
ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e y]]
U Spec, 5
7 EXIST(b):[Set'(b) &
ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e y]]
Detach, 6, 1
8 Set'(xy) & ALL(c1):ALL(c2):[(c1,c2) e xy <=> c1 e x & c2 e y]
E Spec, 7
Define: xy
9 Set'(xy)
Split, 8
10 ALL(c1):ALL(c2):[(c1,c2) e xy <=> c1 e x & c2 e y]
Split, 8
Apply Powerset Axiom
11 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
12 Set'(xy) => EXIST(b):[Set(b)
&
ALL(c):[c e b <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e xy]]]
U Spec, 11
13 EXIST(b):[Set(b)
&
ALL(c):[c e b <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e xy]]]
Detach, 12, 9
14 Set(pxy)
&
ALL(c):[c e pxy <=>
Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e xy]]
E Spec, 13
Define: pxy
15 Set(pxy)
Split, 14
16 ALL(c):[c e pxy <=>
Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e xy]]
Split, 14
Apply Subset Axiom
17 EXIST(fs):[Set(fs) & ALL(f):[f e fs <=> f e pxy &
[ALL(a):[a e x => EXIST(b):[b e y & (a,b) e f]]
&
ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=>
[(a,b1) e f & (a,b2) e f => b1=b2]]]]]
Subset, 15
18 Set(fs) & ALL(f):[f e fs <=> f e pxy &
[ALL(a):[a e x => EXIST(b):[b e y & (a,b) e f]]
&
ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=>
[(a,b1) e f & (a,b2) e f => b1=b2]]]]
E Spec, 17
Define: fs
19 Set(fs)
Split, 18
20 ALL(f):[f e fs <=> f e pxy &
[ALL(a):[a e x => EXIST(b):[b e y & (a,b) e f]]
&
ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=>
[(a,b1) e f & (a,b2) e f => b1=b2]]]]
Split, 18
Prove: ALL(f):[f e fs
=> Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e x & b e y]
& [ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=> [(a,b1) e f & (a,b2) e f =>
b1=b2]]]]
Suppose...
21 t e fs
Premise
Apply definition of fs to get rid of pxy
reference
22 t e fs <=> t e pxy & [ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e t]]
&
ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=>
[(a,b1) e t & (a,b2) e t => b1=b2]]]
U Spec, 20
23 [t e fs => t e pxy & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e t]]
&
ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=>
[(a,b1) e t & (a,b2) e t => b1=b2]]]]
&
[t e pxy & [ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e t]]
&
ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=>
[(a,b1) e t & (a,b2) e t => b1=b2]]] => t e fs]
Iff-And, 22
24 t e fs => t e pxy & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e t]]
&
ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=>
[(a,b1) e t & (a,b2) e t => b1=b2]]]
Split, 23
25 t e pxy & [ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e t]]
&
ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=>
[(a,b1) e t & (a,b2) e t => b1=b2]]]
Detach, 24, 21
26 t e pxy
Split, 25
27 ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e t]]
&
ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=>
[(a,b1) e t & (a,b2) e t => b1=b2]]
Split, 25
Apply definition of pxy
28 t e pxy <=> Set'(t) & ALL(d1):ALL(d2):[(d1,d2) e t => (d1,d2) e xy]
U Spec, 16
29 [t e pxy => Set'(t) & ALL(d1):ALL(d2):[(d1,d2) e t => (d1,d2) e xy]]
&
[Set'(t) & ALL(d1):ALL(d2):[(d1,d2) e t => (d1,d2) e xy] => t e pxy]
Iff-And, 28
30 t e pxy => Set'(t) & ALL(d1):ALL(d2):[(d1,d2) e t => (d1,d2) e xy]
Split, 29
31 Set'(t) & ALL(d1):ALL(d2):[(d1,d2) e t => (d1,d2) e xy]
Detach, 30, 26
32 Set'(t)
Split, 31
33 ALL(d1):ALL(d2):[(d1,d2) e t => (d1,d2) e xy]
Split, 31
Prove: ALL(a):ALL(b):[(a,b) e t => a e x & b e y]
Suppose...
34 (u,v) e t
Premise
Apply definition of xy
35 ALL(d2):[(u,d2) e t => (u,d2) e xy]
U Spec, 33
36 (u,v) e t => (u,v) e xy
U Spec, 35
37 (u,v) e xy
Detach, 36, 34
38 ALL(c2):[(u,c2) e xy <=> u e x & c2 e y]
U Spec, 10
39 (u,v) e xy <=> u e x & v e y
U Spec, 38
40 [(u,v) e xy => u e x & v e y]
&
[u e x & v e y => (u,v) e xy]
Iff-And, 39
41 (u,v) e xy => u e x & v e y
Split, 40
42 u e x & v e y
Detach, 41, 37
As Required:
43 ALL(a):ALL(b):[(a,b) e t => a e x & b e y]
4 Conclusion, 34
44 Set'(t)
&
ALL(a):ALL(b):[(a,b) e t => a e x & b e y]
Join, 32, 43
45 Set'(t)
&
ALL(a):ALL(b):[(a,b) e t => a e x & b e y]
&
[ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e t]]
&
ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=>
[(a,b1) e t & (a,b2) e t => b1=b2]]]
Join, 44, 27
As Required:
46 ALL(f):[f e fs
=>
Set'(f)
&
ALL(a):ALL(b):[(a,b) e f => a e x & b e y]
&
[ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e f]]
&
ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=>
[(a,b1) e f & (a,b2) e f => b1=b2]]]]
4 Conclusion, 21
Prove: ALL(f):[Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e x & b e y]
& [ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=> [(a,b1) e f & (a,b2) e f => b1=b2]]]
=> f e fs]
Suppose...
47 Set'(t)
&
ALL(a):ALL(b):[(a,b) e t => a e x & b e y]
&
[ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e t]]
&
ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=>
[(a,b1) e t & (a,b2) e t => b1=b2]]]
Premise
48 Set'(t)
Split, 47
49 ALL(a):ALL(b):[(a,b) e t => a e x & b e y]
Split, 47
50 ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e t]]
&
ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=>
[(a,b1) e t & (a,b2) e t => b1=b2]]
Split, 47
Apply definition of fs
51 t e fs <=> t e pxy & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e t]]
&
ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=>
[(a,b1) e t & (a,b2) e t => b1=b2]]]
U Spec, 20
52 [t e fs => t e pxy & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e t]]
&
ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=>
[(a,b1) e t & (a,b2) e t => b1=b2]]]]
&
[t e pxy & [ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e t]]
&
ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=>
[(a,b1) e t & (a,b2) e t => b1=b2]]] => t e fs]
Iff-And, 51
53 t e pxy & [ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e t]]
&
ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=>
[(a,b1) e t & (a,b2) e t => b1=b2]]] => t e fs
Split, 52
Apply definition of pxy
54 t e pxy <=> Set'(t) & ALL(d1):ALL(d2):[(d1,d2) e t => (d1,d2) e xy]
U Spec, 16
55 [t e pxy => Set'(t) & ALL(d1):ALL(d2):[(d1,d2) e t => (d1,d2) e xy]]
&
[Set'(t) & ALL(d1):ALL(d2):[(d1,d2) e t => (d1,d2) e xy] => t e pxy]
Iff-And, 54
Sufficient: For t e pxy
56 Set'(t) & ALL(d1):ALL(d2):[(d1,d2) e t => (d1,d2) e xy] => t e pxy
Split, 55
Prove: ALL(a):ALL(b):[(a,b) e t => (a,b)
e xy]
Suppose...
57 (u,v) e t
Premise
Apply definition of xy
58 ALL(c2):[(u,c2) e xy <=> u e x & c2 e y]
U Spec, 10
59 (u,v) e xy <=> u e x & v e y
U Spec, 58
60 [(u,v) e xy => u e x & v e y]
&
[u e x & v e y => (u,v) e xy]
Iff-And, 59
61 u e x & v e y => (u,v) e xy
Split, 60
62 ALL(b):[(u,b) e t => u e x & b e y]
U Spec, 49
63 (u,v) e t => u e x & v e y
U Spec, 62
64 u e x & v e y
Detach, 63, 57
65 (u,v) e xy
Detach, 61, 64
As Required:
66 ALL(a):ALL(b):[(a,b) e t => (a,b) e xy]
4 Conclusion, 57
67 Set'(t) & ALL(a):ALL(b):[(a,b) e t => (a,b) e xy]
Join, 48, 66
68 t e pxy
Detach, 56, 67
69 t e pxy
&
[ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e t]]
&
ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=>
[(a,b1) e t & (a,b2) e t => b1=b2]]]
Join, 68, 50
70 t e fs
Detach, 53, 69
As Required:
71 ALL(f):[Set'(f)
&
ALL(a):ALL(b):[(a,b) e f => a e x & b e y]
&
[ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e f]]
&
ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=>
[(a,b1) e f & (a,b2) e f => b1=b2]]]
=>
f e fs]
4 Conclusion, 47
72 ALL(f):[[f e fs
=>
Set'(f)
&
ALL(a):ALL(b):[(a,b) e f => a e x & b e y]
&
[ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e f]]
&
ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=>
[(a,b1) e f & (a,b2) e f => b1=b2]]]] & [Set'(f)
&
ALL(a):ALL(b):[(a,b) e f => a e x & b e y]
&
[ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e f]]
&
ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=>
[(a,b1) e f & (a,b2) e f => b1=b2]]]
=>
f e fs]]
Join, 46, 71
Alternatively Define: fs (without pxy)
73 ALL(f):[f e fs
<=>
Set'(f)
&
ALL(a):ALL(b):[(a,b) e f => a e x & b e y]
&
[ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e f]]
&
ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=>
[(a,b1) e f & (a,b2) e f => b1=b2]]]]
Iff-And, 72
Prove: ALL(f):[f e fs
=> EXIST(g):[ALL(a):[a e x => g(a) e y]
& ALL(a1):ALL(b):[a1 e x & b e y
=> [g(a1)=b <=> (a1,b) e f]]
& ALL(g'):[ALL(a):[a e x => g'(a)
e y]
& ALL(a1):ALL(b):[a1 e x & b e y => [g'(a1)=b <=> (a1,b) e f]]
=> ALL(a):[a e x =>
g'(a)=g(a)]]]]
Suppose...
74 f e fs
Premise
Apply definition of fs
75 f e fs
<=>
Set'(f)
&
ALL(a):ALL(b):[(a,b) e f => a e x & b e y]
&
[ALL(a):[a e x => EXIST(b):[b e y & (a,b) e f]]
&
ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=>
[(a,b1) e f & (a,b2) e f => b1=b2]]]
U Spec, 73
76 [f e fs => Set'(f)
&
ALL(a):ALL(b):[(a,b) e f => a e x & b e y]
&
[ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e f]]
&
ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=>
[(a,b1) e f & (a,b2) e f => b1=b2]]]]
&
[Set'(f)
&
ALL(a):ALL(b):[(a,b) e f => a e x & b e y]
&
[ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e f]]
&
ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=>
[(a,b1) e f & (a,b2) e f => b1=b2]]] => f e fs]
Iff-And, 75
77 f e fs => Set'(f)
&
ALL(a):ALL(b):[(a,b) e f => a e x & b e y]
&
[ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e f]]
&
ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=>
[(a,b1) e f & (a,b2) e f => b1=b2]]]
Split, 76
78 Set'(f)
&
ALL(a):ALL(b):[(a,b) e f => a e x & b e y]
&
[ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e f]]
&
ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=>
[(a,b1) e f & (a,b2) e f => b1=b2]]]
Detach, 77, 74
79 Set'(f)
Split, 78
80 ALL(a):ALL(b):[(a,b) e f => a e x & b e y]
Split, 78
81 ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e f]]
&
ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=>
[(a,b1) e f & (a,b2) e f => b1=b2]]
Split, 78
82 ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e f]]
Split, 81
83 ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=>
[(a,b1) e f & (a,b2) e f => b1=b2]]
Split, 81
Apply Function Axiom
84 ALL(f):ALL(dom):ALL(cod):[Set'(f) &
Set(dom) & Set(cod)
=>
[ALL(a1):[a1 e dom => EXIST(b):[b e cod & (a1,b) e f]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e dom & b1 e cod & b2 e cod
=>
[(a1,b1) e f & (a1,b2) e f => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e dom & b e cod
=>
[fun(a1)=b <=> (a1,b) e f]]]]
Function
85 ALL(dom):ALL(cod):[Set'(f) & Set(dom) & Set(cod)
=>
[ALL(a1):[a1 e dom => EXIST(b):[b e cod & (a1,b) e f]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e dom & b1 e cod & b2 e cod
=>
[(a1,b1) e f & (a1,b2) e f => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e dom & b e cod
=>
[fun(a1)=b <=> (a1,b) e f]]]]
U Spec, 84
86 ALL(cod):[Set'(f) & Set(x) & Set(cod)
=>
[ALL(a1):[a1 e x =>
EXIST(b):[b e cod & (a1,b) e f]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e cod & b2 e cod
=>
[(a1,b1) e f & (a1,b2) e f => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e cod
=>
[fun(a1)=b <=> (a1,b) e f]]]]
U Spec, 85
87 Set'(f) & Set(x) & Set(y)
=>
[ALL(a1):[a1 e x => EXIST(b):[b e y & (a1,b) e f]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e y & b2 e y
=>
[(a1,b1) e f & (a1,b2) e f => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e y
=>
[fun(a1)=b <=> (a1,b) e f]]]
U Spec, 86
88 Set'(f) & Set(x)
Join, 79, 2
89 Set'(f) & Set(x) & Set(y)
Join, 88, 3
90 ALL(a1):[a1 e x =>
EXIST(b):[b e y & (a1,b) e f]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e y & b2 e y
=>
[(a1,b1) e f & (a1,b2) e f => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e y
=>
[fun(a1)=b <=> (a1,b) e f]]
Detach, 87, 89
91 EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e y
=>
[fun(a1)=b <=> (a1,b) e f]]
Detach, 90, 81
Define: g
92 ALL(a1):ALL(b):[a1 e x & b e y
=>
[g(a1)=b <=> (a1,b) e f]]
E Spec, 91
Prove: ALL(a):[a e x => g(a) e y]
Suppose...
93 t e x
Premise
94 t e x => EXIST(b):[b e y & (t,b) e f]
U Spec, 82
95 EXIST(b):[b e y & (t,b) e f]
Detach, 94, 93
96 u e y & (t,u) e f
E Spec, 95
97 u e y
Split, 96
98 (t,u) e f
Split, 96
Apply definition of g
99 ALL(b):[t e x & b e y
=>
[g(t)=b <=> (t,b) e f]]
U Spec, 92
100 t e x & u e y
=>
[g(t)=u <=> (t,u) e f]
U Spec, 99
101 t e x & u e y
Join, 93, 97
102 g(t)=u <=> (t,u) e f
Detach, 100, 101
103 [g(t)=u => (t,u) e f] & [(t,u) e f => g(t)=u]
Iff-And, 102
104 (t,u) e f => g(t)=u
Split, 103
105 g(t)=u
Detach, 104, 98
106 g(t) e y
Substitute, 105,
97
As Required:
107 ALL(a):[a e x => g(a) e y]
4 Conclusion, 93
Prove: g is unique
Suppose we have function g' such that...
108 ALL(a):[a e x => g'(a) e y]
&
ALL(a1):ALL(b):[a1 e x & b e y => [g'(a1)=b <=> (a1,b) e f]]
Premise
109 ALL(a):[a e x => g'(a) e y]
Split, 108
110 ALL(a1):ALL(b):[a1 e x & b e y => [g'(a1)=b <=>
(a1,b) e f]]
Split, 108
Prove: ALL(a):[a e x => g'(a)=g(a)]
Suppose...
111 t e x
Premise
112 t e x => EXIST(b):[b e y & (t,b) e f]
U Spec, 82
113 EXIST(b):[b e y & (t,b) e f]
Detach, 112, 111
114 u e y & (t,u) e f
E Spec, 113
115 u e y
Split, 114
116 (t,u) e f
Split, 114
117 ALL(b):[t e x & b e y
=>
[g(t)=b <=> (t,b) e f]]
U Spec, 92
118 t e x & u e y
=>
[g(t)=u <=> (t,u) e f]
U Spec, 117
119 t e x & u e y
Join, 111, 115
120 g(t)=u <=> (t,u) e f
Detach, 118, 119
121 [g(t)=u => (t,u) e f] & [(t,u) e f => g(t)=u]
Iff-And, 120
122 (t,u) e f => g(t)=u
Split, 121
123 g(t)=u
Detach, 122, 116
124 ALL(b):[t e x & b e y => [g'(t)=b <=> (t,b) e f]]
U Spec, 110
125 t e x & u e y => [g'(t)=u <=> (t,u) e f]
U Spec, 124
126 t e x & u e y
Join, 111, 115
127 g'(t)=u <=> (t,u) e f
Detach, 125, 126
128 [g'(t)=u => (t,u) e f] & [(t,u) e f => g'(t)=u]
Iff-And, 127
129 (t,u) e f => g'(t)=u
Split, 128
130 g'(t)=u
Detach, 129, 116
131 g'(t)=g(t)
Substitute, 123,
130
As Required:
132 ALL(a):[a e x => g'(a)=g(a)]
4 Conclusion, 111
As Required:
133 ALL(g'):[ALL(a):[a e x => g'(a) e y]
&
ALL(a1):ALL(b):[a1 e x & b e y => [g'(a1)=b <=> (a1,b) e f]]
=>
ALL(a):[a e x => g'(a)=g(a)]]
4 Conclusion, 108
134 ALL(a):[a e x => g(a) e y]
&
ALL(a1):ALL(b):[a1 e x & b e y
=>
[g(a1)=b <=> (a1,b) e f]]
Join, 107, 92
135 ALL(a):[a e x => g(a) e y]
&
ALL(a1):ALL(b):[a1 e x & b e y
=>
[g(a1)=b <=> (a1,b) e f]]
&
ALL(g'):[ALL(a):[a e x => g'(a) e y]
&
ALL(a1):ALL(b):[a1 e x & b e y => [g'(a1)=b <=> (a1,b) e f]]
=>
ALL(a):[a e x => g'(a)=g(a)]]
Join, 134, 133
As Required:
136 ALL(f):[f e fs
=>
EXIST(g):[ALL(a):[a e x => g(a) e y]
&
ALL(a1):ALL(b):[a1 e x & b e y
=>
[g(a1)=b <=> (a1,b) e f]]
&
ALL(g'):[ALL(a):[a e x => g'(a) e y]
&
ALL(a1):ALL(b):[a1 e x & b e y => [g'(a1)=b <=> (a1,b) e f]]
=>
ALL(a):[a e x =>
g'(a)=g(a)]]]]
4 Conclusion, 74
Joining results...
137 ALL(f):[f e fs
<=>
Set'(f)
&
ALL(a):ALL(b):[(a,b) e f => a e x & b e y]
&
[ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e f]]
&
ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=>
[(a,b1) e f & (a,b2) e f => b1=b2]]]]
&
ALL(f):[f e fs
=>
EXIST(g):[ALL(a):[a e x => g(a) e y]
&
ALL(a1):ALL(b):[a1 e x & b e y
=>
[g(a1)=b <=> (a1,b) e f]]
&
ALL(g'):[ALL(a):[a e x => g'(a) e y]
&
ALL(a1):ALL(b):[a1 e x & b e y => [g'(a1)=b <=> (a1,b) e f]]
=>
ALL(a):[a e x =>
g'(a)=g(a)]]]]
Join, 73, 136
As Required:
138 ALL(x):ALL(y):[Set(x) & Set(y)
=>
EXIST(fs):[ALL(f):[f e fs
<=>
Set'(f)
&
ALL(a):ALL(b):[(a,b) e f => a e x & b e y]
&
[ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e f]]
&
ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y
=>
[(a,b1) e f & (a,b2) e f => b1=b2]]]]
&
ALL(f):[f e fs
=>
EXIST(g):[ALL(a):[a e x => g(a) e y]
&
ALL(a1):ALL(b):[a1 e x & b e y
=>
[g(a1)=b <=> (a1,b) e f]]
&
ALL(g'):[ALL(a):[a e x => g'(a) e y]
&
ALL(a1):ALL(b):[a1 e x & b e y => [g'(a1)=b <=> (a1,b) e f]]
=>
ALL(a):[a e x =>
g'(a)=g(a)]]]]]]
4 Conclusion, 1