THEOREM
-------
By Dan Christensen
http://www.dcproof.com
A function is invertible iff it is injective (1-to-1)
ALL(a):ALL(b):[Set(a) & Set(b)
=> ALL(f):[Function(f,a,b)
=> [Invertible(f,a,b) <=> OneToOne(f,a,b)]]]
where
Set(a) means a is a set
Function(f,a,b) means f is a function mapping set a to set b
Invertible(f,a,b) means f is an invertible function mapping set a to set b
OneToOne(f,a,b) means f is a 1-to-1 (injective) function mapping set a to set b
OUTLINE
-------
Let f be a function mapping set p to set q. Let rng be the range of f. We begin by assuming f is invertible.
Applying the definitions we show by direct proof that f must then be OneToOne.
Then we assume is OneToOne and prove that f must be invertible. We do this by constructing a set of ordered
pairs g={(a,b)|a=f(b)}. We then show by direct proof that g is a function and that it is the required inverse of f.
DEFINITIONS/AXIOMS
------------------
Define: Function
1 ALL(f):ALL(a):ALL(b):[Function(f,a,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(d):ALL(e):[c e a & d e b & e e b => [(c,d) e f & (c,e) e f => d=e]]]
Axiom
Functional notation
2 ALL(f):ALL(a):ALL(b):[Function(f,a,b) => ALL(c):ALL(d):[c e a & d e b => [f(c)=d <=> (c,d) e f]]]
Axiom
3 ALL(f):ALL(a):ALL(b):[Function(f,a,b)
=> ALL(c):[c e a => f(c) e b]]
Axiom
Define: OneToOne
4 ALL(f):ALL(a):ALL(b):[Function(f,a,b) => [OneToOne(f,a,b)
<=> ALL(c):ALL(d):[c e a & d e a => [f(c)=f(d) => c=d]]]]
Axiom
Define: Invertible
5 ALL(f):ALL(a):ALL(b):ALL(c):[Function(f,a,b) & ALL(d):[d e c <=> d e b & EXIST(e):[e e a & f(e)=d]] => [Invertible(f,a,b)
<=> EXIST(g):[ALL(d):[d e c => g(d) e a] & ALL(d):ALL(e):[d e a & e e c => [f(d)=e <=> g(e)=d]]]]]
Axiom
PROOF
-----
Prove: ALL(a):ALL(b):[Set(a) & Set(b)
=> ALL(f):[Function(f,a,b)
=> [Invertible(f,a,b) <=> OneToOne(f,a,b)]]]
Suppose...
6 Set(p) & Set(q)
Premise
7 Set(p)
Split, 6
8 Set(q)
Split, 6
Suppose...
9 Function(f,p,q)
Premise
Apply definition of function notation
10 ALL(a):ALL(b):[Function(f,a,b)
=> ALL(c):[c e a => f(c) e b]]
U Spec, 3
11 ALL(b):[Function(f,p,b)
=> ALL(c):[c e p => f(c) e b]]
U Spec, 10
12 Function(f,p,q)
=> ALL(c):[c e p => f(c) e q]
U Spec, 11
13 ALL(c):[c e p => f(c) e q]
Detach, 12, 9
Apply definition of function notation
14 ALL(a):ALL(b):[Function(f,a,b) => ALL(c):ALL(d):[c e a & d e b => [f(c)=d <=> (c,d) e f]]]
U Spec, 2
15 ALL(b):[Function(f,p,b) => ALL(c):ALL(d):[c e p & d e b => [f(c)=d <=> (c,d) e f]]]
U Spec, 14
16 Function(f,p,q) => ALL(c):ALL(d):[c e p & d e q => [f(c)=d <=> (c,d) e f]]
U Spec, 15
17 ALL(c):ALL(d):[c e p & d e q => [f(c)=d <=> (c,d) e f]]
Detach, 16, 9
Construct range of f
Apply Subset Axiom
18 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e q & EXIST(b):[b e p & f(b)=a]]]
Subset, 8
19 Set(rng) & ALL(a):[a e rng <=> a e q & EXIST(b):[b e p & f(b)=a]]
E Spec, 18
Define: rng (the range of f)
20 Set(rng)
Split, 19
21 ALL(a):[a e rng <=> a e q & EXIST(b):[b e p & f(b)=a]]
Split, 19
Apply definition of OneToOne
22 ALL(a):ALL(b):[Function(f,a,b) => [OneToOne(f,a,b)
<=> ALL(c):ALL(d):[c e a & d e a => [f(c)=f(d) => c=d]]]]
U Spec, 4
23 ALL(b):[Function(f,p,b) => [OneToOne(f,p,b)
<=> ALL(c):ALL(d):[c e p & d e p => [f(c)=f(d) => c=d]]]]
U Spec, 22
24 Function(f,p,q) => [OneToOne(f,p,q)
<=> ALL(c):ALL(d):[c e p & d e p => [f(c)=f(d) => c=d]]]
U Spec, 23
25 OneToOne(f,p,q)
<=> ALL(c):ALL(d):[c e p & d e p => [f(c)=f(d) => c=d]]
Detach, 24, 9
Apply definition of Invertible
26 ALL(a):ALL(b):ALL(c):[Function(f,a,b) & ALL(d):[d e c <=> d e b & EXIST(e):[e e a & f(e)=d]] => [Invertible(f,a,b)
<=> EXIST(g):[ALL(d):[d e c => g(d) e a] & ALL(d):ALL(e):[d e a & e e c => [f(d)=e <=> g(e)=d]]]]]
U Spec, 5
27 ALL(b):ALL(c):[Function(f,p,b) & ALL(d):[d e c <=> d e b & EXIST(e):[e e p & f(e)=d]] => [Invertible(f,p,b)
<=> EXIST(g):[ALL(d):[d e c => g(d) e p] & ALL(d):ALL(e):[d e p & e e c => [f(d)=e <=> g(e)=d]]]]]
U Spec, 26
28 ALL(c):[Function(f,p,q) & ALL(d):[d e c <=> d e q & EXIST(e):[e e p & f(e)=d]] => [Invertible(f,p,q)
<=> EXIST(g):[ALL(d):[d e c => g(d) e p] & ALL(d):ALL(e):[d e p & e e c => [f(d)=e <=> g(e)=d]]]]]
U Spec, 27
29 Function(f,p,q) & ALL(d):[d e rng <=> d e q & EXIST(e):[e e p & f(e)=d]] => [Invertible(f,p,q)
<=> EXIST(g):[ALL(d):[d e rng => g(d) e p] & ALL(d):ALL(e):[d e p & e e rng => [f(d)=e <=> g(e)=d]]]]
U Spec, 28
30 Function(f,p,q)
& ALL(a):[a e rng <=> a e q & EXIST(b):[b e p & f(b)=a]]
Join, 9, 21
31 Invertible(f,p,q)
<=> EXIST(g):[ALL(d):[d e rng => g(d) e p] & ALL(d):ALL(e):[d e p & e e rng => [f(d)=e <=> g(e)=d]]]
Detach, 29, 30
'=>'
Prove: Invertible(f,p,q) => OneToOne(f,p,q)
Suppose...
32 Invertible(f,p,q)
Premise
Apply definition of Invertible
33 [Invertible(f,p,q) => EXIST(g):[ALL(d):[d e rng => g(d) e p] & ALL(d):ALL(e):[d e p & e e rng => [f(d)=e <=> g(e)=d]]]]
& [EXIST(g):[ALL(d):[d e rng => g(d) e p] & ALL(d):ALL(e):[d e p & e e rng => [f(d)=e <=> g(e)=d]]] => Invertible(f,p,q)]
Iff-And, 31
34 Invertible(f,p,q) => EXIST(g):[ALL(d):[d e rng => g(d) e p] & ALL(d):ALL(e):[d e p & e e rng => [f(d)=e <=> g(e)=d]]]
Split, 33
35 EXIST(g):[ALL(d):[d e rng => g(d) e p] & ALL(d):ALL(e):[d e p & e e rng => [f(d)=e <=> g(e)=d]]] => Invertible(f,p,q)
Split, 33
36 EXIST(g):[ALL(d):[d e rng => g(d) e p] & ALL(d):ALL(e):[d e p & e e rng => [f(d)=e <=> g(e)=d]]]
Detach, 34, 32
37 ALL(d):[d e rng => g(d) e p] & ALL(d):ALL(e):[d e p & e e rng => [f(d)=e <=> g(e)=d]]
E Spec, 36
Define: g (the inverse of f)
38 ALL(d):[d e rng => g(d) e p]
Split, 37
39 ALL(d):ALL(e):[d e p & e e rng => [f(d)=e <=> g(e)=d]]
Split, 37
Apply definition of OneToOne
40 [OneToOne(f,p,q) => ALL(c):ALL(d):[c e p & d e p => [f(c)=f(d) => c=d]]]
& [ALL(c):ALL(d):[c e p & d e p => [f(c)=f(d) => c=d]] => OneToOne(f,p,q)]
Iff-And, 25
41 OneToOne(f,p,q) => ALL(c):ALL(d):[c e p & d e p => [f(c)=f(d) => c=d]]
Split, 40
Sufficient: For OneToOne(f,p,q)
42 ALL(c):ALL(d):[c e p & d e p => [f(c)=f(d) => c=d]] => OneToOne(f,p,q)
Split, 40
Prove: ALL(c):ALL(d):[c e p & d e p => [f(c)=f(d) => c=d]]
Suppose...
43 x e p & y e p
Premise
44 x e p
Split, 43
45 y e p
Split, 43
Prove: f(x)=f(y) => x=y
f(x) and f(y) are in the range of f (i.e. the domain of g). By definiton of g, g(f(x))=x and g(f(y))=y.
If f(x)=f(y), then, but substitution we must have x=y.
Suppose...
46 f(x)=f(y)
Premise
Prove: f(x) e rng
Apply definition of rng
47 f(x) e rng <=> f(x) e q & EXIST(b):[b e p & f(b)=f(x)]
U Spec, 21
48 [f(x) e rng => f(x) e q & EXIST(b):[b e p & f(b)=f(x)]]
& [f(x) e q & EXIST(b):[b e p & f(b)=f(x)] => f(x) e rng]
Iff-And, 47
49 f(x) e rng => f(x) e q & EXIST(b):[b e p & f(b)=f(x)]
Split, 48
Sufficient: f(x) e rng
50 f(x) e q & EXIST(b):[b e p & f(b)=f(x)] => f(x) e rng
Split, 48
Apply definition of f
51 x e p => f(x) e q
U Spec, 13
52 f(x) e q
Detach, 51, 44
53 f(x)=f(x)
Reflex
54 x e p & f(x)=f(x)
Join, 44, 53
55 EXIST(b):[b e p & f(b)=f(x)]
E Gen, 54
56 f(x) e q & EXIST(b):[b e p & f(b)=f(x)]
Join, 52, 55
As Required:
57 f(x) e rng
Detach, 50, 56
Prove: f(y) e rng
Apply definition of rng
58 f(y) e rng <=> f(y) e q & EXIST(b):[b e p & f(b)=f(y)]
U Spec, 21
59 [f(y) e rng => f(y) e q & EXIST(b):[b e p & f(b)=f(y)]]
& [f(y) e q & EXIST(b):[b e p & f(b)=f(y)] => f(y) e rng]
Iff-And, 58
60 f(y) e rng => f(y) e q & EXIST(b):[b e p & f(b)=f(y)]
Split, 59
Sufficient: For f(y) e rng
61 f(y) e q & EXIST(b):[b e p & f(b)=f(y)] => f(y) e rng
Split, 59
62 y e p => f(y) e q
U Spec, 13
63 f(y) e q
Detach, 62, 45
64 f(y)=f(y)
Reflex
65 y e p & f(y)=f(y)
Join, 45, 64
66 EXIST(b):[b e p & f(b)=f(y)]
E Gen, 65
67 f(y) e q & EXIST(b):[b e p & f(b)=f(y)]
Join, 63, 66
As Required:
68 f(y) e rng
Detach, 61, 67
Prove: g(f(x))=x
Apply definition of g
69 ALL(e):[x e p & e e rng => [f(x)=e <=> g(e)=x]]
U Spec, 39
70 x e p & f(x) e rng => [f(x)=f(x) <=> g(f(x))=x]
U Spec, 69
71 x e p & f(x) e rng
Join, 44, 57
72 f(x)=f(x) <=> g(f(x))=x
Detach, 70, 71
73 [f(x)=f(x) => g(f(x))=x] & [g(f(x))=x => f(x)=f(x)]
Iff-And, 72
74 f(x)=f(x) => g(f(x))=x
Split, 73
75 g(f(x))=x => f(x)=f(x)
Split, 73
As Required:
76 g(f(x))=x
Detach, 74, 53
Prove: g(f(y))=y
Apply definition of g
77 ALL(e):[y e p & e e rng => [f(y)=e <=> g(e)=y]]
U Spec, 39
78 y e p & f(y) e rng => [f(y)=f(y) <=> g(f(y))=y]
U Spec, 77
79 y e p & f(y) e rng
Join, 45, 68
80 f(y)=f(y) <=> g(f(y))=y
Detach, 78, 79
81 [f(y)=f(y) => g(f(y))=y] & [g(f(y))=y => f(y)=f(y)]
Iff-And, 80
82 f(y)=f(y) => g(f(y))=y
Split, 81
83 g(f(y))=y => f(y)=f(y)
Split, 81
As Required:
84 g(f(y))=y
Detach, 82, 64
85 g(f(x))=y
Substitute, 46, 84
86 x=y
Substitute, 76, 85
As Required:
87 f(x)=f(y) => x=y
4 Conclusion, 46
As Required:
88 ALL(c):ALL(d):[c e p & d e p => [f(c)=f(d) => c=d]]
4 Conclusion, 43
As Required:
89 OneToOne(f,p,q)
Detach, 42, 88
As Required:
90 Invertible(f,p,q) => OneToOne(f,p,q)
4 Conclusion, 32
'<='
Prove: OneToOne(f,s,s) => Invertible(f,s,s)
Suppose...
91 OneToOne(f,p,q)
Premise
Apply definition of OneToOne
92 [OneToOne(f,p,q) => ALL(c):ALL(d):[c e p & d e p => [f(c)=f(d) => c=d]]]
& [ALL(c):ALL(d):[c e p & d e p => [f(c)=f(d) => c=d]] => OneToOne(f,p,q)]
Iff-And, 25
93 OneToOne(f,p,q) => ALL(c):ALL(d):[c e p & d e p => [f(c)=f(d) => c=d]]
Split, 92
94 ALL(c):ALL(d):[c e p & d e p => [f(c)=f(d) => c=d]] => OneToOne(f,p,q)
Split, 92
95 ALL(c):ALL(d):[c e p & d e p => [f(c)=f(d) => c=d]]
Detach, 93, 91
Apply definition of Invertible
96 [Invertible(f,p,q) => EXIST(g):[ALL(d):[d e rng => g(d) e p] & ALL(d):ALL(e):[d e p & e e rng => [f(d)=e <=> g(e)=d]]]]
& [EXIST(g):[ALL(d):[d e rng => g(d) e p] & ALL(d):ALL(e):[d e p & e e rng => [f(d)=e <=> g(e)=d]]] => Invertible(f,p,q)]
Iff-And, 31
97 Invertible(f,p,q) => EXIST(g):[ALL(d):[d e rng => g(d) e p] & ALL(d):ALL(e):[d e p & e e rng => [f(d)=e <=> g(e)=d]]]
Split, 96
Sufficient: For Invertible(f,p,q)
98 EXIST(g):[ALL(d):[d e rng => g(d) e p] & ALL(d):ALL(e):[d e p & e e rng => [f(d)=e <=> g(e)=d]]] => Invertible(f,p,q)
Split, 96
Construct the Cartesian product of rng and p.
Apply the Cartesian Product Axiom.
99 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
100 ALL(a2):[Set(rng) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e rng & c2 e a2]]]
U Spec, 99
101 Set(rng) & Set(p) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e rng & c2 e p]]
U Spec, 100
102 Set(rng) & Set(p)
Join, 20, 7
103 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e rng & c2 e p]]
Detach, 101, 102
104 Set'(rp) & ALL(c1):ALL(c2):[(c1,c2) e rp <=> c1 e rng & c2 e p]
E Spec, 103
Define: rp (the Cartesian product of rng and p)
105 Set'(rp)
Split, 104
106 ALL(c1):ALL(c2):[(c1,c2) e rp <=> c1 e rng & c2 e p]
Split, 104
Construct subset g of rp
107 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e rp & a=f(b)]]
Subset, 105
108 Set'(g) & ALL(a):ALL(b):[(a,b) e g <=> (a,b) e rp & a=f(b)]
E Spec, 107
Define: g (will be shown to be the required inverse function of f)
109 Set'(g)
Split, 108
110 ALL(a):ALL(b):[(a,b) e g <=> (a,b) e rp & a=f(b)]
Split, 108
Apply definition of Function
111 ALL(a):ALL(b):[Function(g,a,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(d):ALL(e):[c e a & d e b & e e b => [(c,d) e g & (c,e) e g => d=e]]]
U Spec, 1
112 ALL(b):[Function(g,rng,b)
<=> ALL(c):ALL(d):[(c,d) e g => c e rng & d e b]
& ALL(c):[c e rng => EXIST(d):[d e b & (c,d) e g]]
& ALL(c):ALL(d):ALL(e):[c e rng & d e b & e e b => [(c,d) e g & (c,e) e g => d=e]]]
U Spec, 111
113 Function(g,rng,p)
<=> ALL(c):ALL(d):[(c,d) e g => c e rng & d e p]
& ALL(c):[c e rng => EXIST(d):[d e p & (c,d) e g]]
& ALL(c):ALL(d):ALL(e):[c e rng & d e p & e e p => [(c,d) e g & (c,e) e g => d=e]]
U Spec, 112
114 [Function(g,rng,p) => ALL(c):ALL(d):[(c,d) e g => c e rng & d e p]
& ALL(c):[c e rng => EXIST(d):[d e p & (c,d) e g]]
& ALL(c):ALL(d):ALL(e):[c e rng & d e p & e e p => [(c,d) e g & (c,e) e g => d=e]]]
& [ALL(c):ALL(d):[(c,d) e g => c e rng & d e p]
& ALL(c):[c e rng => EXIST(d):[d e p & (c,d) e g]]
& ALL(c):ALL(d):ALL(e):[c e rng & d e p & e e p => [(c,d) e g & (c,e) e g => d=e]] => Function(g,rng,p)]
Iff-And, 113
115 Function(g,rng,p) => ALL(c):ALL(d):[(c,d) e g => c e rng & d e p]
& ALL(c):[c e rng => EXIST(d):[d e p & (c,d) e g]]
& ALL(c):ALL(d):ALL(e):[c e rng & d e p & e e p => [(c,d) e g & (c,e) e g => d=e]]
Split, 114
Sufficient: For Function(g,rng,p)
116 ALL(c):ALL(d):[(c,d) e g => c e rng & d e p]
& ALL(c):[c e rng => EXIST(d):[d e p & (c,d) e g]]
& ALL(c):ALL(d):ALL(e):[c e rng & d e p & e e p => [(c,d) e g & (c,e) e g => d=e]] => Function(g,rng,p)
Split, 114
Prove: ALL(c):ALL(d):[(c,d) e g => c e rng & d e p]
Suppose...
117 (x,y) e g
Premise
Apply definition of g
118 ALL(b):[(x,b) e g <=> (x,b) e rp & x=f(b)]
U Spec, 110
119 (x,y) e g <=> (x,y) e rp & x=f(y)
U Spec, 118
120 [(x,y) e g => (x,y) e rp & x=f(y)]
& [(x,y) e rp & x=f(y) => (x,y) e g]
Iff-And, 119
121 (x,y) e g => (x,y) e rp & x=f(y)
Split, 120
122 (x,y) e rp & x=f(y) => (x,y) e g
Split, 120
123 (x,y) e rp & x=f(y)
Detach, 121, 117
124 (x,y) e rp
Split, 123
125 x=f(y)
Split, 123
Apply definition of rp
126 ALL(c2):[(x,c2) e rp <=> x e rng & c2 e p]
U Spec, 106
127 (x,y) e rp <=> x e rng & y e p
U Spec, 126
128 [(x,y) e rp => x e rng & y e p]
& [x e rng & y e p => (x,y) e rp]
Iff-And, 127
129 (x,y) e rp => x e rng & y e p
Split, 128
130 x e rng & y e p => (x,y) e rp
Split, 128
131 x e rng & y e p
Detach, 129, 124
As Required:
132 ALL(c):ALL(d):[(c,d) e g => c e rng & d e p]
4 Conclusion, 117
Prove: ALL(c):[c e rng => EXIST(d):[d e p & (c,d) e g]]
Suppose...
133 x e rng
Premise
Apply definition of rng
134 x e rng <=> x e q & EXIST(b):[b e p & f(b)=x]
U Spec, 21
135 [x e rng => x e q & EXIST(b):[b e p & f(b)=x]]
& [x e q & EXIST(b):[b e p & f(b)=x] => x e rng]
Iff-And, 134
136 x e rng => x e q & EXIST(b):[b e p & f(b)=x]
Split, 135
137 x e q & EXIST(b):[b e p & f(b)=x] => x e rng
Split, 135
138 x e q & EXIST(b):[b e p & f(b)=x]
Detach, 136, 133
139 x e q
Split, 138
140 EXIST(b):[b e p & f(b)=x]
Split, 138
141 y e p & f(y)=x
E Spec, 140
Define: y (the pre-image of x in p under f)
142 y e p
Split, 141
143 f(y)=x
Split, 141
Apply definition of g
144 ALL(b):[(x,b) e g <=> (x,b) e rp & x=f(b)]
U Spec, 110
145 (x,y) e g <=> (x,y) e rp & x=f(y)
U Spec, 144
146 [(x,y) e g => (x,y) e rp & x=f(y)]
& [(x,y) e rp & x=f(y) => (x,y) e g]
Iff-And, 145
147 (x,y) e g => (x,y) e rp & x=f(y)
Split, 146
Sufficient: For (x,y) e g
148 (x,y) e rp & x=f(y) => (x,y) e g
Split, 146
Prove: (x,y) e rp
Apply definition of rp
149 ALL(c2):[(x,c2) e rp <=> x e rng & c2 e p]
U Spec, 106
150 (x,y) e rp <=> x e rng & y e p
U Spec, 149
151 [(x,y) e rp => x e rng & y e p]
& [x e rng & y e p => (x,y) e rp]
Iff-And, 150
152 (x,y) e rp => x e rng & y e p
Split, 151
153 x e rng & y e p => (x,y) e rp
Split, 151
154 x e rng & y e p
Join, 133, 142
As Required:
155 (x,y) e rp
Detach, 153, 154
156 x=f(y)
Sym, 143
157 (x,y) e rp & x=f(y)
Join, 155, 156
158 (x,y) e g
Detach, 148, 157
159 y e p & (x,y) e g
Join, 142, 158
As Required:
160 ALL(c):[c e rng => EXIST(d):[d e p & (c,d) e g]]
4 Conclusion, 133
Prove: ALL(c):ALL(d):ALL(e):[c e rng & d e p & e e p => [(c,d) e g & (c,e) e g => d=e]]
Suppose...
161 x e rng & y e p & z e p
Premise
162 x e rng
Split, 161
163 y e p
Split, 161
164 z e p
Split, 161
Prove: (x,y) e g & (x,z) e g => y=z
Suppose...
165 (x,y) e g & (x,z) e g
Premise
166 (x,y) e g
Split, 165
167 (x,z) e g
Split, 165
Apply definition of g
168 ALL(b):[(x,b) e g <=> (x,b) e rp & x=f(b)]
U Spec, 110
169 (x,y) e g <=> (x,y) e rp & x=f(y)
U Spec, 168
170 [(x,y) e g => (x,y) e rp & x=f(y)]
& [(x,y) e rp & x=f(y) => (x,y) e g]
Iff-And, 169
171 (x,y) e g => (x,y) e rp & x=f(y)
Split, 170
172 (x,y) e rp & x=f(y) => (x,y) e g
Split, 170
173 (x,y) e rp & x=f(y)
Detach, 171, 166
174 (x,y) e rp
Split, 173
175 x=f(y)
Split, 173
176 (x,z) e g <=> (x,z) e rp & x=f(z)
U Spec, 168
177 [(x,z) e g => (x,z) e rp & x=f(z)]
& [(x,z) e rp & x=f(z) => (x,z) e g]
Iff-And, 176
178 (x,z) e g => (x,z) e rp & x=f(z)
Split, 177
179 (x,z) e rp & x=f(z) => (x,z) e g
Split, 177
180 (x,z) e rp & x=f(z)
Detach, 178, 167
181 (x,z) e rp
Split, 180
182 x=f(z)
Split, 180
183 f(y)=f(z)
Substitute, 175, 182
Apply definition of OneToOne
184 ALL(d):[y e p & d e p => [f(y)=f(d) => y=d]]
U Spec, 95
185 y e p & z e p => [f(y)=f(z) => y=z]
U Spec, 184
186 y e p & z e p
Join, 163, 164
187 f(y)=f(z) => y=z
Detach, 185, 186
188 y=z
Detach, 187, 183
As Required:
189 (x,y) e g & (x,z) e g => y=z
4 Conclusion, 165
As Required:
190 ALL(c):ALL(d):ALL(e):[c e rng & d e p & e e p
=> [(c,d) e g & (c,e) e g => d=e]]
4 Conclusion, 161
191 ALL(c):ALL(d):[(c,d) e g => c e rng & d e p]
& ALL(c):[c e rng => EXIST(d):[d e p & (c,d) e g]]
Join, 132, 160
192 ALL(c):ALL(d):[(c,d) e g => c e rng & d e p]
& ALL(c):[c e rng => EXIST(d):[d e p & (c,d) e g]]
& ALL(c):ALL(d):ALL(e):[c e rng & d e p & e e p
=> [(c,d) e g & (c,e) e g => d=e]]
Join, 191, 190
As Required:
193 Function(g,rng,p)
Detach, 116, 192
Apply functional notation
194 ALL(a):ALL(b):[Function(g,a,b) => ALL(c):ALL(d):[c e a & d e b => [g(c)=d <=> (c,d) e g]]]
U Spec, 2
195 ALL(b):[Function(g,rng,b) => ALL(c):ALL(d):[c e rng & d e b => [g(c)=d <=> (c,d) e g]]]
U Spec, 194
196 Function(g,rng,p) => ALL(c):ALL(d):[c e rng & d e p => [g(c)=d <=> (c,d) e g]]
U Spec, 195
197 ALL(c):ALL(d):[c e rng & d e p => [g(c)=d <=> (c,d) e g]]
Detach, 196, 193
198 ALL(a):ALL(b):[Function(g,a,b)
=> ALL(c):[c e a => g(c) e b]]
U Spec, 3
199 ALL(b):[Function(g,rng,b)
=> ALL(c):[c e rng => g(c) e b]]
U Spec, 198
200 Function(g,rng,p)
=> ALL(c):[c e rng => g(c) e p]
U Spec, 199
201 ALL(c):[c e rng => g(c) e p]
Detach, 200, 193
Prove: ALL(d):ALL(e):[d e p & e e rng => [f(d)=e <=> g(e)=d]]
Suppose...
202 x e p & y e rng
Premise
203 x e p
Split, 202
204 y e rng
Split, 202
'=>'
Prove: f(x)=y => g(y)=x
Suppose...
205 f(x)=y
Premise
Apply definition of g
206 ALL(b):[(y,b) e g <=> (y,b) e rp & y=f(b)]
U Spec, 110
207 (y,x) e g <=> (y,x) e rp & y=f(x)
U Spec, 206
208 [(y,x) e g => (y,x) e rp & y=f(x)]
& [(y,x) e rp & y=f(x) => (y,x) e g]
Iff-And, 207
209 (y,x) e g => (y,x) e rp & y=f(x)
Split, 208
Sufficient: For (y,x) e g
210 (y,x) e rp & y=f(x) => (y,x) e g
Split, 208
Prove: (y,x) e rp
Apply definition of rp
211 ALL(c2):[(y,c2) e rp <=> y e rng & c2 e p]
U Spec, 106
212 (y,x) e rp <=> y e rng & x e p
U Spec, 211
213 [(y,x) e rp => y e rng & x e p]
& [y e rng & x e p => (y,x) e rp]
Iff-And, 212
214 (y,x) e rp => y e rng & x e p
Split, 213
215 y e rng & x e p => (y,x) e rp
Split, 213
216 y e rng & x e p
Join, 204, 203
As Required:
217 (y,x) e rp
Detach, 215, 216
218 y=f(x)
Sym, 205
219 (y,x) e rp & y=f(x)
Join, 217, 218
220 (y,x) e g
Detach, 210, 219
Prove: g(y)=x
Apply functionality of g
221 ALL(d):[y e rng & d e p => [g(y)=d <=> (y,d) e g]]
U Spec, 197
222 y e rng & x e p => [g(y)=x <=> (y,x) e g]
U Spec, 221
223 g(y)=x <=> (y,x) e g
Detach, 222, 216
224 [g(y)=x => (y,x) e g] & [(y,x) e g => g(y)=x]
Iff-And, 223
225 g(y)=x => (y,x) e g
Split, 224
226 (y,x) e g => g(y)=x
Split, 224
As Required:
227 g(y)=x
Detach, 226, 220
As Required:
228 f(x)=y => g(y)=x
4 Conclusion, 205
'<='
Prove: g(y)=x => f(x)=y
Suppose...
229 g(y)=x
Premise
Apply definition of g
230 ALL(b):[(y,b) e g <=> (y,b) e rp & y=f(b)]
U Spec, 110
231 (y,x) e g <=> (y,x) e rp & y=f(x)
U Spec, 230
232 [(y,x) e g => (y,x) e rp & y=f(x)]
& [(y,x) e rp & y=f(x) => (y,x) e g]
Iff-And, 231
233 (y,x) e g => (y,x) e rp & y=f(x)
Split, 232
234 (y,x) e rp & y=f(x) => (y,x) e g
Split, 232
235 ALL(d):[y e rng & d e p => [g(y)=d <=> (y,d) e g]]
U Spec, 197
236 y e rng & x e p => [g(y)=x <=> (y,x) e g]
U Spec, 235
237 y e rng & x e p
Join, 204, 203
238 g(y)=x <=> (y,x) e g
Detach, 236, 237
239 [g(y)=x => (y,x) e g] & [(y,x) e g => g(y)=x]
Iff-And, 238
240 g(y)=x => (y,x) e g
Split, 239
241 (y,x) e g => g(y)=x
Split, 239
242 (y,x) e g
Detach, 240, 229
243 (y,x) e rp & y=f(x)
Detach, 233, 242
244 (y,x) e rp
Split, 243
245 y=f(x)
Split, 243
246 f(x)=y
Sym, 245
As Required:
247 g(y)=x => f(x)=y
4 Conclusion, 229
248 [f(x)=y => g(y)=x] & [g(y)=x => f(x)=y]
Join, 228, 247
249 f(x)=y <=> g(y)=x
Iff-And, 248
As Required:
250 ALL(d):ALL(e):[d e p & e e rng => [f(d)=e <=> g(e)=d]]
4 Conclusion, 202
251 ALL(c):[c e rng => g(c) e p]
& ALL(d):ALL(e):[d e p & e e rng => [f(d)=e <=> g(e)=d]]
Join, 201, 250
252 EXIST(g):[ALL(c):[c e rng => g(c) e p]
& ALL(d):ALL(e):[d e p & e e rng => [f(d)=e <=> g(e)=d]]]
E Gen, 251
253 Invertible(f,p,q)
Detach, 98, 252
As Required:
254 OneToOne(f,p,q) => Invertible(f,p,q)
4 Conclusion, 91
255 [Invertible(f,p,q) => OneToOne(f,p,q)]
& [OneToOne(f,p,q) => Invertible(f,p,q)]
Join, 90, 254
256 Invertible(f,p,q) <=> OneToOne(f,p,q)
Iff-And, 255
257 ALL(f):[Function(f,p,q)
=> [Invertible(f,p,q) <=> OneToOne(f,p,q)]]
4 Conclusion, 9
As Required:
258 ALL(a):ALL(b):[Set(a) & Set(b)
=> ALL(f):[Function(f,a,b)
=> [Invertible(f,a,b) <=> OneToOne(f,a,b)]]]
4 Conclusion, 6