THEOREM
*******
Given any sets X and Y, there
exists a function f: X --> Y if and only if there exists a graph set mapping
X to Y.
ALL(x):ALL(y):[Set(x)
& Set(y)
=> [EXIST(f):ALL(a):[a
e x => f(a) e y]
<=> EXIST(g):[Set'(g)
& ALL(a):ALL(b):[(a,b) e g => a e x & b e y]
& ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]
& ALL(a):ALL(b):ALL(c):[a
e x & b e y & c e y => [(a,b) e g & (a,c) e g => b=c]]]]]
By Dan Christensen
2022-04-05
Homepage: http://www.dcproof.com
PROOF
*****
1 Set(x) & Set(y)
Premise
2 Set(x)
Split, 1
3 Set(y)
Split, 1
Prove: EXIST(f):ALL(a):[a e x => f(a) e y]
=> EXIST(g):[Set'(g)
& ALL(a):ALL(b):[(a,b) e g => a e x & b e y]
& ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e g]]
& ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y => [(a,b) e g & (a,c)
e g => b=c]]]
Suppose...
4 EXIST(f):ALL(a):[a e x => f(a) e y]
Premise
5 ALL(a):[a e x => f(a) e y]
E Spec, 4
6 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
7 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, 6
8 Set(x) & Set(y) => EXIST(b):[Set'(b) &
ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e y]]
U Spec, 7
9 EXIST(b):[Set'(b)
& ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e y]]
Detach, 8, 1
10 Set'(xy) & ALL(c1):ALL(c2):[(c1,c2) e xy <=> c1 e x & c2 e y]
E Spec, 9
Define: xy
11 Set'(xy)
Split, 10
12 ALL(c1):ALL(c2):[(c1,c2) e xy <=> c1 e x & c2 e y]
Split, 10
13 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e xy & f(a)=b]]
Subset, 11
14 Set'(g) & ALL(a):ALL(b):[(a,b) e g <=> (a,b) e xy & f(a)=b]
E Spec, 13
Define: g
15 Set'(g)
Split, 14
16 ALL(a):ALL(b):[(a,b) e g <=> (a,b) e xy & f(a)=b]
Split, 14
Prove: ALL(a):ALL(b):[(a,b) e g => a e x & b e y]
Suppose...
17 (t,u) e g
Premise
18 ALL(b):[(t,b) e g <=> (t,b) e xy & f(t)=b]
U Spec, 16
19 (t,u) e g <=> (t,u) e xy & f(t)=u
U Spec, 18
20 [(t,u) e g => (t,u) e xy & f(t)=u]
&
[(t,u) e xy & f(t)=u => (t,u) e g]
Iff-And, 19
21 (t,u) e g => (t,u) e xy & f(t)=u
Split, 20
22 (t,u) e xy & f(t)=u
Detach, 21, 17
23 (t,u) e xy
Split, 22
24 ALL(c2):[(t,c2) e xy <=> t e x & c2 e y]
U Spec, 12
25 (t,u) e xy <=> t e x & u e y
U Spec, 24
26 [(t,u) e xy => t e x & u e y]
&
[t e x & u e y => (t,u) e xy]
Iff-And, 25
27 (t,u) e xy => t e x & u e y
Split, 26
28 t e x & u e y
Detach, 27, 23
Part 1
As Required:
29 ALL(a):ALL(b):[(a,b) e g => a e x & b e y]
4 Conclusion, 17
Prove: ALL(a):[a e x => EXIST(b):[b e y & (a,b) e g]]
Suppose...
30 t e x
Premise
31 t e x => f(t) e y
U Spec, 5
32 f(t) e y
Detach, 31, 30
33 ALL(b):[(t,b) e g <=> (t,b) e xy & f(t)=b]
U Spec, 16
34 (t,f(t)) e g <=> (t,f(t)) e xy & f(t)=f(t)
U Spec, 33, 32
35 [(t,f(t)) e g => (t,f(t)) e xy & f(t)=f(t)]
& [(t,f(t)) e xy & f(t)=f(t) => (t,f(t)) e g]
Iff-And, 34
36 (t,f(t)) e xy & f(t)=f(t) => (t,f(t)) e g
Split, 35
37 ALL(c2):[(t,c2) e xy <=> t e x & c2 e y]
U Spec, 12
38 (t,f(t)) e xy <=> t e x & f(t) e y
U Spec, 37, 32
39 [(t,f(t)) e xy => t e x & f(t) e y]
&
[t e x & f(t) e y => (t,f(t)) e xy]
Iff-And, 38
40 t e x & f(t) e y => (t,f(t)) e xy
Split, 39
41 t e x & f(t) e y
Join, 30, 32
42 (t,f(t)) e xy
Detach, 40, 41
43 f(t)=f(t)
Reflex, 32
44 (t,f(t)) e xy & f(t)=f(t)
Join, 42, 43
45 (t,f(t)) e g
Detach, 36, 44
46 f(t) e y & (t,f(t)) e g
Join, 32, 45
47 EXIST(b):[b e y & (t,b) e g]
E Gen, 46
Part 2
As Required:
48 ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e g]]
4 Conclusion, 30
Prove: ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y
=> [(a,b) e g & (a,c) e g => b=c]]
Suppose...
49 t e x & u1 e y & u2 e y
Premise
50 t e x
Split, 49
51 u1 e y
Split, 49
52 u2 e y
Split, 49
Prove: (t,u1) e g & (t,u2) e g => u1=u2
Suppose...
53 (t,u1) e g & (t,u2) e g
Premise
54 (t,u1) e g
Split, 53
55 (t,u2) e g
Split, 53
56 ALL(b):[(t,b) e g <=> (t,b) e xy & f(t)=b]
U Spec, 16
57 (t,u1) e g <=> (t,u1) e xy & f(t)=u1
U Spec, 56
58 [(t,u1) e g => (t,u1) e xy & f(t)=u1]
&
[(t,u1) e xy & f(t)=u1 => (t,u1) e g]
Iff-And, 57
59 (t,u1) e g => (t,u1) e xy & f(t)=u1
Split, 58
60 (t,u1) e xy & f(t)=u1
Detach, 59, 54
61 f(t)=u1
Split, 60
62 (t,u2) e g <=> (t,u2) e xy & f(t)=u2
U Spec, 56
63 [(t,u2) e g => (t,u2) e xy & f(t)=u2]
&
[(t,u2) e xy & f(t)=u2 => (t,u2) e g]
Iff-And, 62
64 (t,u2) e g => (t,u2) e xy & f(t)=u2
Split, 63
65 (t,u2) e xy & f(t)=u2
Detach, 64, 55
66 f(t)=u2
Split, 65
67 u1=u2
Substitute, 61,
66
As Required:
68 (t,u1) e g & (t,u2) e g => u1=u2
4 Conclusion, 53
Part 3
As Required:
69 ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y
=>
[(a,b) e g & (a,c) e g => b=c]]
4 Conclusion, 49
70 Set'(g)
&
ALL(a):ALL(b):[(a,b) e g => a e x & b e y]
Join, 15, 29
71 Set'(g)
&
ALL(a):ALL(b):[(a,b) e g => a e x & b e y]
&
ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e g]]
Join, 70, 48
72 Set'(g)
&
ALL(a):ALL(b):[(a,b) e g => a e x & b e y]
&
ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e g]]
&
ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y
=>
[(a,b) e g & (a,c) e g => b=c]]
Join, 71, 69
As Required:
73 EXIST(f):ALL(a):[a e x => f(a) e y]
=>
EXIST(g):[Set'(g)
&
ALL(a):ALL(b):[(a,b) e g => a e x & b e y]
&
ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e g]]
&
ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y
=>
[(a,b) e g & (a,c) e g => b=c]]]
4 Conclusion, 4
'<='
Prove: EXIST(g):[Set'(g)
& ALL(a):ALL(b):[(a,b) e g => a e x & b e y]
& ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e g]]
& ALL(a):ALL(b):ALL(c):[a
e x & b e y & c e y => [(a,b) e g & (a,c) e g => b=c]]]
=> EXIST(f):ALL(a):[a e x => f(a) e y]
Suppose...
74 EXIST(g):[Set'(g)
&
ALL(a):ALL(b):[(a,b) e g => a e x & b e y]
&
ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e g]]
&
ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y
=>
[(a,b) e g & (a,c) e g => b=c]]]
Premise
75 Set'(g)
&
ALL(a):ALL(b):[(a,b) e g => a e x & b e y]
&
ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e g]]
&
ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y
=>
[(a,b) e g & (a,c) e g => b=c]]
E Spec, 74
76 Set'(g)
Split, 75
77 ALL(a):ALL(b):[(a,b) e g => a e x & b e y]
Split, 75
78 ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e g]]
Split, 75
79 ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y
=>
[(a,b) e g & (a,c) e g => b=c]]
Split, 75
80 ALL(dom):ALL(cod):ALL(gra):[Set(dom) & Set(cod)
& Set'(gra)
=>
[ALL(a1):ALL(b):[(a1,b) e gra => a1 e dom & b e cod]
&
ALL(a1):[a1 e dom => EXIST(b):[b e cod & (a1,b) e gra]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e dom & b1 e cod & b2 e cod
=>
[(a1,b1) e gra & (a1,b2) e gra => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e dom & b e cod
=>
[fun(a1)=b <=> (a1,b) e gra]]]]
Function
81 ALL(cod):ALL(gra):[Set(x) & Set(cod)
& Set'(gra)
=>
[ALL(a1):ALL(b):[(a1,b) e gra => a1 e x & b e cod]
&
ALL(a1):[a1 e x =>
EXIST(b):[b e cod & (a1,b) e gra]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e cod & b2 e cod
=>
[(a1,b1) e gra & (a1,b2) e gra => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e cod
=>
[fun(a1)=b <=> (a1,b) e gra]]]]
U Spec, 80
82 ALL(gra):[Set(x) & Set(y) & Set'(gra)
=>
[ALL(a1):ALL(b):[(a1,b) e gra => a1 e x & b e y]
&
ALL(a1):[a1 e x => EXIST(b):[b e y & (a1,b) e gra]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e y & b2 e y
=>
[(a1,b1) e gra & (a1,b2) e gra => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e y
=>
[fun(a1)=b <=> (a1,b) e gra]]]]
U Spec, 81
83 Set(x) & Set(y) & Set'(g)
=>
[ALL(a1):ALL(b):[(a1,b) e g => a1 e x & b e y]
&
ALL(a1):[a1 e x =>
EXIST(b):[b e y & (a1,b) e g]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e y & b2 e y
=>
[(a1,b1) e g & (a1,b2) e g => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e y
=>
[fun(a1)=b <=> (a1,b) e g]]]
U Spec, 82
84 Set(x) & Set(y) & Set'(g)
Join, 1, 76
85 ALL(a1):ALL(b):[(a1,b) e g => a1 e x & b e y]
&
ALL(a1):[a1 e x =>
EXIST(b):[b e y & (a1,b) e g]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e y & b2 e y
=>
[(a1,b1) e g & (a1,b2) e g => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e y
=>
[fun(a1)=b <=> (a1,b) e g]]
Detach, 83, 84
86 ALL(a):ALL(b):[(a,b) e g => a e x & b e y]
&
ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e g]]
Join, 77, 78
87 ALL(a):ALL(b):[(a,b) e g => a e x & b e y]
&
ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e g]]
&
ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y
=>
[(a,b) e g & (a,c) e g => b=c]]
Join, 86, 79
88 EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e y
=>
[fun(a1)=b <=> (a1,b) e g]]
Detach, 85, 87
89 ALL(a1):ALL(b):[a1 e x & b e y
=>
[f(a1)=b <=> (a1,b) e g]]
E Spec, 88
Prove: ALL(a):[a e x => f(a) e y]
Suppose...
90 t e x
Premise
91 t e x => EXIST(b):[b e y & (t,b) e g]
U Spec, 78
92 EXIST(b):[b e y & (t,b) e g]
Detach, 91, 90
93 u e y & (t,u) e g
E Spec, 92
94 u e y
Split, 93
95 (t,u) e g
Split, 93
96 ALL(b):[t e x & b e y
=>
[f(t)=b <=> (t,b) e g]]
U Spec, 89
97 t e x & u e y
=>
[f(t)=u <=> (t,u) e g]
U Spec, 96
98 t e x & u e y
Join, 90, 94
99 f(t)=u <=> (t,u) e g
Detach, 97, 98
100 [f(t)=u => (t,u) e g] & [(t,u) e g => f(t)=u]
Iff-And, 99
101 (t,u) e g => f(t)=u
Split, 100
102 f(t)=u
Detach, 101, 95
103 f(t) e y
Substitute, 102,
94
As Required:
104 ALL(a):[a e x => f(a) e y]
4 Conclusion, 90
105 EXIST(f):ALL(a):[a e x => f(a) e y]
E Gen, 104
As Required:
106 EXIST(g):[Set'(g)
&
ALL(a):ALL(b):[(a,b) e g => a e x & b e y]
&
ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e g]]
&
ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y
=>
[(a,b) e g & (a,c) e g => b=c]]]
=>
EXIST(f):ALL(a):[a e x => f(a) e y]
4 Conclusion, 74
107 [EXIST(f):ALL(a):[a e x => f(a) e y]
=>
EXIST(g):[Set'(g)
&
ALL(a):ALL(b):[(a,b) e g => a e x & b e y]
&
ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e g]]
&
ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y
=>
[(a,b) e g & (a,c) e g => b=c]]]]
&
[EXIST(g):[Set'(g)
&
ALL(a):ALL(b):[(a,b) e g => a e x & b e y]
&
ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e g]]
&
ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y
=>
[(a,b) e g & (a,c) e g => b=c]]]
=>
EXIST(f):ALL(a):[a e x => f(a) e y]]
Join, 73, 106
108 EXIST(f):ALL(a):[a e x => f(a) e y]
<=>
EXIST(g):[Set'(g)
&
ALL(a):ALL(b):[(a,b) e g => a e x & b e y]
&
ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e g]]
&
ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y
=>
[(a,b) e g & (a,c) e g => b=c]]]
Iff-And, 107
As Required:
109 ALL(x):ALL(y):[Set(x) & Set(y)
=>
[EXIST(f):ALL(a):[a e x => f(a) e y]
<=>
EXIST(g):[Set'(g)
&
ALL(a):ALL(b):[(a,b) e g => a e x & b e y]
&
ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e g]]
&
ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y
=>
[(a,b) e g & (a,c) e g => b=c]]]]]
4 Conclusion, 1