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