THEOREM
*******
Bijectivity is
transitive.
Informally: |A|=|B| &
|B|=|C| => |A|=|C|
Formally:
ALL(t):ALL(u):ALL(v):[Set(t)
& Set(u) & Set(v)
=> [EXIST(f):[ALL(a):[a
in t => f(a) in u] & Bijection(f,t,u)]
& EXIST(f):[ALL(a):[a
in u => f(a) in v] & Bijection(f,u,v)]
=> EXIST(h):Bijection(h,t,v)]]
Where Bijection(f,x,y) means f is a bijection mapping set x to set y.
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
Dan Christensen
2022-07-01
DEFINITIONS
***********
Define: Injection
1 ALL(f):ALL(a):ALL(b):[Set(a) & Set(b) & ALL(c):[c e a => f(c) e 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):[Set(a) & Set(b) & ALL(c):[c e a => f(c) e 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):[Set(a) & Set(b) & ALL(c):[c e a => f(c) e b]
=>
[Bijection(f,a,b) <=>
Injection(f,a,b) & Surjection(f,a,b)]]
Axiom
Suppose...
4 Set(t) & Set(u) & Set(v)
Premise
5 Set(t)
Split, 4
6 Set(u)
Split, 4
7 Set(v)
Split, 4
Suppose...
8 EXIST(f):[ALL(a):[a e t => f(a) e u] & Bijection(f,t,u)]
&
EXIST(f):[ALL(a):[a e u => f(a) e v] & Bijection(f,u,v)]
Premise
9 EXIST(f):[ALL(a):[a e t => f(a) e u] & Bijection(f,t,u)]
Split, 8
10 EXIST(f):[ALL(a):[a e u => f(a) e v] & Bijection(f,u,v)]
Split, 8
Define: Bijection f: t --> u
11 ALL(a):[a e t => f(a) e u] & Bijection(f,t,u)
E Spec, 9
12 ALL(a):[a e t => f(a) e u]
Split, 11
13 Bijection(f,t,u)
Split, 11
Define: Bijection g: u --> v
14 ALL(a):[a e u => g(a) e v] & Bijection(g,u,v)
E Spec, 10
15 ALL(a):[a e u => g(a) e v]
Split, 14
16 Bijection(g,u,v)
Split, 14
Construct function h
17 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
18 ALL(a2):[Set(t) & Set(a2) => EXIST(b):[Set'(b) &
ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e t & c2 e a2]]]
U Spec, 17
19 Set(t) & Set(v) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e t & c2 e v]]
U Spec, 18
20 Set(t) & Set(v)
Join, 5, 7
21 EXIST(b):[Set'(b) &
ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e t & c2 e v]]
Detach, 19, 20
22 Set'(tv) & ALL(c1):ALL(c2):[(c1,c2) e tv <=> c1 e t & c2 e v]
E Spec, 21
Define: tv Cartesian Product t*v
23 Set'(tv)
Split, 22
24 ALL(c1):ALL(c2):[(c1,c2) e tv <=> c1 e t & c2 e v]
Split, 22
25 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e tv & b=g(f(a))]]
Subset, 23
26 Set'(gra) &
ALL(a):ALL(b):[(a,b) e gra <=> (a,b) e tv & b=g(f(a))]
E Spec, 25
Define: gra Graph set for function h
27 Set'(gra)
Split, 26
28 ALL(a):ALL(b):[(a,b) e gra <=> (a,b) e tv & b=g(f(a))]
Split, 26
Apply Function Axiom
29 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
30 ALL(cod):ALL(gra):[Set(t) & Set(cod)
& Set'(gra)
=>
[ALL(a1):ALL(b):[(a1,b) e gra => a1 e t & b e cod]
&
ALL(a1):[a1 e t =>
EXIST(b):[b e cod & (a1,b) e gra]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e t & b1 e cod & b2 e cod
=>
[(a1,b1) e gra & (a1,b2) e gra => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e t & b e cod
=>
[fun(a1)=b <=> (a1,b) e gra]]]]
U Spec, 29
31 ALL(gra):[Set(t) & Set(v) & Set'(gra)
=>
[ALL(a1):ALL(b):[(a1,b) e gra => a1 e t & b e v]
&
ALL(a1):[a1 e t =>
EXIST(b):[b e v & (a1,b) e gra]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e t & b1 e v & b2 e v
=>
[(a1,b1) e gra & (a1,b2) e gra => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e t & b e v
=>
[fun(a1)=b <=> (a1,b) e gra]]]]
U Spec, 30
32 Set(t) & Set(v) & Set'(gra)
=>
[ALL(a1):ALL(b):[(a1,b) e gra => a1 e t & b e v]
&
ALL(a1):[a1 e t =>
EXIST(b):[b e v & (a1,b) e gra]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e t & b1 e v & b2 e v
=>
[(a1,b1) e gra & (a1,b2) e gra => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e t & b e v
=>
[fun(a1)=b <=> (a1,b) e gra]]]
U Spec, 31
33 Set(t) & Set(v)
Join, 5, 7
34 Set(t) & Set(v) & Set'(gra)
Join, 33, 27
Sufficient: For functionality of graph set
35 ALL(a1):ALL(b):[(a1,b) e gra => a1 e t & b e v]
&
ALL(a1):[a1 e t =>
EXIST(b):[b e v & (a1,b) e gra]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e t & b1 e v & b2 e v
=>
[(a1,b1) e gra & (a1,b2) e gra => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e t & b e v
=>
[fun(a1)=b <=> (a1,b) e gra]]
Detach, 32, 34
Prove: ALL(a1):ALL(b):[(a1,b) e gra => a1 e t & b e v]
Suppose...
36 (x,y) e gra
Premise
37 ALL(b):[(x,b) e gra <=> (x,b) e tv & b=g(f(x))]
U Spec, 28
38 (x,y) e gra <=> (x,y) e tv & y=g(f(x))
U Spec, 37
39 [(x,y) e gra => (x,y) e tv & y=g(f(x))]
&
[(x,y) e tv & y=g(f(x)) => (x,y) e gra]
Iff-And, 38
40 (x,y) e gra => (x,y) e tv & y=g(f(x))
Split, 39
41 (x,y) e tv & y=g(f(x))
Detach, 40, 36
42 (x,y) e tv
Split, 41
43 ALL(c2):[(x,c2) e tv <=> x e t & c2 e v]
U Spec, 24
44 (x,y) e tv <=> x e t & y e v
U Spec, 43
45 [(x,y) e tv => x e t & y e v]
&
[x e t & y e v => (x,y) e tv]
Iff-And, 44
46 (x,y) e tv => x e t & y e v
Split, 45
47 x e t & y e v
Detach, 46, 42
Part 1
48 ALL(a1):ALL(b):[(a1,b) e gra => a1 e t & b e v]
4 Conclusion, 36
Prove: ALL(a1):[a1 e t => EXIST(b):[b e v &
(a1,b) e gra]]
Suppose...
49 x e t
Premise
50 x e t => f(x) e u
U Spec, 12
51 f(x) e u
Detach, 50, 49
52 f(x) e u => g(f(x)) e v
U Spec, 15, 51
53 g(f(x)) e v
Detach, 52, 51
54 ALL(b):[(x,b) e gra <=> (x,b) e tv & b=g(f(x))]
U Spec, 28
55 (x,g(f(x))) e gra <=> (x,g(f(x))) e tv & g(f(x))=g(f(x))
U Spec, 54, 53
56 [(x,g(f(x))) e gra => (x,g(f(x))) e tv & g(f(x))=g(f(x))]
&
[(x,g(f(x))) e tv & g(f(x))=g(f(x)) => (x,g(f(x))) e gra]
Iff-And, 55
Sufficient: For (x,g(f(x)))
e gra
57 (x,g(f(x))) e tv & g(f(x))=g(f(x)) => (x,g(f(x))) e gra
Split, 56
58 ALL(c2):[(x,c2) e tv <=> x e t & c2 e v]
U Spec, 24
59 (x,g(f(x))) e tv <=> x e t & g(f(x)) e v
U Spec, 58, 53
60 [(x,g(f(x))) e tv => x e t & g(f(x)) e v]
&
[x e t & g(f(x)) e v => (x,g(f(x))) e tv]
Iff-And, 59
61 x e t & g(f(x)) e v => (x,g(f(x))) e tv
Split, 60
62 x e t & g(f(x)) e v
Join, 49, 53
63 (x,g(f(x))) e tv
Detach, 61, 62
64 g(f(x))=g(f(x))
Reflex, 53
65 (x,g(f(x))) e tv & g(f(x))=g(f(x))
Join, 63, 64
66 (x,g(f(x))) e gra
Detach, 57, 65
67 g(f(x)) e v & (x,g(f(x))) e gra
Join, 53, 66
68 EXIST(b):[b e v & (x,b) e gra]
E Gen, 67
Part 2
69 ALL(a1):[a1 e t =>
EXIST(b):[b e v & (a1,b) e gra]]
4 Conclusion, 49
Prove: ALL(a1):ALL(b1):ALL(b2):[a1
e t & b1 e v & b2 e v
=> [(a1,b1) e gra &
(a1,b2) e gra => b1=b2]]
Suppose...
70 x e t & y1 e v & y2 e v
Premise
71 x e t
Split, 70
72 y1 e v
Split, 70
73 y2 e v
Split, 70
Prove: (x,y1) e gra &
(x,y2) e gra => y1=y2
Suppose...
74 (x,y1) e gra & (x,y2) e gra
Premise
75 (x,y1) e gra
Split, 74
76 (x,y2) e gra
Split, 74
77 ALL(b):[(x,b) e gra <=> (x,b) e tv & b=g(f(x))]
U Spec, 28
78 (x,y1) e gra <=> (x,y1) e tv & y1=g(f(x))
U Spec, 77
79 [(x,y1) e gra => (x,y1) e tv & y1=g(f(x))]
&
[(x,y1) e tv & y1=g(f(x)) => (x,y1) e gra]
Iff-And, 78
80 (x,y1) e gra => (x,y1) e tv & y1=g(f(x))
Split, 79
81 (x,y1) e tv & y1=g(f(x))
Detach, 80, 75
82 y1=g(f(x))
Split, 81
83 (x,y2) e gra <=> (x,y2) e tv & y2=g(f(x))
U Spec, 77
84 [(x,y2) e gra => (x,y2) e tv & y2=g(f(x))]
&
[(x,y2) e tv & y2=g(f(x)) => (x,y2) e gra]
Iff-And, 83
85 (x,y2) e gra => (x,y2) e tv & y2=g(f(x))
Split, 84
86 (x,y2) e tv & y2=g(f(x))
Detach, 85, 76
87 y2=g(f(x))
Split, 86
88 y1=y2
Substitute, 87,
82
As Required:
89 (x,y1) e gra & (x,y2) e gra => y1=y2
4 Conclusion, 74
Part 3
90 ALL(a1):ALL(b1):ALL(b2):[a1 e t & b1 e v & b2 e v
=>
[(a1,b1) e gra & (a1,b2) e gra => b1=b2]]
4 Conclusion, 70
91 ALL(a1):ALL(b):[(a1,b) e gra => a1 e t & b e v]
&
ALL(a1):[a1 e t => EXIST(b):[b e v & (a1,b) e gra]]
Join, 48, 69
92 ALL(a1):ALL(b):[(a1,b) e gra => a1 e t & b e v]
&
ALL(a1):[a1 e t =>
EXIST(b):[b e v & (a1,b) e gra]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e t & b1 e v & b2 e v
=>
[(a1,b1) e gra & (a1,b2) e gra => b1=b2]]
Join, 91, 90
93 EXIST(fun):ALL(a1):ALL(b):[a1 e t & b e v
=>
[fun(a1)=b <=> (a1,b) e gra]]
Detach, 35, 92
Define: h in terms
of gra
94 ALL(a1):ALL(b):[a1 e t & b e v
=>
[h(a1)=b <=> (a1,b) e gra]]
E Spec, 93
Prove: ALL(a):[a e t => h(a) e v]
Suppose...
95 x e t
Premise
96 x e t => EXIST(b):[b e v & (x,b) e gra]
U Spec, 69
97 EXIST(b):[b e v & (x,b) e gra]
Detach, 96, 95
98 y e v & (x,y) e gra
E Spec, 97
99 y e v
Split, 98
100 (x,y) e gra
Split, 98
101 ALL(b):[x e t & b e v
=>
[h(x)=b <=> (x,b) e gra]]
U Spec, 94
102 x e t & y e v
=>
[h(x)=y <=> (x,y) e gra]
U Spec, 101
103 x e t & y e v
Join, 95, 99
104 h(x)=y <=> (x,y) e gra
Detach, 102, 103
105 [h(x)=y => (x,y) e gra] & [(x,y) e gra => h(x)=y]
Iff-And, 104
106 (x,y) e gra => h(x)=y
Split, 105
107 h(x)=y
Detach, 106, 100
108 h(x) e v
Substitute, 107,
99
As Required:
109 ALL(a):[a e t => h(a) e v]
4 Conclusion, 95
Prove: ALL(a):[a e t => h(a)=g(f(a))]
Suppose...
110 x e t
Premise
111 x e t => EXIST(b):[b e v & (x,b) e gra]
U Spec, 69
112 EXIST(b):[b e v & (x,b) e gra]
Detach, 111, 110
113 y e v & (x,y) e gra
E Spec, 112
114 y e v
Split, 113
115 (x,y) e gra
Split, 113
116 ALL(b):[(x,b) e gra <=> (x,b) e tv & b=g(f(x))]
U Spec, 28
117 (x,y) e gra <=> (x,y) e tv & y=g(f(x))
U Spec, 116
118 [(x,y) e gra => (x,y) e tv & y=g(f(x))]
&
[(x,y) e tv & y=g(f(x)) => (x,y) e gra]
Iff-And, 117
119 (x,y) e gra => (x,y) e tv & y=g(f(x))
Split, 118
120 (x,y) e tv & y=g(f(x))
Detach, 119, 115
121 (x,y) e tv
Split, 120
122 y=g(f(x))
Split, 120
123 (x,g(f(x))) e gra
Substitute, 122,
115
124 ALL(b):[x e t & b e v
=>
[h(x)=b <=> (x,b) e gra]]
U Spec, 94
125 x e t => f(x) e u
U Spec, 12
126 f(x) e u
Detach, 125, 110
127 f(x) e u => g(f(x)) e v
U Spec, 15, 126
128 g(f(x)) e v
Detach, 127, 126
129 x e t & g(f(x)) e v
=>
[h(x)=g(f(x)) <=> (x,g(f(x))) e gra]
U Spec, 124, 128
130 x e t & g(f(x)) e v
Join, 110, 128
131 h(x)=g(f(x)) <=> (x,g(f(x))) e gra
Detach, 129, 130
132 [h(x)=g(f(x)) => (x,g(f(x))) e gra]
&
[(x,g(f(x))) e gra => h(x)=g(f(x))]
Iff-And, 131
133 (x,g(f(x))) e gra => h(x)=g(f(x))
Split, 132
134 h(x)=g(f(x))
Detach, 133, 123
As Required:
135 ALL(a):[a e t => h(a)=g(f(a))]
4 Conclusion, 110
Apply definition of Bijection
136 ALL(a):ALL(b):[Set(a) & Set(b) &
ALL(c):[c e a => h(c) e b]
=>
[Bijection(h,a,b) <=>
Injection(h,a,b) & Surjection(h,a,b)]]
U Spec, 3
137 ALL(b):[Set(t) & Set(b) & ALL(c):[c e t => h(c) e b]
=>
[Bijection(h,t,b) <=>
Injection(h,t,b) & Surjection(h,t,b)]]
U Spec, 136
138 Set(t) & Set(v) &
ALL(c):[c e t => h(c) e v]
=>
[Bijection(h,t,v) <=>
Injection(h,t,v) & Surjection(h,t,v)]
U Spec, 137
139 Set(t) & Set(v)
Join, 5, 7
140 Set(t) & Set(v) &
ALL(a):[a e t => h(a) e v]
Join, 139, 109
141 Bijection(h,t,v) <=>
Injection(h,t,v) & Surjection(h,t,v)
Detach, 138, 140
142 [Bijection(h,t,v) =>
Injection(h,t,v) & Surjection(h,t,v)]
&
[Injection(h,t,v) & Surjection(h,t,v) => Bijection(h,t,v)]
Iff-And, 141
Sufficient: For Bijection(h,t,v)
143 Injection(h,t,v) & Surjection(h,t,v) => Bijection(h,t,v)
Split, 142
144 ALL(a):ALL(b):[Set(a) & Set(b) &
ALL(c):[c e a => f(c) e b]
=>
[Bijection(f,a,b) <=>
Injection(f,a,b) & Surjection(f,a,b)]]
U Spec, 3
145 ALL(b):[Set(t) & Set(b) & ALL(c):[c e t => f(c) e b]
=>
[Bijection(f,t,b) <=>
Injection(f,t,b) & Surjection(f,t,b)]]
U Spec, 144
146 Set(t) & Set(u) & ALL(c):[c e t => f(c) e u]
=>
[Bijection(f,t,u) <=>
Injection(f,t,u) & Surjection(f,t,u)]
U Spec, 145
147 Set(t) & Set(u)
Join, 5, 6
148 Set(t) & Set(u) &
ALL(a):[a e t => f(a) e u]
Join, 147, 12
149 Bijection(f,t,u) <=>
Injection(f,t,u) & Surjection(f,t,u)
Detach, 146, 148
150 [Bijection(f,t,u) =>
Injection(f,t,u) & Surjection(f,t,u)]
&
[Injection(f,t,u) & Surjection(f,t,u) => Bijection(f,t,u)]
Iff-And, 149
151 Bijection(f,t,u) =>
Injection(f,t,u) & Surjection(f,t,u)
Split, 150
152 Injection(f,t,u) &
Surjection(f,t,u)
Detach, 151, 13
153 Injection(f,t,u)
Split, 152
154 Surjection(f,t,u)
Split, 152
155 ALL(a):ALL(b):[Set(a) & Set(b) &
ALL(c):[c e a => g(c) e b]
=>
[Bijection(g,a,b) <=>
Injection(g,a,b) & Surjection(g,a,b)]]
U Spec, 3
156 ALL(b):[Set(u) & Set(b) & ALL(c):[c e u => g(c) e b]
=>
[Bijection(g,u,b) <=>
Injection(g,u,b) & Surjection(g,u,b)]]
U Spec, 155
157 Set(u) & Set(v) &
ALL(c):[c e u => g(c) e v]
=>
[Bijection(g,u,v) <=>
Injection(g,u,v) & Surjection(g,u,v)]
U Spec, 156
158 Set(u) & Set(v)
Join, 6, 7
159 Set(u) & Set(v) &
ALL(a):[a e u => g(a) e v]
Join, 158, 15
160 Bijection(g,u,v) <=>
Injection(g,u,v) & Surjection(g,u,v)
Detach, 157, 159
161 [Bijection(g,u,v) =>
Injection(g,u,v) & Surjection(g,u,v)]
&
[Injection(g,u,v) & Surjection(g,u,v) => Bijection(g,u,v)]
Iff-And, 160
162 Bijection(g,u,v) =>
Injection(g,u,v) & Surjection(g,u,v)
Split, 161
163 Injection(g,u,v) & Surjection(g,u,v)
Detach, 162, 16
164 Injection(g,u,v)
Split, 163
165 Surjection(g,u,v)
Split, 163
166 ALL(a):ALL(b):[Set(a) & Set(b) &
ALL(c):[c e a => h(c) e b]
=>
[Injection(h,a,b) <=>
ALL(c):ALL(d):[c e a & d e a => [h(c)=h(d) => c=d]]]]
U Spec, 1
167 ALL(b):[Set(t) & Set(b) & ALL(c):[c e t => h(c) e b]
=>
[Injection(h,t,b) <=>
ALL(c):ALL(d):[c e t & d e t => [h(c)=h(d) =>
c=d]]]]
U Spec, 166
168 Set(t) & Set(v) &
ALL(c):[c e t => h(c) e v]
=>
[Injection(h,t,v) <=>
ALL(c):ALL(d):[c e t & d e t => [h(c)=h(d) => c=d]]]
U Spec, 167
169 Set(t) & Set(v)
Join, 5, 7
170 Set(t) & Set(v) &
ALL(a):[a e t => h(a) e v]
Join, 169, 109
171 Injection(h,t,v) <=>
ALL(c):ALL(d):[c e t & d e t => [h(c)=h(d) => c=d]]
Detach, 168, 170
172 [Injection(h,t,v) =>
ALL(c):ALL(d):[c e t & d e t => [h(c)=h(d) => c=d]]]
&
[ALL(c):ALL(d):[c e t & d e t => [h(c)=h(d) => c=d]] => Injection(h,t,v)]
Iff-And, 171
Sufficient: For Injection(h,t,v)
173 ALL(c):ALL(d):[c e t & d e t => [h(c)=h(d) => c=d]]
=> Injection(h,t,v)
Split, 172
Prove: ALL(a):ALL(b):[a e t & b e t =>
[h(a)=h(b) => a=b]]
Suppose...
174 x e t & y e t
Premise
175 x e t
Split, 174
176 y e t
Split, 174
Prove: h(x)=h(y) => x=y
Suppose...
177 h(x)=h(y)
Premise
178 x e t => h(x)=g(f(x))
U Spec, 135
179 h(x)=g(f(x))
Detach, 178, 175
180 y e t => h(y)=g(f(y))
U Spec, 135
181 h(y)=g(f(y))
Detach, 180, 176
182 g(f(x))=h(y)
Substitute, 179,
177
183 g(f(x))=g(f(y))
Substitute, 181,
182
184 ALL(a):ALL(b):[Set(a) & Set(b) &
ALL(c):[c e a => g(c) e b]
=>
[Bijection(g,a,b) <=>
Injection(g,a,b) & Surjection(g,a,b)]]
U Spec, 3
185 ALL(b):[Set(u) & Set(b) & ALL(c):[c e u => g(c) e b]
=>
[Bijection(g,u,b) <=>
Injection(g,u,b) & Surjection(g,u,b)]]
U Spec, 184
186 Set(u) & Set(v) &
ALL(c):[c e u => g(c) e v]
=>
[Bijection(g,u,v) <=>
Injection(g,u,v) & Surjection(g,u,v)]
U Spec, 185
187 Set(u) & Set(v)
Join, 6, 7
188 Set(u) & Set(v) &
ALL(a):[a e u => g(a) e v]
Join, 187, 15
189 Bijection(g,u,v) <=>
Injection(g,u,v) & Surjection(g,u,v)
Detach, 186, 188
190 [Bijection(g,u,v) =>
Injection(g,u,v) & Surjection(g,u,v)]
&
[Injection(g,u,v) & Surjection(g,u,v) => Bijection(g,u,v)]
Iff-And, 189
191 Bijection(g,u,v) =>
Injection(g,u,v) & Surjection(g,u,v)
Split, 190
192 Injection(g,u,v) & Surjection(g,u,v)
Detach, 191, 16
193 Injection(g,u,v)
Split, 192
194 Surjection(g,u,v)
Split, 192
195 ALL(a):ALL(b):[Set(a) & Set(b) &
ALL(c):[c e a => g(c) e b]
=>
[Injection(g,a,b) <=>
ALL(c):ALL(d):[c e a & d e a => [g(c)=g(d) =>
c=d]]]]
U Spec, 1
196 ALL(b):[Set(u) & Set(b) & ALL(c):[c e u => g(c) e b]
=>
[Injection(g,u,b) <=>
ALL(c):ALL(d):[c e u & d e u => [g(c)=g(d) =>
c=d]]]]
U Spec, 195
197 Set(u) & Set(v) &
ALL(c):[c e u => g(c) e v]
=> [Injection(g,u,v) <=> ALL(c):ALL(d):[c e u & d e u => [g(c)=g(d) => c=d]]]
U Spec, 196
198 Injection(g,u,v) <=>
ALL(c):ALL(d):[c e u & d e u => [g(c)=g(d) => c=d]]
Detach, 197, 188
199 [Injection(g,u,v) =>
ALL(c):ALL(d):[c e u & d e u => [g(c)=g(d) => c=d]]]
&
[ALL(c):ALL(d):[c e u & d e u => [g(c)=g(d) => c=d]] => Injection(g,u,v)]
Iff-And, 198
200 Injection(g,u,v) =>
ALL(c):ALL(d):[c e u & d e u => [g(c)=g(d) => c=d]]
Split, 199
201 ALL(c):ALL(d):[c e u & d e u => [g(c)=g(d) => c=d]]
Detach, 200, 193
202 x e t => f(x) e u
U Spec, 12
203 f(x) e u
Detach, 202, 175
204 y e t => f(y) e u
U Spec, 12
205 f(y) e u
Detach, 204, 176
206 ALL(d):[f(x) e u & d e u => [g(f(x))=g(d) => f(x)=d]]
U Spec, 201, 203
207 f(x) e u & f(y) e u => [g(f(x))=g(f(y)) => f(x)=f(y)]
U Spec, 206, 205
208 f(x) e u & f(y) e u
Join, 203, 205
209 g(f(x))=g(f(y)) => f(x)=f(y)
Detach, 207, 208
210 f(x)=f(y)
Detach, 209, 183
211 ALL(a):ALL(b):[Set(a) & Set(b) &
ALL(c):[c e a => f(c) e b]
=>
[Injection(f,a,b) <=>
ALL(c):ALL(d):[c e a & d e a => [f(c)=f(d) =>
c=d]]]]
U Spec, 1
212 ALL(b):[Set(t) & Set(b) & ALL(c):[c e t => f(c) e b]
=> [Injection(f,t,b) <=> ALL(c):ALL(d):[c e t & d e t => [f(c)=f(d) => c=d]]]]
U Spec, 211
213 Set(t) & Set(u) &
ALL(c):[c e t => f(c) e u]
=>
[Injection(f,t,u) <=>
ALL(c):ALL(d):[c e t & d e t => [f(c)=f(d) => c=d]]]
U Spec, 212
214 Set(t) & Set(u)
Join, 5, 6
215 Set(t) & Set(u) &
ALL(a):[a e t => f(a) e u]
Join, 214, 12
216 Injection(f,t,u) <=>
ALL(c):ALL(d):[c e t & d e t => [f(c)=f(d) => c=d]]
Detach, 213, 215
217 [Injection(f,t,u) => ALL(c):ALL(d):[c e t & d e t => [f(c)=f(d) => c=d]]]
&
[ALL(c):ALL(d):[c e t & d e t => [f(c)=f(d) => c=d]] => Injection(f,t,u)]
Iff-And, 216
218 Injection(f,t,u) =>
ALL(c):ALL(d):[c e t & d e t => [f(c)=f(d) => c=d]]
Split, 217
219 ALL(c):ALL(d):[c e t & d e t => [f(c)=f(d) => c=d]]
Detach, 218, 153
220 ALL(d):[x e t & d e t => [f(x)=f(d) => x=d]]
U Spec, 219
221 x e t & y e t => [f(x)=f(y) => x=y]
U Spec, 220
222 f(x)=f(y) => x=y
Detach, 221, 174
223 x=y
Detach, 222, 210
As Required:
224 h(x)=h(y) => x=y
4 Conclusion, 177
As Required:
225 ALL(a):ALL(b):[a e t & b e t => [h(a)=h(b) => a=b]]
4 Conclusion, 174
226 Injection(h,t,v)
Detach, 173, 225
Apply definition of Surjection
227 ALL(a):ALL(b):[Set(a) & Set(b) &
ALL(c):[c e a => h(c) e b]
=>
[Surjection(h,a,b) <=>
ALL(c):[c e b => EXIST(d):[d e a & h(d)=c]]]]
U Spec, 2
228 ALL(b):[Set(t) & Set(b) & ALL(c):[c e t => h(c) e b]
=>
[Surjection(h,t,b) <=>
ALL(c):[c e b => EXIST(d):[d e t & h(d)=c]]]]
U Spec, 227
229 Set(t) & Set(v) &
ALL(c):[c e t => h(c) e v]
=>
[Surjection(h,t,v) <=>
ALL(c):[c e v => EXIST(d):[d e t & h(d)=c]]]
U Spec, 228
230 Set(t) & Set(v)
Join, 5, 7
231 Set(t) & Set(v) &
ALL(a):[a e t => h(a) e v]
Join, 230, 109
232 Surjection(h,t,v) <=>
ALL(c):[c e v => EXIST(d):[d e t & h(d)=c]]
Detach, 229, 231
233 [Surjection(h,t,v) =>
ALL(c):[c e v => EXIST(d):[d e t & h(d)=c]]]
&
[ALL(c):[c e v =>
EXIST(d):[d e t & h(d)=c]] => Surjection(h,t,v)]
Iff-And, 232
Sufficient: For Surjection(h,t,v)
234 ALL(c):[c e v =>
EXIST(d):[d e t & h(d)=c]] => Surjection(h,t,v)
Split, 233
Prove: ALL(c):[c e v => EXIST(d):[d e t &
h(d)=c]]
Suppose...
235 x e v
Premise
236 ALL(a):ALL(b):[Set(a) & Set(b) &
ALL(c):[c e a => g(c) e b]
=>
[Surjection(g,a,b) <=>
ALL(c):[c e b => EXIST(d):[d e a & g(d)=c]]]]
U Spec, 2
237 ALL(b):[Set(u) & Set(b) & ALL(c):[c e u => g(c) e b]
=>
[Surjection(g,u,b) <=>
ALL(c):[c e b => EXIST(d):[d e u & g(d)=c]]]]
U Spec, 236
238 Set(u) & Set(v) &
ALL(c):[c e u => g(c) e v]
=>
[Surjection(g,u,v) <=>
ALL(c):[c e v => EXIST(d):[d e u & g(d)=c]]]
U Spec, 237
239 Set(u) & Set(v)
Join, 6, 7
240 Set(u) & Set(v) &
ALL(a):[a e u => g(a) e v]
Join, 239, 15
241 Surjection(g,u,v) <=>
ALL(c):[c e v => EXIST(d):[d e u & g(d)=c]]
Detach, 238, 240
242 [Surjection(g,u,v) =>
ALL(c):[c e v => EXIST(d):[d e u & g(d)=c]]]
&
[ALL(c):[c e v =>
EXIST(d):[d e u & g(d)=c]] => Surjection(g,u,v)]
Iff-And, 241
243 Surjection(g,u,v) =>
ALL(c):[c e v => EXIST(d):[d e u & g(d)=c]]
Split, 242
244 ALL(c):[c e v =>
EXIST(d):[d e u & g(d)=c]]
Detach, 243, 165
245 x e v => EXIST(d):[d e u & g(d)=x]
U Spec, 244
246 EXIST(d):[d e u & g(d)=x]
Detach, 245, 235
247 y e u & g(y)=x
E Spec, 246
Define: y
pre-image of x under y
248 y e u
Split, 247
249 g(y)=x
Split, 247
250 ALL(a):ALL(b):[Set(a) & Set(b) &
ALL(c):[c e a => f(c) e b]
=>
[Surjection(f,a,b) <=>
ALL(c):[c e b => EXIST(d):[d e a & f(d)=c]]]]
U Spec, 2
251 ALL(b):[Set(t) & Set(b) & ALL(c):[c e t => f(c) e b]
=>
[Surjection(f,t,b) <=>
ALL(c):[c e b => EXIST(d):[d e t & f(d)=c]]]]
U Spec, 250
252 Set(t) & Set(u) &
ALL(c):[c e t => f(c) e u]
=>
[Surjection(f,t,u) <=>
ALL(c):[c e u => EXIST(d):[d e t & f(d)=c]]]
U Spec, 251
253 Set(t) & Set(u)
Join, 5, 6
254 Set(t) & Set(u) &
ALL(a):[a e t => f(a) e u]
Join, 253, 12
255 Surjection(f,t,u) <=>
ALL(c):[c e u => EXIST(d):[d e t & f(d)=c]]
Detach, 252, 254
256 [Surjection(f,t,u) =>
ALL(c):[c e u => EXIST(d):[d e t & f(d)=c]]]
& [ALL(c):[c e u => EXIST(d):[d e t & f(d)=c]] =>
Surjection(f,t,u)]
Iff-And, 255
257 Surjection(f,t,u) =>
ALL(c):[c e u => EXIST(d):[d e t & f(d)=c]]
Split, 256
258 ALL(c):[c e u =>
EXIST(d):[d e t & f(d)=c]]
Detach, 257, 154
259 y e u => EXIST(d):[d e t & f(d)=y]
U Spec, 258
260 EXIST(d):[d e t & f(d)=y]
Detach, 259, 248
261 z e t & f(z)=y
E Spec, 260
Define: z
pre-image of y under f
262 z e t
Split, 261
263 f(z)=y
Split, 261
264 z e t => h(z)=g(f(z))
U Spec, 135
265 h(z)=g(f(z))
Detach, 264, 262
266 z e t & h(z)=g(f(z))
Join, 262, 265
267 z e t & h(z)=g(y)
Substitute, 263,
266
268 z e t & h(z)=x
Substitute, 249,
267
269 EXIST(d):[d e t & h(d)=x]
E Gen, 268
As Required:
270 ALL(c):[c e v =>
EXIST(d):[d e t & h(d)=c]]
4 Conclusion, 235
271 Surjection(h,t,v)
Detach, 234, 270
272 Injection(h,t,v) &
Surjection(h,t,v)
Join, 226, 271
273 Bijection(h,t,v)
Detach, 143, 272
As Required:
274 EXIST(f):[ALL(a):[a e t => f(a) e u] & Bijection(f,t,u)]
&
EXIST(f):[ALL(a):[a e u => f(a) e v] & Bijection(f,u,v)]
=>
EXIST(h):Bijection(h,t,v)
4 Conclusion, 8
As Required:
275 ALL(t):ALL(u):ALL(v):[Set(t) & Set(u)
& Set(v)
=>
[EXIST(f):[ALL(a):[a e t => f(a) e u] & Bijection(f,t,u)]
&
EXIST(f):[ALL(a):[a e u => f(a) e v] & Bijection(f,u,v)]
=>
EXIST(h):Bijection(h,t,v)]]
4 Conclusion, 4