THEOREM
*******
For any injective (1-1)
function f1: x --> y, where x is non-empty set, there exists
a surjective function f2: y --> x
ALL(a):ALL(b):ALL(f1):[Set(a)
& EXIST(c):c e a & Set(b) (non-empty set a)
& ALL(c):[c e a => f1(c) e b] (function f1: a --> b)
& ALL(c):ALL(d):[c
e a & d e a =>
[f1(c)=f1(d) => c=d]] (f1 is
injective)
=> EXIST(f2):[ALL(c):[c
e b => f2(c) e a] (function f2: b --> a]
& ALL(c):[c e a => EXIST(d):[d e b & f2(d)=c]]]] (f2 is surjective)
By Dan Christensen
2022-06-04
This machine-verified formal
proof was written with the aid of the author's DC Proof 2.0 software available
at http://www.dcproof.com
PROOF
*****
Suppose...
1 Set(x) & EXIST(c):c e x & Set(y)
&
ALL(c):[c e x => f(c) e y]
&
ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]
Premise
2 Set(x)
Split, 1
Non-empty set x
3 EXIST(c):c e x
Split, 1
4 Set(y)
Split, 1
Function f: x --> y
5 ALL(c):[c e x => f(c) e y]
Split, 1
f is injective
6 ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]
Split, 1
Define: x0
7 x0 e x
E Spec, 3
Construct image f(x)
8 EXIST(sub):[Set(sub)
& ALL(a):[a e sub <=> a e y & EXIST(b):[b e x & f(b)=a]]]
Subset, 4
9 Set(fx) &
ALL(a):[a e fx <=> a e y & EXIST(b):[b e x & f(b)=a]]
E Spec, 8
Define: fx (image of x under f)
10 Set(fx)
Split, 9
11 ALL(a):[a e fx <=> a e y & EXIST(b):[b e x & f(b)=a]]
Split, 9
Construct graph set for function f': fx --> x
(f' is the inverse of f on fx)
Apply Cartesian Product Axiom
12 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
13 ALL(a2):[Set(fx) & Set(a2)
=> EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e fx & c2 e a2]]]
U Spec, 12
14 Set(fx) & Set(x) =>
EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e fx & c2 e x]]
U Spec, 13
15 Set(fx) & Set(x)
Join, 10, 2
16 EXIST(b):[Set'(b) &
ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e fx & c2 e x]]
Detach, 14, 15
17 Set'(fxx) & ALL(c1):ALL(c2):[(c1,c2) e fxx <=> c1 e fx & c2 e x]
E Spec, 16
Define: fxx (Cartesian product
of fx and x)
18 Set'(fxx)
Split, 17
19 ALL(c1):ALL(c2):[(c1,c2) e fxx <=> c1 e fx & c2 e x]
Split, 17
Construct graph set of f'
20 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e fxx & a=f(b)]]
Subset, 18
21 Set'(graf') &
ALL(a):ALL(b):[(a,b) e graf' <=> (a,b) e fxx & a=f(b)]
E Spec, 20
Define: graf' (graph set for
function f')
22 Set'(graf')
Split, 21
23 ALL(a):ALL(b):[(a,b) e graf' <=> (a,b) e fxx & a=f(b)]
Split, 21
Establish sufficient conditions for functionality of graf'
Apply Function Axiom
24 ALL(dom):ALL(cod):ALL(gra):[Set(dom) & Set(cod)
& Set'(gra)
&
EXIST(a1):a1 e dom & EXIST(a1):a1 e cod
=>
[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
25 ALL(cod):ALL(gra):[Set(fx) & Set(cod) & Set'(gra)
&
EXIST(a1):a1 e fx & EXIST(a1):a1 e cod
=>
[ALL(a1):ALL(b):[(a1,b) e gra => a1 e fx & b e cod]
&
ALL(a1):[a1 e fx => EXIST(b):[b e cod & (a1,b) e gra]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e fx & b1 e cod & b2 e cod
=>
[(a1,b1) e gra & (a1,b2) e gra => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e fx & b e cod
=>
[fun(a1)=b <=> (a1,b) e gra]]]]
U Spec, 24
26 ALL(gra):[Set(fx) & Set(x) & Set'(gra)
&
EXIST(a1):a1 e fx & EXIST(a1):a1 e x
=>
[ALL(a1):ALL(b):[(a1,b) e gra => a1 e fx & b e x]
& ALL(a1):[a1 e fx =>
EXIST(b):[b e x & (a1,b) e gra]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e fx & b1 e x & b2 e x
=>
[(a1,b1) e gra & (a1,b2) e gra => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e fx & b e x
=>
[fun(a1)=b <=> (a1,b) e gra]]]]
U Spec, 25
27 Set(fx) & Set(x) & Set'(graf')
&
EXIST(a1):a1 e fx & EXIST(a1):a1 e x
=>
[ALL(a1):ALL(b):[(a1,b) e graf' => a1 e fx & b e x]
&
ALL(a1):[a1 e fx => EXIST(b):[b e x & (a1,b) e graf']]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e fx & b1 e x & b2 e x
=>
[(a1,b1) e graf' & (a1,b2) e graf' => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e fx & b e x
=>
[fun(a1)=b <=> (a1,b) e graf']]]
U Spec, 26
Prove: EXIST(a1):a1 e fx
(namely f(x0))
28 x0 e x => f(x0) e y
U Spec, 5
29 f(x0) e y
Detach, 28, 7
30 f(x0) e fx <=> f(x0) e y & EXIST(b):[b e x & f(b)=f(x0)]
U Spec, 11, 29
31 [f(x0) e fx => f(x0) e y & EXIST(b):[b e x & f(b)=f(x0)]]
&
[f(x0) e y & EXIST(b):[b e x & f(b)=f(x0)] => f(x0) e fx]
Iff-And, 30
32 f(x0) e y & EXIST(b):[b e x & f(b)=f(x0)] => f(x0) e fx
Split, 31
33 f(x0)=f(x0)
Reflex, 29
34 x0 e x & f(x0)=f(x0)
Join, 7, 33
35 EXIST(b):[b e x & f(b)=f(x0)]
E Gen, 34
36 f(x0) e y & EXIST(b):[b e x & f(b)=f(x0)]
Join, 29, 35
37 f(x0) e fx
Detach, 32, 36
As Required:
38 EXIST(a1):a1 e fx
E Gen, 37
39 Set(fx) & Set(x)
Join, 10, 2
40 Set(fx) & Set(x) & Set'(graf')
Join, 39, 22
41 Set(fx) & Set(x) & Set'(graf')
&
EXIST(a1):a1 e fx
Join, 40, 38
42 Set(fx) & Set(x) & Set'(graf')
&
EXIST(a1):a1 e fx
&
EXIST(c):c e x
Join, 41, 3
Sufficient: For functionality of graf'
43 ALL(a1):ALL(b):[(a1,b) e graf' => a1 e fx & b e x]
&
ALL(a1):[a1 e fx => EXIST(b):[b e x & (a1,b) e graf']]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e fx & b1 e x & b2 e x
=>
[(a1,b1) e graf' & (a1,b2) e graf' => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e fx & b e x
=>
[fun(a1)=b <=> (a1,b) e graf']]
Detach, 27, 42
Prove: ALL(a1):ALL(b):[(a1,b) e graf' => a1 e fx & b e x]
Suppose...
44 (t,u) e graf'
Premise
45 ALL(b):[(t,b) e graf' <=> (t,b) e fxx & t=f(b)]
U Spec, 23
46 (t,u) e graf' <=> (t,u) e fxx & t=f(u)
U Spec, 45
47 [(t,u) e graf' => (t,u) e fxx & t=f(u)]
&
[(t,u) e fxx & t=f(u) => (t,u) e graf']
Iff-And, 46
48 (t,u) e graf' => (t,u) e fxx & t=f(u)
Split, 47
49 (t,u) e fxx & t=f(u)
Detach, 48, 44
50 (t,u) e fxx
Split, 49
51 ALL(c2):[(t,c2) e fxx <=> t e fx & c2 e x]
U Spec, 19
52 (t,u) e fxx <=> t e fx & u e x
U Spec, 51
53 [(t,u) e fxx => t e fx & u e x]
&
[t e fx & u e x => (t,u) e fxx]
Iff-And, 52
54 (t,u) e fxx => t e fx & u e x
Split, 53
55 t e fx & u e x
Detach, 54, 50
Part 1
56 ALL(a1):ALL(b):[(a1,b) e graf' => a1 e fx & b e x]
4 Conclusion, 44
Prove: ALL(a1):[a1 e fx => EXIST(b):[b e x & (a1,b) e graf']]
Suppose...
57 t e fx
Premise
58 t e fx <=> t e y & EXIST(b):[b e x & f(b)=t]
U Spec, 11
59 [t e fx => t e y & EXIST(b):[b e x & f(b)=t]]
&
[t e y & EXIST(b):[b e x & f(b)=t] => t e fx]
Iff-And, 58
60 t e fx => t e y & EXIST(b):[b e x & f(b)=t]
Split, 59
61 t e y & EXIST(b):[b e x & f(b)=t]
Detach, 60, 57
62 t e y
Split, 61
63 EXIST(b):[b e x & f(b)=t]
Split, 61
64 u e x & f(u)=t
E Spec, 63
65 u e x
Split, 64
66 f(u)=t
Split, 64
67 ALL(b):[(t,b) e graf' <=> (t,b) e fxx & t=f(b)]
U Spec, 23
68 (t,u) e graf' <=> (t,u) e fxx & t=f(u)
U Spec, 67
69 [(t,u) e graf' => (t,u) e fxx & t=f(u)]
&
[(t,u) e fxx & t=f(u) => (t,u) e graf']
Iff-And, 68
70 (t,u) e fxx & t=f(u) => (t,u) e graf'
Split, 69
71 ALL(c2):[(t,c2) e fxx <=> t e fx & c2 e x]
U Spec, 19
72 (t,u) e fxx <=> t e fx & u e x
U Spec, 71
73 [(t,u) e fxx => t e fx & u e x]
&
[t e fx & u e x => (t,u) e fxx]
Iff-And, 72
74 t e fx & u e x => (t,u) e fxx
Split, 73
75 t e fx & u e x
Join, 57, 65
76 (t,u) e fxx
Detach, 74, 75
77 t=f(u)
Sym, 66
78 (t,u) e fxx & t=f(u)
Join, 76, 77
79 (t,u) e graf'
Detach, 70, 78
80 u e x & (t,u) e graf'
Join, 65, 79
Part 2
81 ALL(a1):[a1 e fx => EXIST(b):[b e x & (a1,b) e graf']]
4 Conclusion, 57
Prove: ALL(a1):ALL(b1):ALL(b2):[a1 e fx & b1 e x & b2 e x
=> [(a1,b1) e graf' &
(a1,b2) e graf' => b1=b2]]
Suppose...
82 t e fx & u1 e x & u2 e x
Premise
83 t e fx
Split, 82
84 u1 e x
Split, 82
85 u2 e x
Split, 82
Prove: (t,u1) e graf' & (t,u2) e graf' => u1=u2
Suppose...
86 (t,u1) e graf' & (t,u2) e graf'
Premise
87 (t,u1) e graf'
Split, 86
88 (t,u2) e graf'
Split, 86
89 ALL(b):[(t,b) e graf' <=> (t,b) e fxx & t=f(b)]
U Spec, 23
90 (t,u1) e graf' <=> (t,u1) e fxx & t=f(u1)
U Spec, 89
91 [(t,u1) e graf' => (t,u1) e fxx & t=f(u1)]
&
[(t,u1) e fxx & t=f(u1) => (t,u1) e graf']
Iff-And, 90
92 (t,u1) e graf' => (t,u1) e fxx & t=f(u1)
Split, 91
93 (t,u1) e fxx & t=f(u1)
Detach, 92, 87
94 t=f(u1)
Split, 93
95 (t,u2) e graf' <=> (t,u2) e fxx & t=f(u2)
U Spec, 89
96 [(t,u2) e graf' => (t,u2) e fxx & t=f(u2)]
&
[(t,u2) e fxx & t=f(u2) => (t,u2) e graf']
Iff-And, 95
97 (t,u2) e graf' => (t,u2) e fxx & t=f(u2)
Split, 96
98 (t,u2) e fxx & t=f(u2)
Detach, 97, 88
99 t=f(u2)
Split, 98
100 f(u1)=f(u2)
Substitute, 94,
99
101 ALL(d):[u1 e x & d e x => [f(u1)=f(d) => u1=d]]
U Spec, 6
102 u1 e x & u2 e x => [f(u1)=f(u2) => u1=u2]
U Spec, 101
103 u1 e x & u2 e x
Join, 84, 85
104 f(u1)=f(u2) => u1=u2
Detach, 102, 103
105 u1=u2
Detach, 104, 100
As Required:
106 (t,u1) e graf' & (t,u2) e graf' => u1=u2
4 Conclusion, 86
Part 3
107 ALL(a1):ALL(b1):ALL(b2):[a1 e fx & b1 e x & b2 e x
=>
[(a1,b1) e graf' & (a1,b2) e graf' => b1=b2]]
4 Conclusion, 82
108 ALL(a1):ALL(b):[(a1,b) e graf' => a1 e fx & b e x]
&
ALL(a1):[a1 e fx => EXIST(b):[b e x & (a1,b) e graf']]
Join, 56, 81
109 ALL(a1):ALL(b):[(a1,b) e graf' => a1 e fx & b e x]
&
ALL(a1):[a1 e fx => EXIST(b):[b e x & (a1,b) e graf']]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e fx & b1 e x & b2 e x
=>
[(a1,b1) e graf' & (a1,b2) e graf' => b1=b2]]
Join, 108, 107
110 EXIST(fun):ALL(a1):ALL(b):[a1 e fx & b e x
=>
[fun(a1)=b <=> (a1,b) e graf']]
Detach, 43, 109
Define: Function f' in terms of its graph
111 ALL(a1):ALL(b):[a1 e fx & b e x
=>
[f'(a1)=b <=> (a1,b) e graf']]
E Spec, 110
Prove: ALL(a):[a e fx => f'(a) e x]
Suppose...
112 t e fx
Premise
113 t e fx => EXIST(b):[b e x & (t,b) e graf']
U Spec, 81
114 EXIST(b):[b e x & (t,b) e graf']
Detach, 113, 112
115 u e x & (t,u) e graf'
E Spec, 114
116 u e x
Split, 115
117 (t,u) e graf'
Split, 115
118 ALL(b):[t e fx & b e x
=>
[f'(t)=b <=> (t,b) e graf']]
U Spec, 111
119 t e fx & u e x
=>
[f'(t)=u <=> (t,u) e graf']
U Spec, 118
120 t e fx & u e x
Join, 112, 116
121 f'(t)=u <=> (t,u) e graf'
Detach, 119, 120
122 [f'(t)=u => (t,u) e graf'] & [(t,u) e graf' => f'(t)=u]
Iff-And, 121
123 f'(t)=u => (t,u) e graf'
Split, 122
124 (t,u) e graf' => f'(t)=u
Split, 122
125 f'(t)=u
Detach, 124, 117
126 f'(t) e x
Substitute, 125,
116
As Required:
127 ALL(a):[a e fx => f'(a) e x]
4 Conclusion, 112
Prove: ALL(a):[a e fx => a=f(f'(a))]
Suppose...
128 t e fx
Premise
129 t e fx => EXIST(b):[b e x & (t,b) e graf']
U Spec, 81
130 EXIST(b):[b e x & (t,b) e graf']
Detach, 129, 128
131 u e x & (t,u) e graf'
E Spec, 130
132 u e x
Split, 131
133 (t,u) e graf'
Split, 131
134 ALL(b):[(t,b) e graf' <=> (t,b) e fxx & t=f(b)]
U Spec, 23
135 (t,u) e graf' <=> (t,u) e fxx & t=f(u)
U Spec, 134
136 [(t,u) e graf' => (t,u) e fxx & t=f(u)]
&
[(t,u) e fxx & t=f(u) => (t,u) e graf']
Iff-And, 135
137 (t,u) e graf' => (t,u) e fxx & t=f(u)
Split, 136
138 (t,u) e fxx & t=f(u)
Detach, 137, 133
139 t=f(u)
Split, 138
140 ALL(b):[t e fx & b e x
=>
[f'(t)=b <=> (t,b) e graf']]
U Spec, 111
141 t e fx & u e x
=>
[f'(t)=u <=> (t,u) e graf']
U Spec, 140
142 t e fx & u e x
Join, 128, 132
143 f'(t)=u <=> (t,u) e graf'
Detach, 141, 142
144 [f'(t)=u => (t,u) e graf'] & [(t,u) e graf' => f'(t)=u]
Iff-And, 143
145 (t,u) e graf' => f'(t)=u
Split, 144
146 f'(t)=u
Detach, 145, 133
147 t=f(f'(t))
Substitute, 146,
139
As Required:
148 ALL(a):[a e fx => a=f(f'(a))]
4 Conclusion, 128
Construct surjective g: y --> x
Apply Cartesian Product Axiom
149 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
150 ALL(a2):[Set(y) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e y & c2 e a2]]]
U Spec, 149
151 Set(y) & Set(x) => EXIST(b):[Set'(b) &
ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e y & c2 e x]]
U Spec, 150
152 Set(y) & Set(x)
Join, 4, 2
153 EXIST(b):[Set'(b) &
ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e y & c2 e x]]
Detach, 151, 152
154 Set'(yx) & ALL(c1):ALL(c2):[(c1,c2) e yx <=> c1 e y & c2 e x]
E Spec, 153
Define: yx (Cartesian product
of y and x)
155 Set'(yx)
Split, 154
156 ALL(c1):ALL(c2):[(c1,c2) e yx <=> c1 e y & c2 e x]
Split, 154
157 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e yx & [a e fx & b=f'(a) | ~a e fx & b=x0]]]
Subset, 155
158 Set'(grag) & ALL(a):ALL(b):[(a,b) e grag <=> (a,b) e yx & [a e fx & b=f'(a) | ~a e fx & b=x0]]
E Spec, 157
Define: grag (graph set of
function g)
159 Set'(grag)
Split, 158
160 ALL(a):ALL(b):[(a,b) e grag <=> (a,b) e yx & [a e fx & b=f'(a) | ~a e fx & b=x0]]
Split, 158
Establish sufficient conditions for functionality of grag
Apply Function Axiom
161 ALL(dom):ALL(cod):ALL(gra):[Set(dom) & Set(cod)
& Set'(gra)
&
EXIST(a1):a1 e dom & EXIST(a1):a1 e cod
=>
[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
162 ALL(cod):ALL(gra):[Set(y) & Set(cod)
& Set'(gra)
&
EXIST(a1):a1 e y &
EXIST(a1):a1 e cod
=>
[ALL(a1):ALL(b):[(a1,b) e gra => a1 e y & b e cod]
&
ALL(a1):[a1 e y =>
EXIST(b):[b e cod & (a1,b) e gra]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e y & b1 e cod & b2 e cod
=>
[(a1,b1) e gra & (a1,b2) e gra => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e y & b e cod
=>
[fun(a1)=b <=> (a1,b) e gra]]]]
U Spec, 161
163 ALL(gra):[Set(y) & Set(x) & Set'(gra)
&
EXIST(a1):a1 e y &
EXIST(a1):a1 e x
=>
[ALL(a1):ALL(b):[(a1,b) e gra => a1 e y & b e x]
&
ALL(a1):[a1 e y =>
EXIST(b):[b e x & (a1,b) e gra]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e y & b1 e x & b2 e x
=>
[(a1,b1) e gra & (a1,b2) e gra => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e y & b e x
=>
[fun(a1)=b <=> (a1,b) e gra]]]]
U Spec, 162
164 Set(y) & Set(x) & Set'(grag)
&
EXIST(a1):a1 e y &
EXIST(a1):a1 e x
=>
[ALL(a1):ALL(b):[(a1,b) e grag => a1 e y & b e x]
&
ALL(a1):[a1 e y =>
EXIST(b):[b e x & (a1,b) e grag]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e y & b1 e x & b2 e x
=>
[(a1,b1) e grag & (a1,b2) e grag => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e y & b e x
=>
[fun(a1)=b <=> (a1,b) e grag]]]
U Spec, 163
165 x0 e x => f(x0) e y
U Spec, 5
166 f(x0) e y
Detach, 165, 7
167 EXIST(a1):a1 e y
E Gen, 166
168 Set(y) & Set(x)
Join, 4, 2
169 Set(y) & Set(x) & Set'(grag)
Join, 168, 159
170 Set(y) & Set(x) & Set'(grag) & EXIST(a1):a1 e y
Join, 169, 167
171 Set(y) & Set(x) & Set'(grag) & EXIST(a1):a1 e y
&
EXIST(c):c e x
Join, 170, 3
Sufficient: For functionality of grag
172 ALL(a1):ALL(b):[(a1,b) e grag => a1 e y & b e x]
&
ALL(a1):[a1 e y =>
EXIST(b):[b e x & (a1,b) e grag]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e y & b1 e x & b2 e x
=>
[(a1,b1) e grag & (a1,b2) e grag => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e y & b e x
=>
[fun(a1)=b <=> (a1,b) e grag]]
Detach, 164, 171
Prove: ALL(a1):ALL(b):[(a1,b) e grag => a1 e y & b e x]
Suppose...
173 (t,u) e grag
Premise
174 ALL(b):[(t,b) e grag <=> (t,b) e yx & [t e fx & b=f'(t) | ~t e fx & b=x0]]
U Spec, 160
175 (t,u) e grag <=> (t,u) e yx & [t e fx & u=f'(t) | ~t e fx & u=x0]
U Spec, 174
176 [(t,u) e grag => (t,u) e yx & [t e fx & u=f'(t) | ~t e fx & u=x0]]
&
[(t,u) e yx & [t e fx & u=f'(t) | ~t e fx & u=x0] => (t,u) e grag]
Iff-And, 175
177 (t,u) e grag => (t,u) e yx & [t e fx & u=f'(t) | ~t e fx & u=x0]
Split, 176
178 (t,u) e yx & [t e fx & u=f'(t) | ~t e fx & u=x0]
Detach, 177, 173
179 (t,u) e yx
Split, 178
180 ALL(c2):[(t,c2) e yx <=> t e y & c2 e x]
U Spec, 156
181 (t,u) e yx <=> t e y & u e x
U Spec, 180
182 [(t,u) e yx => t e y & u e x]
&
[t e y & u e x => (t,u) e yx]
Iff-And, 181
183 (t,u) e yx => t e y & u e x
Split, 182
184 t e y & u e x => (t,u) e yx
Split, 182
185 t e y & u e x
Detach, 183, 179
Part 1
186 ALL(a1):ALL(b):[(a1,b) e grag => a1 e y & b e x]
4 Conclusion, 173
Prove: ALL(a1):[a1 e y => EXIST(b):[b e x &
(a1,b) e grag]]
Suppose...
187 t e y
Premise
Two Cases:
188 t e fx | ~t e fx
Or Not
Case 1
Prove: t e fx => EXIST(b):[b e x & (t,b) e grag]
Suppose...
189 t e fx
Premise
190 t e fx <=> t e y & EXIST(b):[b e x & f(b)=t]
U Spec, 11
191 [t e fx => t e y & EXIST(b):[b e x & f(b)=t]]
&
[t e y & EXIST(b):[b e x & f(b)=t] => t e fx]
Iff-And, 190
192 t e fx => t e y & EXIST(b):[b e x & f(b)=t]
Split, 191
193 t e y & EXIST(b):[b e x & f(b)=t]
Detach, 192, 189
194 t e y
Split, 193
195 EXIST(b):[b e x & f(b)=t]
Split, 193
196 u e x & f(u)=t
E Spec, 195
197 u e x
Split, 196
198 f(u)=t
Split, 196
199 ALL(b):[(t,b) e grag <=> (t,b) e yx & [t e fx & b=f'(t) | ~t e fx & b=x0]]
U Spec, 160
200 (t,u) e grag <=> (t,u) e yx & [t e fx & u=f'(t) | ~t e fx & u=x0]
U Spec, 199
201 [(t,u) e grag => (t,u) e yx & [t e fx & u=f'(t) | ~t e fx & u=x0]]
&
[(t,u) e yx & [t e fx & u=f'(t) | ~t e fx & u=x0] => (t,u) e grag]
Iff-And, 200
Sufficient: For (t,u)
e grag
202 (t,u) e yx & [t e fx & u=f'(t) | ~t e fx & u=x0] => (t,u) e grag
Split, 201
203 ALL(c2):[(t,c2) e yx <=> t e y & c2 e x]
U Spec, 156
204 (t,u) e yx <=> t e y & u e x
U Spec, 203
205 [(t,u) e yx => t e y & u e x]
&
[t e y & u e x => (t,u) e yx]
Iff-And, 204
206 t e y & u e x => (t,u) e yx
Split, 205
207 t e y & u e x
Join, 187, 197
208 (t,u) e yx
Detach, 206, 207
209 t e fx => t=f(f'(t))
U Spec, 148
210 t=f(f'(t))
Detach, 209, 189
211 f(u)=f(f'(t))
Substitute, 198,
210
212 t e fx => f'(t) e x
U Spec, 127
213 f'(t) e x
Detach, 212, 189
214 ALL(d):[u e x & d e x => [f(u)=f(d) => u=d]]
U Spec, 6
215 u e x & f'(t) e x => [f(u)=f(f'(t)) => u=f'(t)]
U Spec, 214, 213
216 u e x & f'(t) e x
Join, 197, 213
217 f(u)=f(f'(t)) => u=f'(t)
Detach, 215, 216
218 u=f'(t)
Detach, 217, 211
219 t e fx & u=f'(t)
Join, 189, 218
220 t e fx & u=f'(t) | ~t e fx & u=x0
Arb Or, 219
221 (t,u) e yx & [t e fx & u=f'(t) | ~t e fx & u=x0]
Join, 208, 220
222 (t,u) e grag
Detach, 202, 221
223 u e x & (t,u) e grag
Join, 197, 222
Case 1
As Required:
224 t e fx => EXIST(b):[b e x & (t,b) e grag]
4 Conclusion, 189
Case 2
Prove: ~t e fx => EXIST(b):[b e x & (t,b) e grag]
Suppose...
225 ~t e fx
Premise
226 ALL(b):[(t,b) e grag <=> (t,b) e yx & [t e fx & b=f'(t) | ~t e fx & b=x0]]
U Spec, 160
227 (t,x0) e grag <=> (t,x0) e yx & [t e fx & x0=f'(t) | ~t e fx & x0=x0]
U Spec, 226
228 [(t,x0) e grag => (t,x0) e yx & [t e fx & x0=f'(t) | ~t e fx & x0=x0]]
&
[(t,x0) e yx & [t e fx & x0=f'(t) | ~t e fx & x0=x0] => (t,x0) e grag]
Iff-And, 227
229 (t,x0) e yx & [t e fx & x0=f'(t) | ~t e fx & x0=x0] => (t,x0) e grag
Split, 228
230 ALL(c2):[(t,c2) e yx <=> t e y & c2 e x]
U Spec, 156
231 (t,x0) e yx <=> t e y & x0 e x
U Spec, 230
232 [(t,x0) e yx => t e y & x0 e x]
&
[t e y & x0 e x => (t,x0) e yx]
Iff-And, 231
233 (t,x0) e yx => t e y & x0 e x
Split, 232
234 t e y & x0 e x => (t,x0) e yx
Split, 232
235 t e y & x0 e x
Join, 187, 7
236 (t,x0) e yx
Detach, 234, 235
237 (t,x0) e yx & [t e fx & x0=f'(t) | ~t e fx & x0=x0] => (t,x0) e grag
Split, 228
238 x0=x0
Reflex
239 ~t e fx & x0=x0
Join, 225, 238
240 t e fx & x0=f'(t) | ~t e fx & x0=x0
Arb Or, 239
241 (t,x0) e yx & [t e fx & x0=f'(t) | ~t e fx & x0=x0]
Join, 236, 240
242 (t,x0) e grag
Detach, 229, 241
243 x0 e x & (t,x0) e grag
Join, 7, 242
244 EXIST(b):[b e x & (t,b) e grag]
E Gen, 243
Case 2
As Required:
245 ~t e fx => EXIST(b):[b e x & (t,b) e grag]
4 Conclusion, 225
246 [t e fx => EXIST(b):[b e x & (t,b) e grag]]
&
[~t e fx => EXIST(b):[b e x & (t,b) e grag]]
Join, 224, 245
247 EXIST(b):[b e x & (t,b) e grag]
Cases, 188, 246
Part 2
248 ALL(a1):[a1 e y =>
EXIST(b):[b e x & (a1,b) e grag]]
4 Conclusion, 187
Prove: ALL(a1):ALL(b1):ALL(b2):[a1 e y & b1 e x & b2 e x
=> [(a1,b1) e grag &
(a1,b2) e grag => b1=b2]]
Suppose...
249 t e y & u1 e x & u2 e x
Premise
250 t e y
Split, 249
251 u1 e x
Split, 249
252 u2 e x
Split, 249
Prove: (t,u1) e grag & (t,u2) e grag => u1=u2
Suppose...
253 (t,u1) e grag & (t,u2) e grag
Premise
254 (t,u1) e grag
Split, 253
255 (t,u2) e grag
Split, 253
256 ALL(b):[(t,b) e grag <=> (t,b) e yx & [t e fx & b=f'(t) | ~t e fx & b=x0]]
U Spec, 160
257 (t,u1) e grag <=> (t,u1) e yx & [t e fx & u1=f'(t) | ~t e fx & u1=x0]
U Spec, 256
258 [(t,u1) e grag => (t,u1) e yx & [t e fx & u1=f'(t) | ~t e fx & u1=x0]]
&
[(t,u1) e yx & [t e fx & u1=f'(t) | ~t e fx & u1=x0] => (t,u1) e grag]
Iff-And, 257
259 (t,u1) e grag => (t,u1) e yx & [t e fx & u1=f'(t) | ~t e fx & u1=x0]
Split, 258
260 (t,u1) e yx & [t e fx & u1=f'(t) | ~t e fx & u1=x0]
Detach, 259, 254
261 t e fx & u1=f'(t) | ~t e fx & u1=x0
Split, 260
262 (t,u2) e grag <=> (t,u2) e yx & [t e fx & u2=f'(t) | ~t e fx & u2=x0]
U Spec, 256
263 [(t,u2) e grag => (t,u2) e yx & [t e fx & u2=f'(t) | ~t e fx & u2=x0]]
&
[(t,u2) e yx & [t e fx & u2=f'(t) | ~t e fx & u2=x0] => (t,u2) e grag]
Iff-And, 262
264 (t,u2) e grag => (t,u2) e yx & [t e fx & u2=f'(t) | ~t e fx & u2=x0]
Split, 263
265 (t,u2) e yx & [t e fx & u2=f'(t) | ~t e fx & u2=x0]
Detach, 264, 255
266 t e fx & u2=f'(t) | ~t e fx & u2=x0
Split, 265
Two cases:
267 t e fx | ~t e fx
Or Not
Case 1
Prove: t e fx => u1=u2
Suppose...
268 t e fx
Premise
269 ~[t e fx & u1=f'(t)] => ~t e fx & u1=x0
Imply-Or, 261
270 ~[~t e fx & u1=x0] => ~~[t e fx & u1=f'(t)]
Contra, 269
271 ~[~t e fx & u1=x0] => t e fx & u1=f'(t)
Rem DNeg, 270
272 ~~[~~t e fx | ~u1=x0] => t e fx & u1=f'(t)
DeMorgan, 271
273 ~~t e fx | ~u1=x0 => t e fx & u1=f'(t)
Rem DNeg, 272
274 t e fx | ~u1=x0 => t e fx & u1=f'(t)
Rem DNeg, 273
275 t e fx | ~u1=x0
Arb Or, 268
276 t e fx & u1=f'(t)
Detach, 274, 275
277 t e fx
Split, 276
278 u1=f'(t)
Split, 276
279 ~[t e fx & u2=f'(t)] => ~t e fx & u2=x0
Imply-Or, 266
280 ~[~t e fx & u2=x0] => ~~[t e fx & u2=f'(t)]
Contra, 279
281 ~[~t e fx & u2=x0] => t e fx & u2=f'(t)
Rem DNeg, 280
282 ~~[~~t e fx | ~u2=x0] => t e fx & u2=f'(t)
DeMorgan, 281
283 ~~t e fx | ~u2=x0 => t e fx & u2=f'(t)
Rem DNeg, 282
284 t e fx | ~u2=x0 => t e fx & u2=f'(t)
Rem DNeg, 283
285 t e fx | ~u2=x0
Arb Or, 268
286 t e fx & u2=f'(t)
Detach, 284, 285
287 u2=f'(t)
Split, 286
288 u1=u2
Substitute, 287,
278
Case 1
As Required:
289 t e fx => u1=u2
4 Conclusion, 268
Case 2
Prove: ~t e fx => u1=u2
Suppose...
290 ~t e fx
Premise
291 ~[t e fx & u1=f'(t)] => ~t e fx & u1=x0
Imply-Or, 261
292 ~~[~t e fx | ~u1=f'(t)] => ~t e fx & u1=x0
DeMorgan, 291
293 ~t e fx | ~u1=f'(t) => ~t e fx & u1=x0
Rem DNeg, 292
294 ~t e fx | ~u1=f'(t)
Arb Or, 290
295 ~t e fx & u1=x0
Detach, 293, 294
296 ~t e fx
Split, 295
297 u1=x0
Split, 295
298 ~[t e fx & u2=f'(t)] => ~t e fx & u2=x0
Imply-Or, 266
299 ~~[~t e fx | ~u2=f'(t)] => ~t e fx & u2=x0
DeMorgan, 298
300 ~t e fx | ~u2=f'(t) => ~t e fx & u2=x0
Rem DNeg, 299
301 ~t e fx | ~u2=f'(t)
Arb Or, 290
302 ~t e fx & u2=x0
Detach, 300, 301
303 u2=x0
Split, 302
304 u1=u2
Substitute, 303,
297
Case 2
As Required:
305 ~t e fx => u1=u2
4 Conclusion, 290
306 [t e fx => u1=u2] & [~t e fx => u1=u2]
Join, 289, 305
307 u1=u2
Cases, 267, 306
As Required:
308 (t,u1) e grag & (t,u2) e grag => u1=u2
4 Conclusion, 253
Part 3
309 ALL(a1):ALL(b1):ALL(b2):[a1 e y & b1 e x & b2 e x
=>
[(a1,b1) e grag & (a1,b2) e grag => b1=b2]]
4 Conclusion, 249
310 ALL(a1):ALL(b):[(a1,b) e grag => a1 e y & b e x]
&
ALL(a1):[a1 e y =>
EXIST(b):[b e x & (a1,b) e grag]]
Join, 186, 248
311 ALL(a1):ALL(b):[(a1,b) e grag => a1 e y & b e x]
&
ALL(a1):[a1 e y =>
EXIST(b):[b e x & (a1,b) e grag]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e y & b1 e x & b2 e x
=>
[(a1,b1) e grag & (a1,b2) e grag => b1=b2]]
Join, 310, 309
312 EXIST(fun):ALL(a1):ALL(b):[a1 e y & b e x
=>
[fun(a1)=b <=> (a1,b) e grag]]
Detach, 172, 311
Define: Function g in terms of its graph set
313 ALL(a1):ALL(b):[a1 e y & b e x
=>
[g(a1)=b <=> (a1,b) e grag]]
E Spec, 312
Prove: ALL(a):[a e y => g(a) e x]
Suppose...
314 t e y
Premise
315 t e y => EXIST(b):[b e x & (t,b) e grag]
U Spec, 248
316 EXIST(b):[b e x & (t,b) e grag]
Detach, 315, 314
317 u e x & (t,u) e grag
E Spec, 316
318 u e x
Split, 317
319 (t,u) e grag
Split, 317
320 ALL(b):[t e y & b e x
=>
[g(t)=b <=> (t,b) e grag]]
U Spec, 313
321 t e y & u e x
=>
[g(t)=u <=> (t,u) e grag]
U Spec, 320
322 t e y & u e x
Join, 314, 318
323 g(t)=u <=> (t,u) e grag
Detach, 321, 322
324 [g(t)=u => (t,u) e grag] & [(t,u) e grag => g(t)=u]
Iff-And, 323
325 (t,u) e grag => g(t)=u
Split, 324
326 g(t)=u
Detach, 325, 319
327 g(t) e x
Substitute, 326,
318
As Required:
328 ALL(a):[a e y => g(a) e x]
4 Conclusion, 314
Prove: ALL(a):[a e y
=> [a e fx => g(a)=f'(a)]
& [~a e fx => g(a)=x0]]
Suppose...
329 t e y
Premise
330 t e y => EXIST(b):[b e x & (t,b) e grag]
U Spec, 248
331 EXIST(b):[b e x & (t,b) e grag]
Detach, 330, 329
332 u e x & (t,u) e grag
E Spec, 331
333 u e x
Split, 332
334 (t,u) e grag
Split, 332
335 ALL(b):[t e y & b e x
=>
[g(t)=b <=> (t,b) e grag]]
U Spec, 313
336 t e y & u e x
=>
[g(t)=u <=> (t,u) e grag]
U Spec, 335
337 t e y & u e x
Join, 329, 333
338 g(t)=u <=> (t,u) e grag
Detach, 336, 337
339 [g(t)=u => (t,u) e grag] & [(t,u) e grag => g(t)=u]
Iff-And, 338
340 (t,u) e grag => g(t)=u
Split, 339
341 g(t)=u
Detach, 340, 334
342 ALL(b):[(t,b) e grag <=> (t,b) e yx & [t e fx & b=f'(t) | ~t e fx & b=x0]]
U Spec, 160
343 (t,u) e grag <=> (t,u) e yx & [t e fx & u=f'(t) | ~t e fx & u=x0]
U Spec, 342
344 [(t,u) e grag => (t,u) e yx & [t e fx & u=f'(t) | ~t e fx & u=x0]]
&
[(t,u) e yx & [t e fx & u=f'(t) | ~t e fx & u=x0] => (t,u) e grag]
Iff-And, 343
345 (t,u) e grag => (t,u) e yx & [t e fx & u=f'(t) | ~t e fx & u=x0]
Split, 344
346 (t,u) e yx & [t e fx & u=f'(t) | ~t e fx & u=x0]
Detach, 345, 334
347 (t,u) e yx
Split, 346
348 t e fx & u=f'(t) | ~t e fx & u=x0
Split, 346
349 t e fx & g(t)=f'(t) | ~t e fx & g(t)=x0
Substitute, 341,
348
Prove: t e fx => g(t)=f'(t)
Suppose...
350 t e fx
Premise
351 ~[t e fx & g(t)=f'(t)] => ~t e fx & g(t)=x0
Imply-Or, 349
352 ~[~t e fx & g(t)=x0] => ~~[t e fx & g(t)=f'(t)]
Contra, 351
353 ~[~t e fx & g(t)=x0] => t e fx & g(t)=f'(t)
Rem DNeg, 352
354 ~~[~~t e fx | ~g(t)=x0] => t e fx & g(t)=f'(t)
DeMorgan, 353
355 ~~t e fx | ~g(t)=x0 => t e fx & g(t)=f'(t)
Rem DNeg, 354
356 t e fx | ~g(t)=x0 => t e fx & g(t)=f'(t)
Rem DNeg, 355
357 t e fx | ~g(t)=x0
Arb Or, 350
358 t e fx & g(t)=f'(t)
Detach, 356, 357
359 g(t)=f'(t)
Split, 358
As Required:
360 t e fx => g(t)=f'(t)
4 Conclusion, 350
Prove: ~t e fx => g(t)=x0
Suppose...
361 ~t e fx
Premise
362 ~[t e fx & g(t)=f'(t)] => ~t e fx & g(t)=x0
Imply-Or, 349
363 ~~[~t e fx | ~g(t)=f'(t)] => ~t e fx & g(t)=x0
DeMorgan, 362
364 ~t e fx | ~g(t)=f'(t) => ~t e fx & g(t)=x0
Rem DNeg, 363
365 ~t e fx | ~g(t)=f'(t)
Arb Or, 361
366 ~t e fx & g(t)=x0
Detach, 364, 365
367 g(t)=x0
Split, 366
As Required:
368 ~t e fx => g(t)=x0
4 Conclusion, 361
369 [t e fx => g(t)=f'(t)] & [~t e fx => g(t)=x0]
Join, 360, 368
As Required:
370 ALL(a):[a e y
=>
[a e fx => g(a)=f'(a)] & [~a e fx => g(a)=x0]]
4 Conclusion, 329
Prove: ALL(c):[c e x => EXIST(d):[d e y & g(d) e x]]
Suppose...
371 t e x
Premise
372 t e x => f(t) e y
U Spec, 5
373 f(t) e y
Detach, 372, 371
374 f(t) e y => g(f(t)) e x
U Spec, 328, 373
375 g(f(t)) e x
Detach, 374, 373
376 f(t) e y & g(f(t)) e x
Join, 373, 375
377 EXIST(d):[d e y & g(d) e x]
E Gen, 376
As Required:
378 ALL(c):[c e x =>
EXIST(d):[d e y & g(d) e x]]
4 Conclusion, 371
379 ALL(c):[c e y => g(c) e x]
Rename, 328
380 ALL(c):[c e y => g(c) e x]
&
ALL(c):[c e x =>
EXIST(d):[d e y & g(d) e x]]
Join, 379, 378
As Required:
381 ALL(a):ALL(b):ALL(f1):[Set(a) &
EXIST(c):c e a & Set(b)
&
ALL(c):[c e a => f1(c) e b]
&
ALL(c):ALL(d):[c e a & d e a => [f1(c)=f1(d) => c=d]]
=>
EXIST(f2):[ALL(c):[c e b => f2(c) e a]
&
ALL(c):[c e a =>
EXIST(d):[d e b & f2(d) e a]]]]
4 Conclusion, 1