THEOREM
*******
Given sets x and y, and
function f mapping x to y, there exists a unique set fxy
= {(a,b)|a e x & b ey &
f(a)=b}. Here, we foramally prove:
ALL(x):ALL(y):[Set(x)
& Set(y)
=> ALL(f):[ALL(a):[a
e x => f(a) e y]
=> EXIST(fxy):[Set'(fxy) & ALL(a):ALL(b):[(a,b) e fxy <=> a e x & b e y &
f(a)=b]
& ALL(fxy'):[Set'(fxy') & ALL(a):ALL(b):[(a,b) e fxy' <=> a e x & b e y &
f(a)=b]=> fxy'=fxy]]]]
& ALL(a):ALL(b):[(a,b) e fxy => a
e x & b e y]
& ALL(a):[a e x => EXIST(b):[b e y & (a,b) e fxy]]
& ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y => [(a,b) e fxy & (a,c) e fxy =>
b=c]]]]]
Note that the Function Axiom
(not used in this proof) allows you to introduce functional notation (e.g.
y=f(x)) given a set of ordered pairs. Here we work it backwards, introducing a
set of ordered pairs from functional notation.
By Dan Christensen
2022-01-07
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
PROOF
*****
Let x and y be sets
1 Set(x) & Set(y)
Premise
Suppose...
2 ALL(a):[a e x => f(a) e y]
Premise
Apply the Cartesian Product Axiom
3 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
4 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, 3
5 Set(x) & Set(y) => EXIST(b):[Set'(b) &
ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e y]]
U Spec, 4
6 EXIST(b):[Set'(b)
& ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e y]]
Detach, 5, 1
7 Set'(xy) & ALL(c1):ALL(c2):[(c1,c2) e xy <=> c1 e x & c2 e y]
E Spec, 6
Define: xy
8 Set'(xy)
Split, 7
9 ALL(c1):ALL(c2):[(c1,c2) e xy <=> c1 e x & c2 e y]
Split, 7
Apply the Subset Axiom
10 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e xy & f(a)=b]]
Subset, 8
11 Set'(fxy) &
ALL(a):ALL(b):[(a,b) e fxy <=> (a,b) e xy & f(a)=b]
E Spec, 10
Define: fxy
12 Set'(fxy)
Split, 11
13 ALL(a):ALL(b):[(a,b) e fxy <=> (a,b) e xy & f(a)=b]
Split, 11
'=>
Prove: ALL(a):ALL(b):[(a,b) e fxy => a
e x & b e y &
f(a)=b]
Suppose...
14 (t,u) e fxy
Premise
Apply the definition of fxy
15 ALL(b):[(t,b) e fxy <=> (t,b) e xy & f(t)=b]
U Spec, 13
16 (t,u) e fxy <=> (t,u) e xy & f(t)=u
U Spec, 15
17 [(t,u) e fxy => (t,u) e xy & f(t)=u]
&
[(t,u) e xy & f(t)=u => (t,u) e fxy]
Iff-And, 16
18 (t,u) e fxy => (t,u) e xy & f(t)=u
Split, 17
19 (t,u) e xy & f(t)=u
Detach, 18, 14
20 (t,u) e xy
Split, 19
21 f(t)=u
Split, 19
Apply the definition of xy
22 ALL(c2):[(t,c2) e xy <=> t e x & c2 e y]
U Spec, 9
23 (t,u) e xy <=> t e x & u e y
U Spec, 22
24 [(t,u) e xy => t e x & u e y]
&
[t e x & u e y => (t,u) e xy]
Iff-And, 23
25 (t,u) e xy => t e x & u e y
Split, 24
26 t e x & u e y
Detach, 25, 20
27 t e x & u e y & f(t)=u
Join, 26, 21
As Required:
28 ALL(a):ALL(b):[(a,b) e fxy => a e x & b e y & f(a)=b]
4 Conclusion, 14
'<='
Prove: ALL(a):ALL(b):[a e x & b e y &
f(a)=b => (a,b) e fxy]
Suppose...
29 t e x & u e y & f(t)=u
Premise
Apply the definition of fxy
30 ALL(b):[(t,b) e fxy <=> (t,b) e xy & f(t)=b]
U Spec, 13
31 (t,u) e fxy <=> (t,u) e xy & f(t)=u
U Spec, 30
32 [(t,u) e fxy => (t,u) e xy & f(t)=u]
&
[(t,u) e xy & f(t)=u => (t,u) e fxy]
Iff-And, 31
Sufficient: For (t,u)
e fxy
33 (t,u) e xy & f(t)=u => (t,u) e fxy
Split, 32
34 ALL(c2):[(t,c2) e xy <=> t e x & c2 e y]
U Spec, 9
35 (t,u) e xy <=> t e x & u e y
U Spec, 34
36 [(t,u) e xy => t e x & u e y]
&
[t e x & u e y => (t,u) e xy]
Iff-And, 35
37 t e x & u e y => (t,u) e xy
Split, 36
38 t e x
Split, 29
39 u e y
Split, 29
40 f(t)=u
Split, 29
41 t e x & u e y
Join, 38, 39
42 (t,u) e xy
Detach, 37, 41
43 (t,u) e xy & f(t)=u
Join, 42, 40
44 (t,u) e fxy
Detach, 33, 43
As Required:
45 ALL(a):ALL(b):[a e x & b e y & f(a)=b => (a,b) e fxy]
4 Conclusion, 29
46 ALL(a):ALL(b):[[(a,b) e fxy => a e x & b e y & f(a)=b] & [a e x & b e y & f(a)=b => (a,b) e fxy]]
Join, 28, 45
Alternative definition of fxy
(without reference to xy):
47 ALL(a):ALL(b):[(a,b) e fxy
<=>
a e x & b e y & f(a)=b]
Iff-And, 46
Prove fxy is unique. Let fxy' be another such set.
Suppose...
48 Set'(fxy') & ALL(a):ALL(b):[(a,b) e fxy' <=> a e x & b e y & f(a)=b]
Premise
49 Set'(fxy')
Split, 48
50 ALL(a):ALL(b):[(a,b) e fxy' <=> a e x & b e y & f(a)=b]
Split, 48
Apply Set Equality Axiom
51 ALL(a):ALL(b):[Set'(a) & Set'(b) =>
[a=b
<=>
ALL(c1):ALL(c2):[(c1,c2) e a <=>
(c1,c2) e b]]]
Set Equality
52 ALL(b):[Set'(fxy') & Set'(b)
=> [fxy'=b
<=>
ALL(c1):ALL(c2):[(c1,c2) e fxy' <=> (c1,c2) e b]]]
U Spec, 51
53 Set'(fxy') & Set'(fxy) => [fxy'=fxy
<=>
ALL(c1):ALL(c2):[(c1,c2) e fxy' <=> (c1,c2) e fxy]]
U Spec, 52
54 Set'(fxy') & Set'(fxy)
Join, 49, 12
55 fxy'=fxy
<=>
ALL(c1):ALL(c2):[(c1,c2) e fxy' <=> (c1,c2) e fxy]
Detach, 53, 54
56 [fxy'=fxy => ALL(c1):ALL(c2):[(c1,c2) e fxy' <=>
(c1,c2) e fxy]]
&
[ALL(c1):ALL(c2):[(c1,c2) e fxy' <=>
(c1,c2) e fxy] => fxy'=fxy]
Iff-And, 55
Sufficient: For fxy'=fxy
57 ALL(c1):ALL(c2):[(c1,c2) e fxy' <=>
(c1,c2) e fxy] => fxy'=fxy
Split, 56
'=>'
Prove: ALL(a):ALL(b):[(a,b) e fxy' =>
(a,b) e fxy]
Suppose...
58 (t,u) e fxy'
Premise
Apply definition of fxy'
59 ALL(b):[(t,b) e fxy' <=> t e x & b e y & f(t)=b]
U Spec, 50
60 (t,u) e fxy' <=> t e x & u e y & f(t)=u
U Spec, 59
61 [(t,u) e fxy' => t e x & u e y & f(t)=u]
&
[t e x & u e y & f(t)=u => (t,u) e fxy']
Iff-And, 60
62 (t,u) e fxy' => t e x & u e y & f(t)=u
Split, 61
63 t e x & u e y & f(t)=u
Detach, 62, 58
Apply alternative definition of fxy
64 ALL(b):[(t,b) e fxy
<=>
t e x & b e y & f(t)=b]
U Spec, 47
65 (t,u) e fxy
<=>
t e x & u e y & f(t)=u
U Spec, 64
66 [(t,u) e fxy => t e x & u e y & f(t)=u]
&
[t e x & u e y & f(t)=u => (t,u) e fxy]
Iff-And, 65
67 t e x & u e y & f(t)=u => (t,u) e fxy
Split, 66
68 (t,u) e fxy
Detach, 67, 63
As Required:
69 ALL(a):ALL(b):[(a,b) e fxy' => (a,b) e fxy]
4 Conclusion, 58
'<='
Prove: ALL(a):ALL(b):[(a,b) e fxy => (a,b) e fxy']
Suppose...
70 (t,u) e fxy
Premise
Apply alternative definition of fxy
71 ALL(b):[(t,b) e fxy
<=>
t e x & b e y & f(t)=b]
U Spec, 47
72 (t,u) e fxy
<=>
t e x & u e y & f(t)=u
U Spec, 71
73 [(t,u) e fxy => t e x & u e y & f(t)=u]
&
[t e x & u e y & f(t)=u => (t,u) e fxy]
Iff-And, 72
74 (t,u) e fxy => t e x & u e y & f(t)=u
Split, 73
75 t e x & u e y & f(t)=u
Detach, 74, 70
Apply definition of fxy'
76 ALL(b):[(t,b) e fxy' <=> t e x & b e y & f(t)=b]
U Spec, 50
77 (t,u) e fxy' <=> t e x & u e y & f(t)=u
U Spec, 76
78 [(t,u) e fxy' => t e x & u e y & f(t)=u]
&
[t e x & u e y & f(t)=u => (t,u) e fxy']
Iff-And, 77
79 t e x & u e y & f(t)=u => (t,u) e fxy'
Split, 78
80 (t,u) e fxy'
Detach, 79, 75
As Required:
81 ALL(a):ALL(b):[(a,b) e fxy => (a,b) e fxy']
4 Conclusion, 70
82 ALL(a):ALL(b):[[(a,b) e fxy' => (a,b) e fxy] & [(a,b) e fxy => (a,b) e fxy']]
Join, 69, 81
83 ALL(a):ALL(b):[(a,b) e fxy' <=> (a,b) e fxy]
Iff-And, 82
84 fxy'=fxy
Detach, 57, 83
As Required:
85 ALL(fxy'):[Set'(fxy')
& ALL(a):ALL(b):[(a,b) e fxy' <=> a e x & b e y & f(a)=b]
=>
fxy'=fxy]
4 Conclusion, 48
Prove: ALL(a):ALL(b):[(a,b) e fxy => a
e x & b e y]
Suppose...
86 (t,u) e fxy
Premise
Apply alternative definition of fxy
87 ALL(b):[(t,b) e fxy
<=>
t e x & b e y & f(t)=b]
U Spec, 47
88 (t,u) e fxy
<=>
t e x & u e y & f(t)=u
U Spec, 87
89 [(t,u) e fxy => t e x & u e y & f(t)=u]
&
[t e x & u e y & f(t)=u => (t,u) e fxy]
Iff-And, 88
90 (t,u) e fxy => t e x & u e y & f(t)=u
Split, 89
91 t e x & u e y & f(t)=u
Detach, 90, 86
92 t e x
Split, 91
93 u e y
Split, 91
94 t e x & u e y
Join, 92, 93
As Required:
95 ALL(a):ALL(b):[(a,b) e fxy => a e x & b e y]
4 Conclusion, 86
Prove: ALL(a):[a e x => EXIST(b):[b e y & (a,b) e fxy]]
Suppose...
96 t e x
Premise
Apply definition of f
97 t e x => f(t) e y
U Spec, 2
98 f(t) e y
Detach, 97, 96
Apply alternative definition of f
99 ALL(b):[(t,b) e fxy
<=>
t e x & b e y & f(t)=b]
U Spec, 47
100 (t,f(t)) e fxy
<=>
t e x & f(t) e y & f(t)=f(t)
U Spec, 99, 98
101 [(t,f(t)) e fxy => t e x & f(t) e y & f(t)=f(t)]
&
[t e x & f(t) e y & f(t)=f(t) => (t,f(t)) e fxy]
Iff-And, 100
102 t e x & f(t) e y & f(t)=f(t) => (t,f(t)) e fxy
Split, 101
103 f(t)=f(t)
Reflex, 98
104 t e x & f(t) e y
Join, 96, 98
105 t e x & f(t) e y & f(t)=f(t)
Join, 104, 103
106 (t,f(t)) e fxy
Detach, 102, 105
107 f(t) e y & (t,f(t)) e fxy
Join, 98, 106
108 EXIST(b):[b e y & (t,b) e fxy]
E Gen, 107
As Required:
109 ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e fxy]]
4 Conclusion, 96
Prove: ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y => [(a,b) e fxy & (a,c)
e fxy => b=c]]
Suppose...
110 t e x & u1 e y & u2 e y
Premise
Prove: (t,u1) e fxy & (t,u2) e fxy => u1=u2
Suppose...
111 (t,u1) e fxy & (t,u2) e fxy
Premise
112 (t,u1) e fxy
Split, 111
113 (t,u2) e fxy
Split, 111
Apply alternative definition of fxy
114 ALL(b):[(t,b) e fxy
<=>
t e x & b e y & f(t)=b]
U Spec, 47
115 (t,u1) e fxy
<=>
t e x & u1 e y & f(t)=u1
U Spec, 114
116 [(t,u1) e fxy => t e x & u1 e y & f(t)=u1]
&
[t e x & u1 e y & f(t)=u1 => (t,u1) e fxy]
Iff-And, 115
117 (t,u1) e fxy => t e x & u1 e y & f(t)=u1
Split, 116
118 t e x & u1 e y & f(t)=u1
Detach, 117, 112
119 f(t)=u1
Split, 118
120 (t,u2) e fxy
<=>
t e x & u2 e y & f(t)=u2
U Spec, 114
121 [(t,u2) e fxy => t e x & u2 e y & f(t)=u2]
&
[t e x & u2 e y & f(t)=u2 => (t,u2) e fxy]
Iff-And, 120
122 (t,u2) e fxy => t e x & u2 e y & f(t)=u2
Split, 121
123 t e x & u2 e y & f(t)=u2
Detach, 122, 113
124 f(t)=u2
Split, 123
125 u1=u2
Substitute, 119,
124
As Required:
126 (t,u1) e fxy & (t,u2) e fxy => u1=u2
4 Conclusion, 111
As Required:
127 ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y
=>
[(a,b) e fxy & (a,c) e fxy => b=c]]
4 Conclusion, 110
128 Set'(fxy)
&
ALL(a):ALL(b):[(a,b) e fxy
<=>
a e x & b e y & f(a)=b]
Join, 12, 47
129 Set'(fxy)
&
ALL(a):ALL(b):[(a,b) e fxy
<=>
a e x & b e y & f(a)=b]
&
ALL(fxy'):[Set'(fxy') &
ALL(a):ALL(b):[(a,b) e fxy' <=> a e x & b e y & f(a)=b]
=>
fxy'=fxy]
Join, 128, 85
130 Set'(fxy)
&
ALL(a):ALL(b):[(a,b) e fxy
<=>
a e x & b e y & f(a)=b]
&
ALL(fxy'):[Set'(fxy') &
ALL(a):ALL(b):[(a,b) e fxy' <=> a e x & b e y & f(a)=b]
=>
fxy'=fxy]
&
ALL(a):ALL(b):[(a,b) e fxy => a e x & b e y]
Join, 129, 95
131 Set'(fxy)
&
ALL(a):ALL(b):[(a,b) e fxy
<=>
a e x & b e y & f(a)=b]
&
ALL(fxy'):[Set'(fxy') &
ALL(a):ALL(b):[(a,b) e fxy' <=> a e x & b e y & f(a)=b]
=>
fxy'=fxy]
&
ALL(a):ALL(b):[(a,b) e fxy => a e x & b e y]
&
ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e fxy]]
Join, 130, 109
132 Set'(fxy)
&
ALL(a):ALL(b):[(a,b) e fxy
<=>
a e x & b e y & f(a)=b]
&
ALL(fxy'):[Set'(fxy') &
ALL(a):ALL(b):[(a,b) e fxy' <=> a e x & b e y & f(a)=b]
=>
fxy'=fxy]
&
ALL(a):ALL(b):[(a,b) e fxy => a e x & b e y]
&
ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e fxy]]
&
ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y
=>
[(a,b) e fxy & (a,c) e fxy => b=c]]
Join, 131, 127
As Required:
133 ALL(f):[ALL(a):[a e x => f(a) e y]
=>
EXIST(fxy):[Set'(fxy)
&
ALL(a):ALL(b):[(a,b) e fxy
<=>
a e x & b e y & f(a)=b]
&
ALL(fxy'):[Set'(fxy') &
ALL(a):ALL(b):[(a,b) e fxy' <=> a e x & b e y & f(a)=b]
=>
fxy'=fxy]
&
ALL(a):ALL(b):[(a,b) e fxy => a e x & b e y]
&
ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e fxy]]
&
ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y
=>
[(a,b) e fxy & (a,c) e fxy => b=c]]]]
4 Conclusion, 2
As Required:
134 ALL(x):ALL(y):[Set(x) & Set(y)
=>
ALL(f):[ALL(a):[a e x => f(a) e y]
=>
EXIST(fxy):[Set'(fxy)
&
ALL(a):ALL(b):[(a,b) e fxy
<=>
a e x & b e y & f(a)=b]
&
ALL(fxy'):[Set'(fxy') &
ALL(a):ALL(b):[(a,b) e fxy' <=> a e x & b e y & f(a)=b]
=>
fxy'=fxy]
&
ALL(a):ALL(b):[(a,b) e fxy => a e x & b e y]
&
ALL(a):[a e x =>
EXIST(b):[b e y & (a,b) e fxy]]
&
ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y
=>
[(a,b) e fxy & (a,c) e fxy => b=c]]]]]
4 Conclusion, 1