THEOREM
*******
Inverses of functions are bijections (injective and surjective)
ALL(set1):ALL(set2):ALL(func):ALL(inv):[Set(set1) & Set(set2)
& ALL(a):[a e set1 => func(a) e set2]
& ALL(a):[a e set2 => inv(a) e set1]
& ALL(a):ALL(b):[a e set1 & b e set2 => [inv(b)=a <=> func(a)=b]]
=> ALL(a):ALL(b):[a e set2 & b e set2 => [inv(a)=inv(b) => a=b]]
& ALL(a):[a e set1 => EXIST(b):[b e set2 & inv(b)=a]]]
PROOF
*****
1 Set(x) & Set(y)
& ALL(a):[a e x => f(a) e y]
& ALL(a):[a e y => f'(a) e x]
& ALL(a):ALL(b):[a e x & b e y => [f'(b)=a <=> f(a)=b]]
Premise
2 Set(x)
Split, 1
3 Set(y)
Split, 1
f maps elements of x to elements of y
4 ALL(a):[a e x => f(a) e y]
Split, 1
f' is the inverse of f
5 ALL(a):[a e y => f'(a) e x]
Split, 1
6 ALL(a):ALL(b):[a e x & b e y => [f'(b)=a <=> f(a)=b]]
Split, 1
Prove: ALL(a):ALL(b):[a e y & b e y => [f'(a)=f'(b) => a=b]]
Suppose...
7 p e y & q e y
Premise
8 p e y
Split, 7
9 q e y
Split, 7
Prove: f'(p)=f'(q) => p=q
Suppose...
10 f'(p)=f'(q)
Premise
11 ALL(b):[f'(q) e x & b e y => [f'(b)=f'(q) <=> f(f'(q))=b]]
U Spec, 6
12 f'(q) e x & p e y => [f'(p)=f'(q) <=> f(f'(q))=p]
U Spec, 11
13 q e y => f'(q) e x
U Spec, 5
14 f'(q) e x
Detach, 13, 9
15 f'(q) e x & p e y
Join, 14, 8
16 f'(p)=f'(q) <=> f(f'(q))=p
Detach, 12, 15
17 [f'(p)=f'(q) => f(f'(q))=p]
& [f(f'(q))=p => f'(p)=f'(q)]
Iff-And, 16
18 f'(p)=f'(q) => f(f'(q))=p
Split, 17
19 f(f'(q))=p => f'(p)=f'(q)
Split, 17
20 f(f'(q))=p
Detach, 18, 10
21 ALL(b):[f'(q) e x & b e y => [f'(b)=f'(q) <=> f(f'(q))=b]]
U Spec, 6
22 f'(q) e x & q e y => [f'(q)=f'(q) <=> f(f'(q))=q]
U Spec, 21
23 f'(q) e x & q e y
Join, 14, 9
24 f'(q)=f'(q) <=> f(f'(q))=q
Detach, 22, 23
25 [f'(q)=f'(q) => f(f'(q))=q]
& [f(f'(q))=q => f'(q)=f'(q)]
Iff-And, 24
26 f'(q)=f'(q) => f(f'(q))=q
Split, 25
27 f(f'(q))=q => f'(q)=f'(q)
Split, 25
28 f'(q)=f'(q)
Reflex
29 f(f'(q))=q
Detach, 26, 28
30 p=q
Substitute, 20, 29
As Required:
31 f'(p)=f'(q) => p=q
4 Conclusion, 10
As Required:
32 ALL(a):ALL(b):[a e y & b e y => [f'(a)=f'(b) => a=b]]
4 Conclusion, 7
Prove: ALL(a):[a e x => EXIST(b):[b e y & f'(b)=a]]
Suppose...
33 p e x
Premise
34 p e x => f(p) e y
U Spec, 4
35 f(p) e y
Detach, 34, 33
36 ALL(b):[p e x & b e y => [f'(b)=p <=> f(p)=b]]
U Spec, 6
37 p e x & f(p) e y => [f'(f(p))=p <=> f(p)=f(p)]
U Spec, 36
38 p e x & f(p) e y
Join, 33, 35
39 f'(f(p))=p <=> f(p)=f(p)
Detach, 37, 38
40 [f'(f(p))=p => f(p)=f(p)] & [f(p)=f(p) => f'(f(p))=p]
Iff-And, 39
41 f'(f(p))=p => f(p)=f(p)
Split, 40
42 f(p)=f(p) => f'(f(p))=p
Split, 40
43 f(p)=f(p)
Reflex
44 f'(f(p))=p
Detach, 42, 43
45 f(p) e y & f'(f(p))=p
Join, 35, 44
46 EXIST(b):[b e y & f'(b)=p]
E Gen, 45
As Required:
47 ALL(a):[a e x => EXIST(b):[b e y & f'(b)=a]]
4 Conclusion, 33
48 ALL(a):ALL(b):[a e y & b e y => [f'(a)=f'(b) => a=b]]
& ALL(a):[a e x => EXIST(b):[b e y & f'(b)=a]]
Join, 32, 47
As Required:
49 ALL(set1):ALL(set2):ALL(func):ALL(inv):[Set(set1) & Set(set2)
& ALL(a):[a e set1 => func(a) e set2]
& ALL(a):[a e set2 => inv(a) e set1]
& ALL(a):ALL(b):[a e set1 & b e set2 => [inv(b)=a <=> func(a)=b]]
=> ALL(a):ALL(b):[a e set2 & b e set2 => [inv(a)=inv(b) => a=b]]
& ALL(a):[a e set1 => EXIST(b):[b e set2 & inv(b)=a]]]
4 Conclusion, 1