THEOREM
*******
For every set x and y, there
exists a set of graphs (ordered pairs), each of which corresponds a function
mapping x to y.
ALL(x):ALL(y):[Set(x)
& Set(y)
=> EXIST(graphs):[Set(graphs)
& ALL(g):[g e graphs
<=> 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]]]]
& ALL(g):[g e graphs
=> EXIST(fun):ALL(a1):ALL(b):[a1
e x & b e y
=> [fun(a1)=b
<=> (a1,b) e g]]]]]
The revised Function Axiom is
used on line 82.
By Dan Christensen
2022-01-25
This machine-verfied, formal proof was written with the aid of the
author's DC Proof 2.0 freeware available http://www.dcprof.com
PROOF
*****
Let x and y be sets.
1 Set(x) & Set(y)
Premise
2 Set(x)
Split, 1
3 Set(y)
Split, 1
Construct to set of all graphs mapping x to y
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 (Cartesian product
of x and y)
9 Set'(xy)
Split, 8
10 ALL(c1):ALL(c2):[(c1,c2) e xy <=> c1 e x & c2 e y]
Split, 8
Apply Power Set 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 (Power set of xy)
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
17 EXIST(graphs):[Set(graphs) & ALL(g):[g e graphs <=> g e pxy &
[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]]]]]
Subset, 15
18 Set(graphs) & ALL(g):[g e graphs <=> g e pxy &
[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, 17
Define: graphs
(Set of all graphs of functions mapping x to y)
19 Set(graphs)
Split, 18
20 ALL(g):[g e graphs <=> g e pxy &
[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]]]]
Split, 18
Elimainate pxy
term
'=>'
Prove: ALL(g):[g e graphs
=> 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...
21 g e graphs
Premise
22 g e graphs <=> g e pxy & [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]]]
U Spec, 20
23 [g e graphs => g e pxy & [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]]]]
&
[g e pxy & [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]]] => g e graphs]
Iff-And, 22
24 g e graphs => g e pxy & [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]]]
Split, 23
25 g e pxy & [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]]]
Detach, 24, 21
26 g e pxy
Split, 25
27 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]]
Split, 25
Apply definition of pxy
28 g e pxy <=> Set'(g) & ALL(d1):ALL(d2):[(d1,d2) e g => (d1,d2) e xy]
U Spec, 16
29 [g e pxy => Set'(g) & ALL(d1):ALL(d2):[(d1,d2) e g => (d1,d2) e xy]]
&
[Set'(g) & ALL(d1):ALL(d2):[(d1,d2) e g => (d1,d2) e xy] => g e pxy]
Iff-And, 28
30 g e pxy => Set'(g) & ALL(d1):ALL(d2):[(d1,d2) e g => (d1,d2) e xy]
Split, 29
31 Set'(g) & ALL(d1):ALL(d2):[(d1,d2) e g => (d1,d2) e xy]
Detach, 30, 26
32 Set'(g)
Split, 31
33 ALL(d1):ALL(d2):[(d1,d2) e g => (d1,d2) e xy]
Split, 31
34 (t,u) e g
Premise
35 ALL(d2):[(t,d2) e g => (t,d2) e xy]
U Spec, 33
36 (t,u) e g => (t,u) e xy
U Spec, 35
37 (t,u) e xy
Detach, 36, 34
38 ALL(c2):[(t,c2) e xy <=> t e x & c2 e y]
U Spec, 10
39 (t,u) e xy <=> t e x & u e y
U Spec, 38
40 [(t,u) e xy => t e x & u e y]
&
[t e x & u e y => (t,u) e xy]
Iff-And, 39
41 (t,u) e xy => t e x & u e y
Split, 40
42 t e x & u e y
Detach, 41, 37
43 ALL(a):ALL(b):[(a,b) e g => a e x & b e y]
4 Conclusion, 34
44 Set'(g)
&
ALL(a):ALL(b):[(a,b) e g => a e x & b e y]
Join, 32, 43
45 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, 44, 27
As Required:
46 ALL(g):[g e graphs
=>
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, 21
'<='
Prove: ALL(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]]]
=> g e graphs]
Suppose...
47 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
48 Set'(g)
Split, 47
49 ALL(a):ALL(b):[(a,b) e g => a e x & b e y]
Split, 47
50 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]]
Split, 47
51 g e graphs <=> g e pxy & [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]]]
U Spec, 20
52 [g e graphs => g e pxy & [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]]]]
&
[g e pxy & [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]]] => g e graphs]
Iff-And, 51
Sufficient: For g e graphs
53 g e pxy & [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]]] => g e graphs
Split, 52
54 g e pxy <=> Set'(g) & ALL(d1):ALL(d2):[(d1,d2) e g => (d1,d2) e xy]
U Spec, 16
55 [g e pxy => Set'(g) & ALL(d1):ALL(d2):[(d1,d2) e g => (d1,d2) e xy]]
&
[Set'(g) & ALL(d1):ALL(d2):[(d1,d2) e g => (d1,d2) e xy] => g e pxy]
Iff-And, 54
Sufficient: For g e pxy
56 Set'(g) & ALL(d1):ALL(d2):[(d1,d2) e g => (d1,d2) e xy] => g e pxy
Split, 55
Prove: ALL(a):ALL(b):[(a,b) e g => (a,b)
e xy]
Suppose...
57 (t,u) e g
Premise
58 ALL(b):[(t,b) e g => t e x & b e y]
U Spec, 49
59 (t,u) e g => t e x & u e y
U Spec, 58
60 t e x & u e y
Detach, 59, 57
61 ALL(c2):[(t,c2) e xy <=> t e x & c2 e y]
U Spec, 10
62 (t,u) e xy <=> t e x & u e y
U Spec, 61
63 [(t,u) e xy => t e x & u e y]
&
[t e x & u e y => (t,u) e xy]
Iff-And, 62
Sufficient: For (t,u)
e xy
64 t e x & u e y => (t,u) e xy
Split, 63
65 (t,u) e xy
Detach, 64, 60
As Required:
66 ALL(a):ALL(b):[(a,b) e g => (a,b) e xy]
4 Conclusion, 57
67 Set'(g) & ALL(a):ALL(b):[(a,b) e g => (a,b) e xy]
Join, 48, 66
68 g e pxy
Detach, 56, 67
69 g e pxy
&
[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, 68, 50
70 g e graphs
Detach, 53, 69
As Required:
71 ALL(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]]]
=>
g e graphs]
4 Conclusion, 47
Joining results...
72 ALL(g):[[g e graphs
=>
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]]]] & [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]]]
=>
g e graphs]]
Join, 46, 71
As Required:
73 ALL(g):[g e graphs
<=>
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, 72
Prove: ALL(g):[g e graphs
=> EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e y
=> [fun(a1)=b <=> (a1,b) e g]]]
Suppose...
74 g e graphs
Premise
Apply definition of graphs
75 g e graphs
<=>
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]]]
U Spec, 73
76 [g e graphs => 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]]]]
&
[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]]] => g e graphs]
Iff-And, 75
77 g e graphs => 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]]]
Split, 76
78 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]]]
Detach, 77, 74
79 Set'(g)
Split, 78
80 ALL(a):ALL(b):[(a,b) e g => a e x & b e y]
Split, 78
81 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]]
Split, 78
Apply Function Axiom (1 variable)
82 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
83 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, 82
84 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, 83
85 ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e g]]
Split, 81
86 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, 81
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]]
Join, 80, 85
88 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, 84
89 Set(x) & Set(y) & Set'(g)
Join, 1, 79
90 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, 88, 89
91 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, 80, 85
92 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, 91, 86
93 EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e y
=>
[fun(a1)=b <=> (a1,b) e g]]
Detach, 90, 92
As Required:
94 ALL(g):[g e graphs
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e y
=>
[fun(a1)=b <=> (a1,b) e g]]]
4 Conclusion, 74
95 Set(graphs)
&
ALL(g):[g e graphs
<=>
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, 19, 73
96 Set(graphs)
&
ALL(g):[g e graphs
<=>
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]]]]
&
ALL(g):[g e graphs
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e y
=>
[fun(a1)=b <=> (a1,b) e g]]]
Join, 95, 94
As Required:
97 ALL(x):ALL(y):[Set(x) & Set(y)
=>
EXIST(graphs):[Set(graphs)
&
ALL(g):[g e graphs
<=>
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]]]]
&
ALL(g):[g e graphs
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e y
=>
[fun(a1)=b <=> (a1,b) e g]]]]]
4 Conclusion, 1