Existence of Inverse Functions

THEOREM

*******

If a function is surjective and injection, then it has an inverse.

ALL(x):ALL(y):ALL(f):[Set(x) & Set(y)

& ALL(a):[a e x => f(a) e y]

& ALL(a):[a e y => EXIST(b):[b e x & f(b)=a]]

& ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]

=> EXIST(f'):[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]]]]

PROOF

*****

Suppose...

1 Set(x) & Set(y)

& ALL(a):[a e x => f(a) e y]

& ALL(a):[a e y => EXIST(b):[b e x & f(b)=a]]

& ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]

Premise

2 Set(x)

Split, 1

3 Set(y)

Split, 1

4 ALL(a):[a e x => f(a) e y]

Split, 1

5 ALL(a):[a e y => EXIST(b):[b e x & f(b)=a]]

Split, 1

6 ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]

Split, 1

Apply Cartesian Product Axiom

7 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

8 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, 7

9 Set(y) & Set(x) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e y & c2 e x]]

U Spec, 8

10 Set(y) & Set(x)

Join, 3, 2

11 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e y & c2 e x]]

Detach, 9, 10

12 Set'(yx) & ALL(c1):ALL(c2):[(c1,c2) e yx <=> c1 e y & c2 e x]

E Spec, 11

Define: xy (the Cartesian product of y and x)

13 Set'(yx)

Split, 12

14 ALL(c1):ALL(c2):[(c1,c2) e yx <=> c1 e y & c2 e x]

Split, 12

Apply Subset Axiom

15 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e yx & f(b)=a]]

Subset, 13

16 Set'(f') & ALL(a):ALL(b):[(a,b) e f' <=> (a,b) e yx & f(b)=a]

E Spec, 15

Define: f' (as subset of yx)

17 Set'(f')

Split, 16

