LEMMA 4
*******
Suppose we have injective f: x --> y for non-empty x.
Then there exists surjective g: y --> x.
(This proof was written with the aid of the author's DC Proof 2.0 software available at http://www.dcproof.com )
OUTLINE
*******
Suppose an injective (one-to-one) function f maps of non-empty set x to set y. Let x0 e x.
Construct imgf, the image of set x under f. Using f, construct bijection f' mapping set x to imgf.
Construct function g' that is the inverse of f'. Finally, construct the required surjection g:
g: y --> x such that
g(a) = g'(a) if a e imgf
= x0 otherwise
DEFINITIONS
***********
Define: Injection
1 ALL(f):ALL(a):ALL(b):[Injection(f,a,b) <=> ALL(c):ALL(d):[c e a & d e a => [f(c)=f(d) => c=d]]]
Axiom
Define: Surjection
2 ALL(f):ALL(a):ALL(b):[Surjection(f,a,b) <=> ALL(c):[c e b => EXIST(d):[d e a & f(d)=c]]]
Axiom
Define: Bijection
3 ALL(f):ALL(a):ALL(b):[Bijection(f,a,b) <=> Injection(f,a,b) & Surjection(f,a,b)]
Axiom
PREVIOUS RESULTS (with links to proofs)
****************
Lemma 2: Proof
Suppose an injective (one-to-one) function maps set x to set y.
Then there exists bijective function g mapping set x to the image of x under f.
4 ALL(a):ALL(b):ALL(f):[Set(a)
& Set(b)
& ALL(c):[c e a => f(c) e b]
& Injection(f,a,b)
=> EXIST(c):EXIST(g):[Set(c)
& ALL(d):[d e c <=> d e b & EXIST(e):[e e a & f(e)=d]]
& ALL(d):[d e a => g(d) e c]
& ALL(d):[d e a => g(d)=f(d)]
& Bijection(g,a,c)]]
Axiom
Lemma 1: Proof
Bijections are symmetric. Every bijection has an inverse.
5 ALL(a):ALL(b):ALL(f1):[Set(a) & Set(b) & ALL(c):[c e a => f1(c) e b]
=> [Bijection(f1,a,b)
=> EXIST(f2):[ALL(c):[c e b => f2(c) e a]
& ALL(c):ALL(d):[c e a & d e b => [f2(d)=c <=> f1(c)=d]]
& Bijection(f2,b,a)]]]
Axiom
PROOF OF LEMMA 4
****************
Suppose injective (one-to-one) function f maps non-empty set x to set y
6 Set(x)
& Set(y)
& EXIST(c):c e x
& ALL(c):[c e x => f(c) e y]
& Injection(f,x,y)
Premise
7 Set(x)
Split, 6
8 Set(y)
Split, 6
9 EXIST(c):c e x
Split, 6
Define: f
10 ALL(c):[c e x => f(c) e y]
Split, 6
11 Injection(f,x,y)
Split, 6
Define: x0
12 x0 e x
E Spec, 9
Prove: There exists bijective function f' mapping x to the image of x under f.
Apply previous result
13 ALL(b):ALL(f):[Set(x)
& Set(b)
& ALL(c):[c e x => f(c) e b]
& Injection(f,x,b)
=> EXIST(c):EXIST(g):[Set(c)
& ALL(d):[d e c <=> d e b & EXIST(e):[e e x & f(e)=d]]
& ALL(d):[d e x => g(d) e c]
& ALL(d):[d e x => g(d)=f(d)]
& Bijection(g,x,c)]]
U Spec, 4
14 ALL(f):[Set(x)
& Set(y)
& ALL(c):[c e x => f(c) e y]
& Injection(f,x,y)
=> EXIST(c):EXIST(g):[Set(c)
& ALL(d):[d e c <=> d e y & EXIST(e):[e e x & f(e)=d]]
& ALL(d):[d e x => g(d) e c]
& ALL(d):[d e x => g(d)=f(d)]
& Bijection(g,x,c)]]
U Spec, 13
15 Set(x)
& Set(y)
& ALL(c):[c e x => f(c) e y]
& Injection(f,x,y)
=> EXIST(c):EXIST(g):[Set(c)
& ALL(d):[d e c <=> d e y & EXIST(e):[e e x & f(e)=d]]
& ALL(d):[d e x => g(d) e c]
& ALL(d):[d e x => g(d)=f(d)]
& Bijection(g,x,c)]
U Spec, 14
16 Set(x) & Set(y)
Join, 7, 8
17 Set(x) & Set(y) & ALL(c):[c e x => f(c) e y]
Join, 16, 10
18 Set(x) & Set(y) & ALL(c):[c e x => f(c) e y]
& Injection(f,x,y)
Join, 17, 11
19 EXIST(c):EXIST(g):[Set(c)
& ALL(d):[d e c <=> d e y & EXIST(e):[e e x & f(e)=d]]
& ALL(d):[d e x => g(d) e c]
& ALL(d):[d e x => g(d)=f(d)]
& Bijection(g,x,c)]
Detach, 15, 18
20 EXIST(g):[Set(imgf)
& ALL(d):[d e imgf <=> d e y & EXIST(e):[e e x & f(e)=d]]
& ALL(d):[d e x => g(d) e imgf]
& ALL(d):[d e x => g(d)=f(d)]
& Bijection(g,x,imgf)]
E Spec, 19
As Required:
21 Set(imgf)
& ALL(d):[d e imgf <=> d e y & EXIST(e):[e e x & f(e)=d]]
& ALL(d):[d e x => f'(d) e imgf]
& ALL(d):[d e x => f'(d)=f(d)]
& Bijection(f',x,imgf)
E Spec, 20
Define: imgf (the image of x under f)
22 Set(imgf)
Split, 21
23 ALL(d):[d e imgf <=> d e y & EXIST(e):[e e x & f(e)=d]]
Split, 21
Define: f' (restriction of f to imgf)
24 ALL(d):[d e x => f'(d) e imgf]
Split, 21
25 ALL(d):[d e x => f'(d)=f(d)]
Split, 21
26 Bijection(f',x,imgf)
Split, 21
Prove: There exists an inverse g' of f'
Apply previous result
27 ALL(b):ALL(f1):[Set(x) & Set(b) & ALL(c):[c e x => f1(c) e b]
=> [Bijection(f1,x,b)
=> EXIST(f2):[ALL(c):[c e b => f2(c) e x]
& ALL(c):ALL(d):[c e x & d e b => [f2(d)=c <=> f1(c)=d]]
& Bijection(f2,b,x)]]]
U Spec, 5
28 ALL(f1):[Set(x) & Set(imgf) & ALL(c):[c e x => f1(c) e imgf]
=> [Bijection(f1,x,imgf)
=> EXIST(f2):[ALL(c):[c e imgf => f2(c) e x]
& ALL(c):ALL(d):[c e x & d e imgf => [f2(d)=c <=> f1(c)=d]]
& Bijection(f2,imgf,x)]]]
U Spec, 27
29 Set(x) & Set(imgf) & ALL(c):[c e x => f'(c) e imgf]
=> [Bijection(f',x,imgf)
=> EXIST(f2):[ALL(c):[c e imgf => f2(c) e x]
& ALL(c):ALL(d):[c e x & d e imgf => [f2(d)=c <=> f'(c)=d]]
& Bijection(f2,imgf,x)]]
U Spec, 28
30 Set(x) & Set(imgf)
Join, 7, 22
31 Set(x) & Set(imgf)
& ALL(d):[d e x => f'(d) e imgf]
Join, 30, 24
32 Bijection(f',x,imgf)
=> EXIST(f2):[ALL(c):[c e imgf => f2(c) e x]
& ALL(c):ALL(d):[c e x & d e imgf => [f2(d)=c <=> f'(c)=d]]
& Bijection(f2,imgf,x)]
Detach, 29, 31
33 EXIST(f2):[ALL(c):[c e imgf => f2(c) e x]
& ALL(c):ALL(d):[c e x & d e imgf => [f2(d)=c <=> f'(c)=d]]
& Bijection(f2,imgf,x)]
Detach, 32, 26
As Required:
34 ALL(c):[c e imgf => g'(c) e x]
& ALL(c):ALL(d):[c e x & d e imgf => [g'(d)=c <=> f'(c)=d]]
& Bijection(g',imgf,x)
E Spec, 33
Define: g' (the inverse of f')
35 ALL(c):[c e imgf => g'(c) e x]
Split, 34
36 ALL(c):ALL(d):[c e x & d e imgf => [g'(d)=c <=> f'(c)=d]]
Split, 34
37 Bijection(g',imgf,x)
Split, 34
Construct yx
Apply Cartesian Product Axiom
38 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
39 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, 38
40 Set(y) & Set(x) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e y & c2 e x]]
U Spec, 39
41 Set(y) & Set(x)
Join, 8, 7
42 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e y & c2 e x]]
Detach, 40, 41
43 Set'(yx) & ALL(c1):ALL(c2):[(c1,c2) e yx <=> c1 e y & c2 e x]
E Spec, 42
Define: yx (Cartesian product of y and x)
44 Set'(yx)
Split, 43
45 ALL(c1):ALL(c2):[(c1,c2) e yx <=> c1 e y & c2 e x]
Split, 43
Construct g
Apply Subset Axiom
46 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e yx & [a e imgf & b=g'(a) | ~a e imgf & b=x0]]]
Subset, 44
47 Set'(g) & ALL(a):ALL(b):[(a,b) e g <=> (a,b) e yx & [a e imgf & b=g'(a) | ~a e imgf & b=x0]]
E Spec, 46
Define: g
*********
48 Set'(g)
Split, 47
49 ALL(a):ALL(b):[(a,b) e g <=> (a,b) e yx & [a e imgf & b=g'(a) | ~a e imgf & b=x0]]
Split, 47
Prove: Functionality of g
Apply Function Axiom
50 ALL(f):ALL(a):ALL(b):[ALL(c):ALL(d):[(c,d) e f => c e a & d e b]
& ALL(c):[c e a => EXIST(d):[d e b & (c,d) e f]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e f & (c,d2) e f => d1=d2]
=> ALL(c):ALL(d):[d=f(c) <=> (c,d) e f]]
Function
51 ALL(a):ALL(b):[ALL(c):ALL(d):[(c,d) e g => c e a & d e b]
& ALL(c):[c e a => EXIST(d):[d e b & (c,d) e g]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e g & (c,d2) e g => d1=d2]
=> ALL(c):ALL(d):[d=g(c) <=> (c,d) e g]]
U Spec, 50
52 ALL(b):[ALL(c):ALL(d):[(c,d) e g => c e y & d e b]
& ALL(c):[c e y => EXIST(d):[d e b & (c,d) e g]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e g & (c,d2) e g => d1=d2]
=> ALL(c):ALL(d):[d=g(c) <=> (c,d) e g]]
U Spec, 51
Sufficient: For functionality of g
53 ALL(c):ALL(d):[(c,d) e g => c e y & d e x]
& ALL(c):[c e y => EXIST(d):[d e x & (c,d) e g]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e g & (c,d2) e g => d1=d2]
=> ALL(c):ALL(d):[d=g(c) <=> (c,d) e g]
U Spec, 52
Prove: ALL(c):ALL(d):[(c,d) e g => c e y & d e x]
Suppose...
54 (t,u) e g
Premise
Apply definition of g
55 ALL(b):[(t,b) e g <=> (t,b) e yx & [t e imgf & b=g'(t) | ~t e imgf & b=x0]]
U Spec, 49
56 (t,u) e g <=> (t,u) e yx & [t e imgf & u=g'(t) | ~t e imgf & u=x0]
U Spec, 55
57 [(t,u) e g => (t,u) e yx & [t e imgf & u=g'(t) | ~t e imgf & u=x0]]
& [(t,u) e yx & [t e imgf & u=g'(t) | ~t e imgf & u=x0] => (t,u) e g]
Iff-And, 56
58 (t,u) e g => (t,u) e yx & [t e imgf & u=g'(t) | ~t e imgf & u=x0]
Split, 57
59 (t,u) e yx & [t e imgf & u=g'(t) | ~t e imgf & u=x0] => (t,u) e g
Split, 57
60 (t,u) e yx & [t e imgf & u=g'(t) | ~t e imgf & u=x0]
Detach, 58, 54
61 (t,u) e yx
Split, 60
62 t e imgf & u=g'(t) | ~t e imgf & u=x0
Split, 60
Apply definition of yx
63 ALL(c2):[(t,c2) e yx <=> t e y & c2 e x]
U Spec, 45
64 (t,u) e yx <=> t e y & u e x
U Spec, 63
65 [(t,u) e yx => t e y & u e x]
& [t e y & u e x => (t,u) e yx]
Iff-And, 64
66 (t,u) e yx => t e y & u e x
Split, 65
67 t e y & u e x => (t,u) e yx
Split, 65
68 t e y & u e x
Detach, 66, 61
Functionality, Part 1
69 ALL(c):ALL(d):[(c,d) e g => c e y & d e x]
4 Conclusion, 54
Suppose...
70 u e y
Premise
2 cases:
71 u e imgf | ~u e imgf
Or Not
Case 1
Prove: u e imgf => EXIST(d):[d e x & (u,d) e g]
Suppose...
72 u e imgf
Premise
Apply definition of g
73 ALL(b):[(u,b) e g <=> (u,b) e yx & [u e imgf & b=g'(u) | ~u e imgf & b=x0]]
U Spec, 49
74 (u,g'(u)) e g <=> (u,g'(u)) e yx & [u e imgf & g'(u)=g'(u) | ~u e imgf & g'(u)=x0]
U Spec, 73
75 [(u,g'(u)) e g => (u,g'(u)) e yx & [u e imgf & g'(u)=g'(u) | ~u e imgf & g'(u)=x0]]
& [(u,g'(u)) e yx & [u e imgf & g'(u)=g'(u) | ~u e imgf & g'(u)=x0] => (u,g'(u)) e g]
Iff-And, 74
76 (u,g'(u)) e g => (u,g'(u)) e yx & [u e imgf & g'(u)=g'(u) | ~u e imgf & g'(u)=x0]
Split, 75
Sufficient: (u,g'(u)) e g
77 (u,g'(u)) e yx & [u e imgf & g'(u)=g'(u) | ~u e imgf & g'(u)=x0] => (u,g'(u)) e g
Split, 75
Apply definition of yx
78 ALL(c2):[(u,c2) e yx <=> u e y & c2 e x]
U Spec, 45
79 (u,g'(u)) e yx <=> u e y & g'(u) e x
U Spec, 78
80 [(u,g'(u)) e yx => u e y & g'(u) e x]
& [u e y & g'(u) e x => (u,g'(u)) e yx]
Iff-And, 79
81 (u,g'(u)) e yx => u e y & g'(u) e x
Split, 80
82 u e y & g'(u) e x => (u,g'(u)) e yx
Split, 80
Apply definition of g'
83 u e imgf => g'(u) e x
U Spec, 35
84 g'(u) e x
Detach, 83, 72
85 u e y & g'(u) e x
Join, 70, 84
86 (u,g'(u)) e yx
Detach, 82, 85
87 g'(u)=g'(u)
Reflex
88 u e imgf & g'(u)=g'(u)
Join, 72, 87
89 u e imgf & g'(u)=g'(u) | ~u e imgf & g'(u)=x0
Arb Or, 88
90 (u,g'(u)) e yx
& [u e imgf & g'(u)=g'(u) | ~u e imgf & g'(u)=x0]
Join, 86, 89
91 (u,g'(u)) e g
Detach, 77, 90
92 g'(u) e x & (u,g'(u)) e g
Join, 84, 91
93 EXIST(d):[d e x & (u,d) e g]
E Gen, 92
As Required:
94 u e imgf => EXIST(d):[d e x & (u,d) e g]
4 Conclusion, 72
Case 2
Prove: ~u e imgf => EXIST(d):[d e x & (u,d) e g]
Suppose...
95 ~u e imgf
Premise
Apply definition of g
96 ALL(b):[(u,b) e g <=> (u,b) e yx & [u e imgf & b=g'(u) | ~u e imgf & b=x0]]
U Spec, 49
97 (u,x0) e g <=> (u,x0) e yx & [u e imgf & x0=g'(u) | ~u e imgf & x0=x0]
U Spec, 96
98 [(u,x0) e g => (u,x0) e yx & [u e imgf & x0=g'(u) | ~u e imgf & x0=x0]]
& [(u,x0) e yx & [u e imgf & x0=g'(u) | ~u e imgf & x0=x0] => (u,x0) e g]
Iff-And, 97
99 (u,x0) e g => (u,x0) e yx & [u e imgf & x0=g'(u) | ~u e imgf & x0=x0]
Split, 98
100 (u,x0) e yx & [u e imgf & x0=g'(u) | ~u e imgf & x0=x0] => (u,x0) e g
Split, 98
Apply definition of yx
101 ALL(c2):[(u,c2) e yx <=> u e y & c2 e x]
U Spec, 45
102 (u,x0) e yx <=> u e y & x0 e x
U Spec, 101
103 [(u,x0) e yx => u e y & x0 e x]
& [u e y & x0 e x => (u,x0) e yx]
Iff-And, 102
104 (u,x0) e yx => u e y & x0 e x
Split, 103
105 u e y & x0 e x => (u,x0) e yx
Split, 103
106 u e y & x0 e x
Join, 70, 12
107 (u,x0) e yx
Detach, 105, 106
108 x0=x0
Reflex
109 ~u e imgf & x0=x0
Join, 95, 108
110 u e imgf & x0=g'(u) | ~u e imgf & x0=x0
Arb Or, 109
111 (u,x0) e yx
& [u e imgf & x0=g'(u) | ~u e imgf & x0=x0]
Join, 107, 110
112 (u,x0) e g
Detach, 100, 111
113 x0 e x & (u,x0) e g
Join, 12, 112
114 EXIST(d):[d e x & (u,d) e g]
E Gen, 113
As Required:
115 ~u e imgf => EXIST(d):[d e x & (u,d) e g]
4 Conclusion, 95
Join results for Cases Rule
116 [u e imgf => EXIST(d):[d e x & (u,d) e g]]
& [~u e imgf => EXIST(d):[d e x & (u,d) e g]]
Join, 94, 115
Apply Cases Rule
117 EXIST(d):[d e x & (u,d) e g]
Cases, 71, 116
Functionality, Part 2
118 ALL(c):[c e y => EXIST(d):[d e x & (c,d) e g]]
4 Conclusion, 70
Prove: ALL(c):ALL(d1):ALL(d2):[(c,d1) e g & (c,d2) e g => d1=d2]
Suppose...
119 (t,u1) e g & (t,u2) e g
Premise
120 (t,u1) e g
Split, 119
121 (t,u2) e g
Split, 119
2 cases:
122 t e imgf | ~t e imgf
Or Not
Case 1
Prove: t e imgf => u1=u2
Suppose...
123 t e imgf
Premise
Apply definition of g
124 ALL(b):[(t,b) e g <=> (t,b) e yx & [t e imgf & b=g'(t) | ~t e imgf & b=x0]]
U Spec, 49
125 (t,u1) e g <=> (t,u1) e yx & [t e imgf & u1=g'(t) | ~t e imgf & u1=x0]
U Spec, 124
126 [(t,u1) e g => (t,u1) e yx & [t e imgf & u1=g'(t) | ~t e imgf & u1=x0]]
& [(t,u1) e yx & [t e imgf & u1=g'(t) | ~t e imgf & u1=x0] => (t,u1) e g]
Iff-And, 125
127 (t,u1) e g => (t,u1) e yx & [t e imgf & u1=g'(t) | ~t e imgf & u1=x0]
Split, 126
128 (t,u1) e yx & [t e imgf & u1=g'(t) | ~t e imgf & u1=x0] => (t,u1) e g
Split, 126
129 (t,u1) e yx & [t e imgf & u1=g'(t) | ~t e imgf & u1=x0]
Detach, 127, 120
130 (t,u1) e yx
Split, 129
131 t e imgf & u1=g'(t) | ~t e imgf & u1=x0
Split, 129
132 ~[t e imgf & u1=g'(t)] => ~t e imgf & u1=x0
Imply-Or, 131
133 ~[~t e imgf & u1=x0] => ~~[t e imgf & u1=g'(t)]
Contra, 132
134 ~[~t e imgf & u1=x0] => t e imgf & u1=g'(t)
Rem DNeg, 133
Prove: ~[~t e imgf & u1=x0]
Suppose to the contrary...
135 ~t e imgf & u1=x0
Premise
136 ~t e imgf
Split, 135
137 u1=x0
Split, 135
138 t e imgf & ~t e imgf
Join, 123, 136
As Required:
139 ~[~t e imgf & u1=x0]
4 Conclusion, 135
140 t e imgf & u1=g'(t)
Detach, 134, 139
141 t e imgf
Split, 140
142 u1=g'(t)
Split, 140
Apply definition of g
143 (t,u2) e g <=> (t,u2) e yx & [t e imgf & u2=g'(t) | ~t e imgf & u2=x0]
U Spec, 124
144 [(t,u2) e g => (t,u2) e yx & [t e imgf & u2=g'(t) | ~t e imgf & u2=x0]]
& [(t,u2) e yx & [t e imgf & u2=g'(t) | ~t e imgf & u2=x0] => (t,u2) e g]
Iff-And, 143
145 (t,u2) e g => (t,u2) e yx & [t e imgf & u2=g'(t) | ~t e imgf & u2=x0]
Split, 144
146 (t,u2) e yx & [t e imgf & u2=g'(t) | ~t e imgf & u2=x0] => (t,u2) e g
Split, 144
147 (t,u2) e yx & [t e imgf & u2=g'(t) | ~t e imgf & u2=x0]
Detach, 145, 121
148 (t,u2) e yx
Split, 147
149 t e imgf & u2=g'(t) | ~t e imgf & u2=x0
Split, 147
150 ~[t e imgf & u2=g'(t)] => ~t e imgf & u2=x0
Imply-Or, 149
151 ~[~t e imgf & u2=x0] => ~~[t e imgf & u2=g'(t)]
Contra, 150
152 ~[~t e imgf & u2=x0] => t e imgf & u2=g'(t)
Rem DNeg, 151
Prove: ~[~t e imgf & u2=x0]
Suppose to the contrary...
153 ~t e imgf & u2=x0
Premise
154 ~t e imgf
Split, 153
155 u2=x0
Split, 153
156 t e imgf & ~t e imgf
Join, 123, 154
As Required:
157 ~[~t e imgf & u2=x0]
4 Conclusion, 153
158 t e imgf & u2=g'(t)
Detach, 152, 157
159 t e imgf
Split, 158
160 u2=g'(t)
Split, 158
161 u1=u2
Substitute, 160, 142
As Required:
162 t e imgf => u1=u2
4 Conclusion, 123
Case 2
Prove: ~t e imgf => u1=u2
Suppose...
163 ~t e imgf
Premise
Apply definition of g
164 ALL(b):[(t,b) e g <=> (t,b) e yx & [t e imgf & b=g'(t) | ~t e imgf & b=x0]]
U Spec, 49
165 (t,u1) e g <=> (t,u1) e yx & [t e imgf & u1=g'(t) | ~t e imgf & u1=x0]
U Spec, 164
166 [(t,u1) e g => (t,u1) e yx & [t e imgf & u1=g'(t) | ~t e imgf & u1=x0]]
& [(t,u1) e yx & [t e imgf & u1=g'(t) | ~t e imgf & u1=x0] => (t,u1) e g]
Iff-And, 165
167 (t,u1) e g => (t,u1) e yx & [t e imgf & u1=g'(t) | ~t e imgf & u1=x0]
Split, 166
168 (t,u1) e yx & [t e imgf & u1=g'(t) | ~t e imgf & u1=x0] => (t,u1) e g
Split, 166
169 (t,u1) e yx & [t e imgf & u1=g'(t) | ~t e imgf & u1=x0]
Detach, 167, 120
170 (t,u1) e yx
Split, 169
171 t e imgf & u1=g'(t) | ~t e imgf & u1=x0
Split, 169
172 ~[t e imgf & u1=g'(t)] => ~t e imgf & u1=x0
Imply-Or, 171
Prove: ~[t e imgf & u1=g'(t)]
Suppose to the contrary...
173 t e imgf & u1=g'(t)
Premise
174 t e imgf
Split, 173
175 u1=g'(t)
Split, 173
176 t e imgf & ~t e imgf
Join, 174, 163
As Required:
177 ~[t e imgf & u1=g'(t)]
4 Conclusion, 173
178 ~t e imgf & u1=x0
Detach, 172, 177
179 ~t e imgf
Split, 178
180 u1=x0
Split, 178
Apply definition of g
181 (t,u2) e g <=> (t,u2) e yx & [t e imgf & u2=g'(t) | ~t e imgf & u2=x0]
U Spec, 164
182 [(t,u2) e g => (t,u2) e yx & [t e imgf & u2=g'(t) | ~t e imgf & u2=x0]]
& [(t,u2) e yx & [t e imgf & u2=g'(t) | ~t e imgf & u2=x0] => (t,u2) e g]
Iff-And, 181
183 (t,u2) e g => (t,u2) e yx & [t e imgf & u2=g'(t) | ~t e imgf & u2=x0]
Split, 182
184 (t,u2) e yx & [t e imgf & u2=g'(t) | ~t e imgf & u2=x0] => (t,u2) e g
Split, 182
185 (t,u2) e yx & [t e imgf & u2=g'(t) | ~t e imgf & u2=x0]
Detach, 183, 121
186 (t,u2) e yx
Split, 185
187 t e imgf & u2=g'(t) | ~t e imgf & u2=x0
Split, 185
188 ~[t e imgf & u2=g'(t)] => ~t e imgf & u2=x0
Imply-Or, 187
Prove: ~[t e imgf & u2=g'(t)]
Suppose...
189 t e imgf & u2=g'(t)
Premise
190 t e imgf
Split, 189
191 u2=g'(t)
Split, 189
192 t e imgf & ~t e imgf
Join, 190, 163
As Required:
193 ~[t e imgf & u2=g'(t)]
4 Conclusion, 189
194 ~t e imgf & u2=x0
Detach, 188, 193
195 ~t e imgf
Split, 194
196 u2=x0
Split, 194
197 u1=u2
Substitute, 196, 180
As Required:
198 ~t e imgf => u1=u2
4 Conclusion, 163
Join results for Cases Rule
199 [t e imgf => u1=u2] & [~t e imgf => u1=u2]
Join, 162, 198
Apply Cases Rule
200 u1=u2
Cases, 122, 199
Functionality, Part 3
201 ALL(c):ALL(d1):ALL(d2):[(c,d1) e g & (c,d2) e g => d1=d2]
4 Conclusion, 119
202 ALL(c):ALL(d):[(c,d) e g => c e y & d e x]
& ALL(c):[c e y => EXIST(d):[d e x & (c,d) e g]]
Join, 69, 118
203 ALL(c):ALL(d):[(c,d) e g => c e y & d e x]
& ALL(c):[c e y => EXIST(d):[d e x & (c,d) e g]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e g & (c,d2) e g => d1=d2]
Join, 202, 201
As Required:
g is a function
204 ALL(c):ALL(d):[d=g(c) <=> (c,d) e g]
Detach, 53, 203
Prove: ALL(a):[a e y => g(a) e x]
Suppose...
205 t e y
Premise
Apply functionality of g
206 t e y => EXIST(d):[d e x & (t,d) e g]
U Spec, 118
207 EXIST(d):[d e x & (t,d) e g]
Detach, 206, 205
208 u e x & (t,u) e g
E Spec, 207
209 u e x
Split, 208
210 (t,u) e g
Split, 208
Apply functionality of g
211 ALL(d):[d=g(t) <=> (t,d) e g]
U Spec, 204
212 u=g(t) <=> (t,u) e g
U Spec, 211
213 [u=g(t) => (t,u) e g] & [(t,u) e g => u=g(t)]
Iff-And, 212
214 u=g(t) => (t,u) e g
Split, 213
215 (t,u) e g => u=g(t)
Split, 213
216 u=g(t)
Detach, 215, 210
217 g(t) e x
Substitute, 216, 209
As Required:
218 ALL(a):[a e y => g(a) e x]
4 Conclusion, 205
Prove: ALL(a):[a e y => [a e imgf => g(a)=g'(a)] & [~a e imgf => g(a)=x0]]
Suppose...
219 t e y
Premise
Prove: t e imgf => g(t)=g'(t)
Suppose...
220 t e imgf
Premise
Apply definition of g
221 ALL(b):[(t,b) e g <=> (t,b) e yx & [t e imgf & b=g'(t) | ~t e imgf & b=x0]]
U Spec, 49
222 (t,g'(t)) e g <=> (t,g'(t)) e yx & [t e imgf & g'(t)=g'(t) | ~t e imgf & g'(t)=x0]
U Spec, 221
223 [(t,g'(t)) e g => (t,g'(t)) e yx & [t e imgf & g'(t)=g'(t) | ~t e imgf & g'(t)=x0]]
& [(t,g'(t)) e yx & [t e imgf & g'(t)=g'(t) | ~t e imgf & g'(t)=x0] => (t,g'(t)) e g]
Iff-And, 222
224 (t,g'(t)) e g => (t,g'(t)) e yx & [t e imgf & g'(t)=g'(t) | ~t e imgf & g'(t)=x0]
Split, 223
Sufficient: (t,g'(t)) e g
225 (t,g'(t)) e yx & [t e imgf & g'(t)=g'(t) | ~t e imgf & g'(t)=x0] => (t,g'(t)) e g
Split, 223
Apply definition of yx
226 ALL(c2):[(t,c2) e yx <=> t e y & c2 e x]
U Spec, 45
227 (t,g'(t)) e yx <=> t e y & g'(t) e x
U Spec, 226
228 [(t,g'(t)) e yx => t e y & g'(t) e x]
& [t e y & g'(t) e x => (t,g'(t)) e yx]
Iff-And, 227
229 (t,g'(t)) e yx => t e y & g'(t) e x
Split, 228
230 t e y & g'(t) e x => (t,g'(t)) e yx
Split, 228
Apply definition of imgf
231 t e imgf => g'(t) e x
U Spec, 35
232 g'(t) e x
Detach, 231, 220
233 t e y & g'(t) e x
Join, 219, 232
234 (t,g'(t)) e yx
Detach, 230, 233
235 g'(t)=g'(t)
Reflex
236 t e imgf & g'(t)=g'(t)
Join, 220, 235
237 t e imgf & g'(t)=g'(t) | ~t e imgf & g'(t)=x0
Arb Or, 236
238 (t,g'(t)) e yx
& [t e imgf & g'(t)=g'(t) | ~t e imgf & g'(t)=x0]
Join, 234, 237
239 (t,g'(t)) e g
Detach, 225, 238
Apply functionality of g
240 ALL(d):[d=g(t) <=> (t,d) e g]
U Spec, 204
241 g'(t)=g(t) <=> (t,g'(t)) e g
U Spec, 240
242 [g'(t)=g(t) => (t,g'(t)) e g]
& [(t,g'(t)) e g => g'(t)=g(t)]
Iff-And, 241
243 g'(t)=g(t) => (t,g'(t)) e g
Split, 242
244 (t,g'(t)) e g => g'(t)=g(t)
Split, 242
245 g'(t)=g(t)
Detach, 244, 239
246 g(t)=g'(t)
Sym, 245
As Required:
247 t e imgf => g(t)=g'(t)
4 Conclusion, 220
Prove: ~t e imgf => g(t)=x0
Suppose...
248 ~t e imgf
Premise
Apply definition of g
249 ALL(b):[(t,b) e g <=> (t,b) e yx & [t e imgf & b=g'(t) | ~t e imgf & b=x0]]
U Spec, 49
250 (t,x0) e g <=> (t,x0) e yx & [t e imgf & x0=g'(t) | ~t e imgf & x0=x0]
U Spec, 249
251 [(t,x0) e g => (t,x0) e yx & [t e imgf & x0=g'(t) | ~t e imgf & x0=x0]]
& [(t,x0) e yx & [t e imgf & x0=g'(t) | ~t e imgf & x0=x0] => (t,x0) e g]
Iff-And, 250
252 (t,x0) e g => (t,x0) e yx & [t e imgf & x0=g'(t) | ~t e imgf & x0=x0]
Split, 251
253 (t,x0) e yx & [t e imgf & x0=g'(t) | ~t e imgf & x0=x0] => (t,x0) e g
Split, 251
Apply definition of yx
254 ALL(c2):[(t,c2) e yx <=> t e y & c2 e x]
U Spec, 45
255 (t,x0) e yx <=> t e y & x0 e x
U Spec, 254
256 [(t,x0) e yx => t e y & x0 e x]
& [t e y & x0 e x => (t,x0) e yx]
Iff-And, 255
257 (t,x0) e yx => t e y & x0 e x
Split, 256
258 t e y & x0 e x => (t,x0) e yx
Split, 256
259 t e y & x0 e x
Join, 219, 12
260 (t,x0) e yx
Detach, 258, 259
261 x0=x0
Reflex
262 ~t e imgf & x0=x0
Join, 248, 261
263 t e imgf & x0=g'(t) | ~t e imgf & x0=x0
Arb Or, 262
264 (t,x0) e yx
& [t e imgf & x0=g'(t) | ~t e imgf & x0=x0]
Join, 260, 263
265 (t,x0) e g
Detach, 253, 264
Apply functionality of g
266 ALL(d):[d=g(t) <=> (t,d) e g]
U Spec, 204
267 x0=g(t) <=> (t,x0) e g
U Spec, 266
268 [x0=g(t) => (t,x0) e g] & [(t,x0) e g => x0=g(t)]
Iff-And, 267
269 x0=g(t) => (t,x0) e g
Split, 268
270 (t,x0) e g => x0=g(t)
Split, 268
271 x0=g(t)
Detach, 270, 265
272 g(t)=x0
Sym, 271
As Required:
273 ~t e imgf => g(t)=x0
4 Conclusion, 248
Joining results...
274 [t e imgf => g(t)=g'(t)] & [~t e imgf => g(t)=x0]
Join, 247, 273
As Required:
275 ALL(a):[a e y
=> [a e imgf => g(a)=g'(a)] & [~a e imgf => g(a)=x0]]
4 Conclusion, 219
Prove: ALL(a):[a e x => g(f(a))=a]
Suppose...
276 t e x
Premise
Apply definition of f
277 t e x => f(t) e y
U Spec, 10
278 f(t) e y
Detach, 277, 276
Apply definition of imgf
279 f(t) e imgf <=> f(t) e y & EXIST(e):[e e x & f(e)=f(t)]
U Spec, 23
280 [f(t) e imgf => f(t) e y & EXIST(e):[e e x & f(e)=f(t)]]
& [f(t) e y & EXIST(e):[e e x & f(e)=f(t)] => f(t) e imgf]
Iff-And, 279
281 f(t) e imgf => f(t) e y & EXIST(e):[e e x & f(e)=f(t)]
Split, 280
282 f(t) e y & EXIST(e):[e e x & f(e)=f(t)] => f(t) e imgf
Split, 280
283 t e x => f(t) e y
U Spec, 10
284 f(t) e y
Detach, 283, 276
285 f(t)=f(t)
Reflex
286 t e x & f(t)=f(t)
Join, 276, 285
287 EXIST(e):[e e x & f(e)=f(t)]
E Gen, 286
288 f(t) e y & EXIST(e):[e e x & f(e)=f(t)]
Join, 284, 287
289 f(t) e imgf
Detach, 282, 288
Apply previous result
290 f(t) e y
=> [f(t) e imgf => g(f(t))=g'(f(t))] & [~f(t) e imgf => g(f(t))=x0]
U Spec, 275
291 [f(t) e imgf => g(f(t))=g'(f(t))] & [~f(t) e imgf => g(f(t))=x0]
Detach, 290, 284
292 f(t) e imgf => g(f(t))=g'(f(t))
Split, 291
293 ~f(t) e imgf => g(f(t))=x0
Split, 291
294 g(f(t))=g'(f(t))
Detach, 292, 289
Apply previous result
295 ALL(d):[t e x & d e imgf => [g'(d)=t <=> f'(t)=d]]
U Spec, 36
296 t e x & f'(t) e imgf => [g'(f'(t))=t <=> f'(t)=f'(t)]
U Spec, 295
Apply definition of f'
297 t e x => f'(t)=f(t)
U Spec, 25
298 f'(t)=f(t)
Detach, 297, 276
299 g(f(t))=g'(f'(t))
Substitute, 298, 294
300 f'(t) e imgf
Substitute, 298, 289
301 t e x & f'(t) e imgf
Join, 276, 300
302 g'(f'(t))=t <=> f'(t)=f'(t)
Detach, 296, 301
303 [g'(f'(t))=t => f'(t)=f'(t)]
& [f'(t)=f'(t) => g'(f'(t))=t]
Iff-And, 302
304 g'(f'(t))=t => f'(t)=f'(t)
Split, 303
305 f'(t)=f'(t) => g'(f'(t))=t
Split, 303
306 f'(t)=f'(t)
Reflex
307 g'(f'(t))=t
Detach, 305, 306
308 g(f(t))=t
Substitute, 299, 307
As Required:
309 ALL(a):[a e x => g(f(a))=a]
4 Conclusion, 276
Apply definition of Surjection
310 ALL(a):ALL(b):[Surjection(g,a,b) <=> ALL(c):[c e b => EXIST(d):[d e a & g(d)=c]]]
U Spec, 2
311 ALL(b):[Surjection(g,y,b) <=> ALL(c):[c e b => EXIST(d):[d e y & g(d)=c]]]
U Spec, 310
312 Surjection(g,y,x) <=> ALL(c):[c e x => EXIST(d):[d e y & g(d)=c]]
U Spec, 311
313 [Surjection(g,y,x) => ALL(c):[c e x => EXIST(d):[d e y & g(d)=c]]]
& [ALL(c):[c e x => EXIST(d):[d e y & g(d)=c]] => Surjection(g,y,x)]
Iff-And, 312
314 Surjection(g,y,x) => ALL(c):[c e x => EXIST(d):[d e y & g(d)=c]]
Split, 313
Sufficient: Surjection(g,y,x)
315 ALL(c):[c e x => EXIST(d):[d e y & g(d)=c]] => Surjection(g,y,x)
Split, 313
Prove: ALL(c):[c e x => EXIST(d):[d e y & g(d)=c]]
Suppose...
316 t e x
Premise
Apply previous result
317 t e x => g(f(t))=t
U Spec, 309
318 g(f(t))=t
Detach, 317, 316
319 t e x => f(t) e y
U Spec, 10
320 f(t) e y
Detach, 319, 316
321 f(t) e y & g(f(t))=t
Join, 320, 318
322 EXIST(d):[d e y & g(d)=t]
E Gen, 321
As Required:
323 ALL(c):[c e x => EXIST(d):[d e y & g(d)=c]]
4 Conclusion, 316
As Required:
324 Surjection(g,y,x)
Detach, 315, 323
325 ALL(c):[c e y => g(c) e x]
Rename, 218
326 ALL(c):[c e y => g(c) e x] & Surjection(g,y,x)
Join, 325, 324
As Required:
327 ALL(a):ALL(b):ALL(f1):[Set(a)
& Set(b)
& EXIST(c):c e a
& ALL(c):[c e a => f1(c) e b]
& Injection(f1,a,b)
=> EXIST(f2):[ALL(c):[c e b => f2(c) e a] & Surjection(f2,b,a)]]
4 Conclusion, 6