THEOREM
*******
ALL(x):[Set(x)
=> EXIST(f):ALL(a):[a e null => f(a) e x]]
Where null is the empty set.
By Dan Christensen
2024-05-28
Define: null (the empty set)
1 Set(null)
Axiom
2 ALL(a):~a e null
Axiom
Suppose x is an arbitrary set
3 Set(x)
Premise
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(null) & Set(a2) => EXIST(b):[Set'(b)
& ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e null & c2 e a2]]]
U Spec, 4
6 Set(null) & Set(x) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e null & c2 e x]]
U Spec, 5
7 Set(null) & Set(x)
Join, 1, 3
8 EXIST(b):[Set'(b)
& ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e null & c2 e x]]
Detach, 6, 7
Define: g
(the required graph set)
9 Set'(g) & ALL(c1):ALL(c2):[(c1,c2) e g <=> c1 e null & c2 e x]
E Spec, 8
10 Set'(g)
Split, 9
11 ALL(c1):ALL(c2):[(c1,c2) e g <=> c1 e null & c2 e x]
Split, 9
Apply Function Axiom
12 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):[Function(fun,dom,cod) &
ALL(a1):ALL(b):[a1 e dom & b e cod
=>
[fun(a1)=b <=> (a1,b) e gra]]]]]
Function
13 ALL(cod):ALL(gra):[Set(null) & Set(cod)
& Set'(gra)
=>
[ALL(a1):ALL(b):[(a1,b) e gra => a1 e null & b e cod]
&
ALL(a1):[a1 e null =>
EXIST(b):[b e cod & (a1,b) e gra]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e null & b1 e cod & b2 e cod
=>
[(a1,b1) e gra & (a1,b2) e gra => b1=b2]]
=>
EXIST(fun):[Function(fun,null,cod) & ALL(a1):ALL(b):[a1 e null & b e cod
=>
[fun(a1)=b <=> (a1,b) e gra]]]]]
U Spec, 12
14 ALL(gra):[Set(null) & Set(x) & Set'(gra)
=>
[ALL(a1):ALL(b):[(a1,b) e gra => a1 e null & b e x]
&
ALL(a1):[a1 e null =>
EXIST(b):[b e x & (a1,b) e gra]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e null & b1 e x & b2 e x
=>
[(a1,b1) e gra & (a1,b2) e gra => b1=b2]]
=>
EXIST(fun):[Function(fun,null,x) & ALL(a1):ALL(b):[a1 e null & b e x
=>
[fun(a1)=b <=> (a1,b) e gra]]]]]
U Spec, 13
15 Set(null) & Set(x) & Set'(g)
=>
[ALL(a1):ALL(b):[(a1,b) e g => a1 e null & b e x]
&
ALL(a1):[a1 e null =>
EXIST(b):[b e x & (a1,b) e g]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e null & b1 e x & b2 e x
=>
[(a1,b1) e g & (a1,b2) e g => b1=b2]]
=>
EXIST(fun):[Function(fun,null,x) & ALL(a1):ALL(b):[a1 e null & b e x
=>
[fun(a1)=b <=> (a1,b) e g]]]]
U Spec, 14
16 Set(null) & Set(x)
Join, 1, 3
17 Set(null) & Set(x) & Set'(g)
Join, 16, 10
Sufficient: For functionality of set g
18 ALL(a1):ALL(b):[(a1,b) e g => a1 e null & b e x]
&
ALL(a1):[a1 e null =>
EXIST(b):[b e x & (a1,b) e g]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e null & b1 e x & b2 e x
=>
[(a1,b1) e g & (a1,b2) e g => b1=b2]]
=>
EXIST(fun):[Function(fun,null,x) & ALL(a1):ALL(b):[a1 e null & b e x
=>
[fun(a1)=b <=> (a1,b) e g]]]
Detach, 15, 17
Part 1
Prove: ALL(a1):ALL(b):[(a1,b) e g => a1 e null & b e x]
Suppose...
19 (y,z) e g
Premise
Apply definition of g
20 ALL(c2):[(y,c2) e g <=> y e null & c2 e x]
U Spec, 11
21 (y,z) e g <=> y e null & z e x
U Spec, 20
22 [(y,z) e g => y e null & z e x]
&
[y e null & z e x => (y,z) e g]
Iff-And, 21
23 (y,z) e g => y e null & z e x
Split, 22
24 y e null & z e x
Detach, 23, 19
Part 1
As Required:
25 ALL(a1):ALL(b):[(a1,b) e g => a1 e null & b e x]
4 Conclusion, 19
Prove: ALL(a1):[a1 e null => EXIST(b):[b e x &
(a1,b) e g]]
Suppose...
26 y e null
Premise
Apply definition of null
27 ~y e null
U Spec, 2
Apply principle of vacuous truth
28 ~y e null => EXIST(b):[b e x & (y,b) e g]
Arb Cons, 26
29 EXIST(b):[b e x & (y,b) e g]
Detach, 28, 27
Part 2
As Required:
30 ALL(a1):[a1 e null =>
EXIST(b):[b e x & (a1,b) e g]]
4 Conclusion, 26
Part 3
Prove: ALL(a1):ALL(b1):ALL(b2):[a1 e null & b1 e x & b2 e x
=> [(a1,b1) e g & (a1,b2) e g => b1=b2]]
Suppose...
31 y e null & z1 e x & z2 e x
Premise
32 y e null
Split, 31
33 ~y e null
U Spec, 2
34 ~y e null => [(y,z1) e g & (y,z2) e g => z1=z2]
Arb Cons, 32
35 (y,z1) e g & (y,z2) e g => z1=z2
Detach, 34, 33
Part 3
As Required:
36 ALL(a1):ALL(b1):ALL(b2):[a1 e null & b1 e x & b2 e x
=>
[(a1,b1) e g & (a1,b2) e g => b1=b2]]
4 Conclusion, 31
Joining results...
37 ALL(a1):ALL(b):[(a1,b) e g => a1 e null & b e x]
&
ALL(a1):[a1 e null =>
EXIST(b):[b e x & (a1,b) e g]]
Join, 25, 30
38 ALL(a1):ALL(b):[(a1,b) e g => a1 e null & b e x]
&
ALL(a1):[a1 e null =>
EXIST(b):[b e x & (a1,b) e g]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e null & b1 e x & b2 e x
=>
[(a1,b1) e g & (a1,b2) e g => b1=b2]]
Join, 37, 36
39 EXIST(fun):[Function(fun,null,x)
& ALL(a1):ALL(b):[a1 e null & b e x
=>
[fun(a1)=b <=> (a1,b) e g]]]
Detach, 18, 38
Define: f
(function)
40 Function(f,null,x) &
ALL(a1):ALL(b):[a1 e null & b e x
=>
[f(a1)=b <=> (a1,b) e g]]
E Spec, 39
41 Function(f,null,x)
Split, 40
42 ALL(a1):ALL(b):[a1 e null & b e x
=>
[f(a1)=b <=> (a1,b) e g]]
Split, 40
Prove: ALL(a):[a e null => f(a) e x]
Suppose...
43 y e null
Premise
Apply Part 2
44 y e null => EXIST(b):[b e x & (y,b) e g]
U Spec, 30
45 EXIST(b):[b e x & (y,b) e g]
Detach, 44, 43
Define: z
46 z e x & (y,z) e g
E Spec, 45
47 z e x
Split, 46
48 (y,z) e g
Split, 46
Apply functionality of g
49 ALL(b):[y e null & b e x
=>
[f(y)=b <=> (y,b) e g]]
U Spec, 42
50 y e null & z e x
=>
[f(y)=z <=> (y,z) e g]
U Spec, 49
51 y e null & z e x
Join, 43, 47
52 f(y)=z <=> (y,z) e g
Detach, 50, 51
53 [f(y)=z => (y,z) e g] & [(y,z) e g => f(y)=z]
Iff-And, 52
54 (y,z) e g => f(y)=z
Split, 53
55 f(y)=z
Detach, 54, 48
56 f(y) e x
Substitute, 55,
47
As Required:
57 ALL(a):[a e null => f(a) e x]
4 Conclusion, 43
As Required:
58 ALL(x):[Set(x) => EXIST(f):ALL(a):[a e null => f(a) e x]]
4 Conclusion, 3