18 ALL(a):ALL(b):[(a,b) e f' <=> (a,b) e yx & f(b)=a]

Split, 16

Prove: f' is a function

Apply the Function Axiom

19 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

20 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']]

U Spec, 19

21 ALL(b):[ALL(c):ALL(d):[(c,d) e f' => c e y & d e b]

& ALL(c):[c e y => 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']]

U Spec, 20

Sufficient: For functionality of f'

22 ALL(c):ALL(d):[(c,d) e f' => c e y & d e x]

& ALL(c):[c e y => EXIST(d):[d e x & (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']

U Spec, 21

Prove: ALL(c):ALL(d):[(c,d) e f' => c e y & d e x]

Suppose...

23 (t,u) e f'

Premise

24 ALL(b):[(t,b) e f' <=> (t,b) e yx & f(b)=t]

U Spec, 18

25 (t,u) e f' <=> (t,u) e yx & f(u)=t

U Spec, 24

26 [(t,u) e f' => (t,u) e yx & f(u)=t]

& [(t,u) e yx & f(u)=t => (t,u) e f']

Iff-And, 25

27 (t,u) e f' => (t,u) e yx & f(u)=t

Split, 26

28 (t,u) e yx & f(u)=t => (t,u) e f'

Split, 26

29 (t,u) e yx & f(u)=t

Detach, 27, 23

30 (t,u) e yx

Split, 29

31 f(u)=t

Split, 29

32 ALL(c2):[(t,c2) e yx <=> t e y & c2 e x]

U Spec, 14

33 (t,u) e yx <=> t e y & u e x

U Spec, 32

34 [(t,u) e yx => t e y & u e x]

& [t e y & u e x => (t,u) e yx]

Iff-And, 33

35 (t,u) e yx => t e y & u e x

Split, 34

36 t e y & u e x => (t,u) e yx

Split, 34

37 t e y & u e x

Detach, 35, 30

As Required:

38 ALL(c):ALL(d):[(c,d) e f' => c e y & d e x]

4 Conclusion, 23

Prove: ALL(c):[c e y => EXIST(d):[d e x & (c,d) e f']]

Suppose...

39 t e y

Premise

40 t e y => EXIST(b):[b e x & f(b)=t]

U Spec, 5

41 EXIST(b):[b e x & f(b)=t]

Detach, 40, 39

42 u e x & f(u)=t

E Spec, 41

43 u e x

Split, 42

44 f(u)=t

Split, 42

45 ALL(b):[(t,b) e f' <=> (t,b) e yx & f(b)=t]

U Spec, 18

46 (t,u) e f' <=> (t,u) e yx & f(u)=t

U Spec, 45

47 [(t,u) e f' => (t,u) e yx & f(u)=t]

& [(t,u) e yx & f(u)=t => (t,u) e f']

Iff-And, 46

48 (t,u) e f' => (t,u) e yx & f(u)=t

Split, 47

49 (t,u) e yx & f(u)=t => (t,u) e f'

Split, 47

50 ALL(c2):[(t,c2) e yx <=> t e y & c2 e x]

U Spec, 14

51 (t,u) e yx <=> t e y & u e x

U Spec, 50

52 [(t,u) e yx => t e y & u e x]

& [t e y & u e x => (t,u) e yx]

Iff-And, 51

53 (t,u) e yx => t e y & u e x

Split, 52

54 t e y & u e x => (t,u) e yx

Split, 52

55 t e y & u e x

Join, 39, 43

56 (t,u) e yx

Detach, 54, 55

57 (t,u) e yx & f(u)=t

Join, 56, 44

58 (t,u) e f'

Detach, 49, 57

59 u e x & (t,u) e f'

Join, 43, 58

60 EXIST(d):[d e x & (t,d) e f']

E Gen, 59

As Required:

61 ALL(c):[c e y => EXIST(d):[d e x & (c,d) e f']]

4 Conclusion, 39

Prove: ALL(c):ALL(d1):ALL(d2):[(c,d1) e f' & (c,d2) e f' => d1=d2]

Suppose...

62 (t,u1) e f' & (t,u2) e f'

Premise

63 (t,u1) e f'

Split, 62

64 (t,u2) e f'

Split, 62

65 ALL(b):[(t,b) e f' <=> (t,b) e yx & f(b)=t]

U Spec, 18

66 (t,u1) e f' <=> (t,u1) e yx & f(u1)=t

U Spec, 65

67 [(t,u1) e f' => (t,u1) e yx & f(u1)=t]

& [(t,u1) e yx & f(u1)=t => (t,u1) e f']

Iff-And, 66

68 (t,u1) e f' => (t,u1) e yx & f(u1)=t

Split, 67

69 (t,u1) e yx & f(u1)=t => (t,u1) e f'

Split, 67

70 (t,u1) e yx & f(u1)=t

Detach, 68, 63

71 (t,u1) e yx

Split, 70

72 f(u1)=t

Split, 70

73 ALL(c2):[(t,c2) e yx <=> t e y & c2 e x]

U Spec, 14

74 (t,u1) e yx <=> t e y & u1 e x

U Spec, 73

75 [(t,u1) e yx => t e y & u1 e x]

& [t e y & u1 e x => (t,u1) e yx]

Iff-And, 74

76 (t,u1) e yx => t e y & u1 e x

Split, 75

77 t e y & u1 e x => (t,u1) e yx

Split, 75

78 t e y & u1 e x

Detach, 76, 71

79 t e y

Split, 78

80 u1 e x

Split, 78

81 (t,u2) e f' <=> (t,u2) e yx & f(u2)=t

U Spec, 65

82 [(t,u2) e f' => (t,u2) e yx & f(u2)=t]

& [(t,u2) e yx & f(u2)=t => (t,u2) e f']

Iff-And, 81

83 (t,u2) e f' => (t,u2) e yx & f(u2)=t

Split, 82

84 (t,u2) e yx & f(u2)=t => (t,u2) e f'

Split, 82

85 (t,u2) e yx & f(u2)=t

Detach, 83, 64

86 (t,u2) e yx

Split, 85

87 f(u2)=t

Split, 85

88 (t,u2) e yx <=> t e y & u2 e x

U Spec, 73

89 [(t,u2) e yx => t e y & u2 e x]

& [t e y & u2 e x => (t,u2) e yx]

Iff-And, 88

90 (t,u2) e yx => t e y & u2 e x

Split, 89

91 t e y & u2 e x => (t,u2) e yx

Split, 89

92 t e y & u2 e x

Detach, 90, 86

93 t e y

Split, 92

94 u2 e x

Split, 92

95 f(u1)=f(u2)

Substitute, 87, 72

96 ALL(b):[u1 e x & b e x => [f(u1)=f(b) => u1=b]]

U Spec, 6

97 u1 e x & u2 e x => [f(u1)=f(u2) => u1=u2]

U Spec, 96

98 u1 e x & u2 e x

Join, 80, 94

99 f(u1)=f(u2) => u1=u2

Detach, 97, 98

100 u1=u2

Detach, 99, 95

As Required:

101 ALL(c):ALL(d1):ALL(d2):[(c,d1) e f' & (c,d2) e f' => d1=d2]

4 Conclusion, 62

102 ALL(c):ALL(d):[(c,d) e f' => c e y & d e x]

& ALL(c):[c e y => EXIST(d):[d e x & (c,d) e f']]

Join, 38, 61

103 ALL(c):ALL(d):[(c,d) e f' => c e y & d e x]

& ALL(c):[c e y => EXIST(d):[d e x & (c,d) e f']]

& ALL(c):ALL(d1):ALL(d2):[(c,d1) e f' & (c,d2) e f' => d1=d2]

Join, 102, 101

f' is a function

104 ALL(c):ALL(d):[d=f'(c) <=> (c,d) e f']

Detach, 22, 103

Prove: ALL(a):ALL(b):[a e x & b e y => [f'(b)=a <=> f(a)=b]]

Suppose...

105 t e x & u e y

Premise

106 t e x

Split, 105

107 u e y

Split, 105

Prove: f'(u)=t => f(t)=u

Suppose...

108 f'(u)=t

Premise

109 ALL(b):[(u,b) e f' <=> (u,b) e yx & f(b)=u]

U Spec, 18

110 (u,t) e f' <=> (u,t) e yx & f(t)=u

U Spec, 109

111 [(u,t) e f' => (u,t) e yx & f(t)=u]

& [(u,t) e yx & f(t)=u => (u,t) e f']

Iff-And, 110

112 (u,t) e f' => (u,t) e yx & f(t)=u

Split, 111

113 (u,t) e yx & f(t)=u => (u,t) e f'

Split, 111

114 ALL(d):[d=f'(u) <=> (u,d) e f']

U Spec, 104

115 t=f'(u) <=> (u,t) e f'

U Spec, 114

116 [t=f'(u) => (u,t) e f'] & [(u,t) e f' => t=f'(u)]

Iff-And, 115

117 t=f'(u) => (u,t) e f'

Split, 116

118 (u,t) e f' => t=f'(u)

Split, 116

119 t=f'(u)

Sym, 108

120 (u,t) e f'

Detach, 117, 119

121 (u,t) e yx & f(t)=u

Detach, 112, 120

122 (u,t) e yx

Split, 121

123 f(t)=u

Split, 121

As Required:

124 f'(u)=t => f(t)=u

4 Conclusion, 108

Prove: f(t)=u => f'(u)=t

Suppose...

125 f(t)=u

Premise

126 ALL(b):[(u,b) e f' <=> (u,b) e yx & f(b)=u]

U Spec, 18

127 (u,t) e f' <=> (u,t) e yx & f(t)=u

U Spec, 126

128 [(u,t) e f' => (u,t) e yx & f(t)=u]

& [(u,t) e yx & f(t)=u => (u,t) e f']

Iff-And, 127

129 (u,t) e f' => (u,t) e yx & f(t)=u

Split, 128

130 (u,t) e yx & f(t)=u => (u,t) e f'

Split, 128

131 ALL(c2):[(u,c2) e yx <=> u e y & c2 e x]

U Spec, 14

132 (u,t) e yx <=> u e y & t e x

U Spec, 131

133 [(u,t) e yx => u e y & t e x]

& [u e y & t e x => (u,t) e yx]

Iff-And, 132

134 (u,t) e yx => u e y & t e x

Split, 133

135 u e y & t e x => (u,t) e yx

Split, 133

136 u e y & t e x

Join, 107, 106

137 (u,t) e yx

Detach, 135, 136

138 (u,t) e yx & f(t)=u

Join, 137, 125

139 (u,t) e f'

Detach, 130, 138

140 ALL(d):[d=f'(u) <=> (u,d) e f']

U Spec, 104

141 t=f'(u) <=> (u,t) e f'

U Spec, 140

142 [t=f'(u) => (u,t) e f'] & [(u,t) e f' => t=f'(u)]

Iff-And, 141

143 t=f'(u) => (u,t) e f'

Split, 142

144 (u,t) e f' => t=f'(u)

Split, 142

145 t=f'(u)

Detach, 144, 139

146 f'(u)=t

Sym, 145

As Required:

147 f(t)=u => f'(u)=t

4 Conclusion, 125

148 [f'(u)=t => f(t)=u] & [f(t)=u => f'(u)=t]

Join, 124, 147

149 f'(u)=t <=> f(t)=u

Iff-And, 148

As Required:

150 ALL(a):ALL(b):[a e x & b e y => [f'(b)=a <=> f(a)=b]]

4 Conclusion, 105

Prove: ALL(a):[a e y => f'(a) e x]

Suppose...

151 t e y

Premise

152 t e y => EXIST(d):[d e x & (t,d) e f']

U Spec, 61

153 EXIST(d):[d e x & (t,d) e f']

Detach, 152, 151

154 u e x & (t,u) e f'

E Spec, 153

155 u e x

Split, 154

156 (t,u) e f'

Split, 154

157 ALL(d):[d=f'(t) <=> (t,d) e f']

U Spec, 104

158 u=f'(t) <=> (t,u) e f'

U Spec, 157

159 [u=f'(t) => (t,u) e f'] & [(t,u) e f' => u=f'(t)]

Iff-And, 158

160 u=f'(t) => (t,u) e f'

Split, 159

161 (t,u) e f' => u=f'(t)

Split, 159

162 u=f'(t)

Detach, 161, 156

163 f'(t) e x

Substitute, 162, 155

As Required:

164 ALL(a):[a e y => f'(a) e x]

4 Conclusion, 151

165 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]]

Join, 164, 150

As Required:

166 ALL(x):ALL(y):ALL(f):[Set(x) & Set(y)

& ALL(a):[a e x => f(a) e y]

& ALL(a):[a e y => EXIST(b):[b e x & f(b)=a]]

& ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]

=> EXIST(f'):[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]]]]

4 Conclusion, 1