LEMMA 1

*******

 

Every bijection has an inverse that is itself a bijection.

 

(This proof was written with the aid of the author's DC Proof 2.0 software available at http://www.dcproof.com )

 

 

OUTLINE

*******

 

Suppose f is a function mapping set x to set y.

Suppose further that f is a bijection.

Construct set of ordered pairs g (reversing the co-ordinates of f).

Prove g is a bijection.

 

 

DEFINITIONS

***********

 

Define: Injection

 

1     ALL(f):ALL(a):ALL(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):[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):[Bijection(f,a,b) <=> Injection(f,a,b) & Surjection(f,a,b)]

      Axiom

 

    

     PROOF OF LEMMA 1

     ****************

    

     Suppose f is a function mapping set x to set y

 

      4     Set(x) & Set(y) & ALL(c):[c e x => f(c) e y]

            Premise

 

      5     Set(x)

            Split, 4

 

      6     Set(y)

            Split, 4

 

      7     ALL(c):[c e x => f(c) e y]

            Split, 4

 

         

          Suppose f is a bijection

 

            8     Bijection(f,x,y)

                  Premise

 

          Apply definition of Bijection

 

            9     ALL(a):ALL(b):[Bijection(f,a,b) <=> Injection(f,a,b) & Surjection(f,a,b)]

                  U Spec, 3

 

            10    ALL(b):[Bijection(f,x,b) <=> Injection(f,x,b) & Surjection(f,x,b)]

                  U Spec, 9

 

            11    Bijection(f,x,y) <=> Injection(f,x,y) & Surjection(f,x,y)

                  U Spec, 10

 

            12    [Bijection(f,x,y) => Injection(f,x,y) & Surjection(f,x,y)]

              & [Injection(f,x,y) & Surjection(f,x,y) => Bijection(f,x,y)]

                  Iff-And, 11

 

            13    Bijection(f,x,y) => Injection(f,x,y) & Surjection(f,x,y)

                  Split, 12

 

            14    Injection(f,x,y) & Surjection(f,x,y) => Bijection(f,x,y)

                  Split, 12

 

            15    Injection(f,x,y) & Surjection(f,x,y)

                  Detach, 13, 8

 

            16    Injection(f,x,y)

                  Split, 15

 

            17    Surjection(f,x,y)

                  Split, 15

 

          Apply definition of Injection

 

            18    ALL(a):ALL(b):[Injection(f,a,b) <=> ALL(c):ALL(d):[c e a & d e a => [f(c)=f(d) => c=d]]]

                  U Spec, 1

 

            19    ALL(b):[Injection(f,x,b) <=> ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]]

                  U Spec, 18

 

            20    Injection(f,x,y) <=> ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]

                  U Spec, 19

 

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

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

                  Iff-And, 20

 

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

                  Split, 21

 

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

                  Split, 21

 

            24    ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]

                  Detach, 22, 16

 

          Apply definition of Surjection

 

            25    ALL(a):ALL(b):[Surjection(f,a,b) <=> ALL(c):[c e b => EXIST(d):[d e a & f(d)=c]]]

                  U Spec, 2

 

            26    ALL(b):[Surjection(f,x,b) <=> ALL(c):[c e b => EXIST(d):[d e x & f(d)=c]]]

                  U Spec, 25

 

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

                  U Spec, 26

 

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

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

                  Iff-And, 27

 

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

                  Split, 28

 

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

                  Split, 28

 

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

                  Detach, 29, 17

 

          Construct function g, the inverse of f.

         

          Apply the Cartesian Product Axiom.

 

            32    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

 

            33    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, 32

 

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

                  U Spec, 33

 

            35    Set(y) & Set(x)

                  Join, 6, 5

 

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

                  Detach, 34, 35

 

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

                  E Spec, 36

 

         

          Define: yx  (Cartesian product of sets y and x)

 

            38    Set'(yx)

                  Split, 37

 

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

                  Split, 37

 

          Construct g

         

          Apply Subset Axiom

 

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

                  Subset, 38

 

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

                  E Spec, 40

 

         

          Define: g  (the inverse of f)

 

            42    Set'(g)

                  Split, 41

 

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

                  Split, 41

 

          Prove functionality of g

         

          Apply Function Axiom

 

            44    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

 

            45    ALL(a):ALL(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(d1):ALL(d2):[(c,d1) e g & (c,d2) e g => d1=d2]

              => ALL(c):ALL(d):[d=g(c) <=> (c,d) e g]]

                  U Spec, 44

 

            46    ALL(b):[ALL(c):ALL(d):[(c,d) e g => c e y & d e b]

              & ALL(c):[c e y => EXIST(d):[d e b & (c,d) e g]]

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

              => ALL(c):ALL(d):[d=g(c) <=> (c,d) e g]]

                  U Spec, 45

 

         

          Sufficient: For functionality of g

 

            47    ALL(c):ALL(d):[(c,d) e g => c e y & d e x]

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

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

              => ALL(c):ALL(d):[d=g(c) <=> (c,d) e g]

                  U Spec, 46

 

             

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

             

              Suppose...

 

                  48    (t,u) e g

                        Premise

 

              Apply definition of g

 

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

                        U Spec, 43

 

                  50    (t,u) e g <=> (t,u) e yx & t=f(u)

                        U Spec, 49

 

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

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

                        Iff-And, 50

 

                  52    (t,u) e g => (t,u) e yx & t=f(u)

                        Split, 51

 

                  53    (t,u) e yx & t=f(u) => (t,u) e g

                        Split, 51

 

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

                        Detach, 52, 48

 

                  55    (t,u) e yx

                        Split, 54

 

                  56    t=f(u)

                        Split, 54

 

              Apply definition of yx

 

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

                        U Spec, 39

 

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

                        U Spec, 57

 

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

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

                        Iff-And, 58

 

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

                        Split, 59

 

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

                        Split, 59

 

                  62    t e y & u e x

                        Detach, 60, 55

 

          Functionality, Part 1

 

            63    ALL(c):ALL(d):[(c,d) e g => c e y & d e x]

                  4 Conclusion, 48

 

             

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

             

              Suppose...

 

                  64    t e y

                        Premise

 

              Apply previous result

 

                  65    t e y => EXIST(d):[d e x & f(d)=t]

                        U Spec, 31

 

                  66    EXIST(d):[d e x & f(d)=t]

                        Detach, 65, 64

 

                  67    u e x & f(u)=t

                        E Spec, 66

 

                  68    u e x

                        Split, 67

 

                  69    f(u)=t

                        Split, 67

 

              Apply definition of g

 

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

                        U Spec, 43

 

                  71    (t,u) e g <=> (t,u) e yx & t=f(u)

                        U Spec, 70

 

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

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

                        Iff-And, 71

 

                  73    (t,u) e g => (t,u) e yx & t=f(u)

                        Split, 72

 

              Sufficient: (t,u) e g

 

                  74    (t,u) e yx & t=f(u) => (t,u) e g

                        Split, 72

 

              Apply definition of yx

 

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

                        U Spec, 39

 

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

                        U Spec, 75

 

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

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

                        Iff-And, 76

 

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

                        Split, 77

 

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

                        Split, 77

 

                  80    t e y & u e x

                        Join, 64, 68

 

                  81    (t,u) e yx

                        Detach, 79, 80

 

                  82    t=f(u)

                        Sym, 69

 

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

                        Join, 81, 82

 

                  84    (t,u) e g

                        Detach, 74, 83

 

                  85    u e x & (t,u) e g

                        Join, 68, 84

 

                  86    EXIST(d):[d e x & (t,d) e g]

                        E Gen, 85

 

          Functionality, Part 2

 

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

                  4 Conclusion, 64

 

             

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

             

              Suppose...

 

                  88    (t,u1) e g & (t,u2) e g

                        Premise

 

                  89    (t,u1) e g

                        Split, 88

 

                  90    (t,u2) e g

                        Split, 88

 

              Apply definition of g

 

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

                        U Spec, 43

 

                  92    (t,u1) e g <=> (t,u1) e yx & t=f(u1)

                        U Spec, 91

 

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

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

                        Iff-And, 92

 

                  94    (t,u1) e g => (t,u1) e yx & t=f(u1)

                        Split, 93

 

                  95    (t,u1) e yx & t=f(u1) => (t,u1) e g

                        Split, 93

 

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

                        Detach, 94, 89

 

                  97    (t,u1) e yx

                        Split, 96

 

                  98    t=f(u1)

                        Split, 96

 

              Apply definition of g

 

                  99    (t,u2) e g <=> (t,u2) e yx & t=f(u2)

                        U Spec, 91

 

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

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

                        Iff-And, 99

 

                  101  (t,u2) e g => (t,u2) e yx & t=f(u2)

                        Split, 100

 

                  102  (t,u2) e yx & t=f(u2) => (t,u2) e g

                        Split, 100

 

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

                        Detach, 101, 90

 

                  104  (t,u2) e yx

                        Split, 103

 

                  105  t=f(u2)

                        Split, 103

 

                  106  f(u1)=f(u2)

                        Substitute, 98, 105

 

              Apply injectivity of f

 

                  107  ALL(d):[u1 e x & d e x => [f(u1)=f(d) => u1=d]]

                        U Spec, 24

 

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

                        U Spec, 107

 

              Apply definition of yx

 

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

                        U Spec, 39

 

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

                        U Spec, 109

 

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

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

                        Iff-And, 110

 

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

                        Split, 111

 

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

                        Split, 111

 

                  114  t e y & u1 e x

                        Detach, 112, 97

 

                  115  t e y

                        Split, 114

 

                  116  u1 e x

                        Split, 114

 

              Apply definition of yx

 

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

                        U Spec, 109

 

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

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

                        Iff-And, 117

 

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

                        Split, 118

 

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

                        Split, 118

 

                  121  t e y & u2 e x

                        Detach, 119, 104

 

                  122  t e y

                        Split, 121

 

                  123  u2 e x

                        Split, 121

 

                  124  u1 e x & u2 e x

                        Join, 116, 123

 

                  125  f(u1)=f(u2) => u1=u2

                        Detach, 108, 124

 

                  126  u1=u2

                        Detach, 125, 106

 

          Functionality, Part 3

 

            127  ALL(c):ALL(d1):ALL(d2):[(c,d1) e g & (c,d2) e g => d1=d2]

                  4 Conclusion, 88

 

            128  ALL(c):ALL(d):[(c,d) e g => c e y & d e x]

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

                  Join, 63, 87

 

            129  ALL(c):ALL(d):[(c,d) e g => c e y & d e x]

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

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

                  Join, 128, 127

 

          As Required:

         

          g is a function

 

            130  ALL(c):ALL(d):[d=g(c) <=> (c,d) e g]

                  Detach, 47, 129

 

             

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

             

              Suppose...

 

                  131  t e y

                        Premise

 

              Apply functionality of g

 

                  132  t e y => EXIST(d):[d e x & (t,d) e g]

                        U Spec, 87

 

                  133  EXIST(d):[d e x & (t,d) e g]

                        Detach, 132, 131

 

                  134  u e x & (t,u) e g

                        E Spec, 133

 

                  135  u e x

                        Split, 134

 

                  136  (t,u) e g

                        Split, 134

 

              Apply functionality of g

 

                  137  ALL(d):[d=g(t) <=> (t,d) e g]

                        U Spec, 130

 

                  138  u=g(t) <=> (t,u) e g

                        U Spec, 137

 

                  139  [u=g(t) => (t,u) e g] & [(t,u) e g => u=g(t)]

                        Iff-And, 138

 

                  140  u=g(t) => (t,u) e g

                        Split, 139

 

                  141  (t,u) e g => u=g(t)

                        Split, 139

 

                  142  u=g(t)

                        Detach, 141, 136

 

                  143  g(t) e x

                        Substitute, 142, 135

 

          As Required:

 

            144  ALL(a):[a e y => g(a) e x]

                  4 Conclusion, 131

 

            145  ALL(c):[c e y => g(c) e x]

                  Rename, 144

 

             

              Prove g is the inverse of f

             

              Suppose...

 

                  146  t e x & u e y

                        Premise

 

                  147  t e x

                        Split, 146

 

                  148  u e y

                        Split, 146

 

                  

                   '=>'

                  

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

                  

                   Suppose...

 

                        149  f(t)=u

                              Premise

 

                   Apply definition of g

 

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

                              U Spec, 43

 

                        151  (u,t) e g <=> (u,t) e yx & u=f(t)

                              U Spec, 150

 

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

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

                              Iff-And, 151

 

                        153  (u,t) e g => (u,t) e yx & u=f(t)

                              Split, 152

 

                        154  (u,t) e yx & u=f(t) => (u,t) e g

                              Split, 152

 

                   Apply definition of yx

 

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

                              U Spec, 39

 

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

                              U Spec, 155

 

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

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

                              Iff-And, 156

 

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

                              Split, 157

 

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

                              Split, 157

 

                        160  u e y & t e x

                              Join, 148, 147

 

                        161  (u,t) e yx

                              Detach, 159, 160

 

                        162  u=f(t)

                              Sym, 149

 

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

                              Join, 161, 162

 

                        164  (u,t) e g

                              Detach, 154, 163

 

                   Apply functionality of g

 

                        165  ALL(d):[d=g(u) <=> (u,d) e g]

                              U Spec, 130

 

                        166  t=g(u) <=> (u,t) e g

                              U Spec, 165

 

                        167  [t=g(u) => (u,t) e g] & [(u,t) e g => t=g(u)]

                              Iff-And, 166

 

                        168  t=g(u) => (u,t) e g

                              Split, 167

 

                        169  (u,t) e g => t=g(u)

                              Split, 167

 

                        170  t=g(u)

                              Detach, 169, 164

 

                        171  g(u)=t

                              Sym, 170

 

              As Required:

 

                  172  f(t)=u => g(u)=t

                        4 Conclusion, 149

 

                  

                   '<='

                  

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

                  

                   Suppose...

 

                        173  g(u)=t

                              Premise

 

                   Apply functionality of g

 

                        174  ALL(d):[d=g(u) <=> (u,d) e g]

                              U Spec, 130

 

                        175  t=g(u) <=> (u,t) e g

                              U Spec, 174

 

                        176  [t=g(u) => (u,t) e g] & [(u,t) e g => t=g(u)]

                              Iff-And, 175

 

                        177  t=g(u) => (u,t) e g

                              Split, 176

 

                        178  (u,t) e g => t=g(u)

                              Split, 176

 

                        179  t=g(u)

                              Sym, 173

 

                        180  (u,t) e g

                              Detach, 177, 179

 

                   Apply definition of g

 

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

                              U Spec, 43

 

                        182  (u,t) e g <=> (u,t) e yx & u=f(t)

                              U Spec, 181

 

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

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

                              Iff-And, 182

 

                        184  (u,t) e g => (u,t) e yx & u=f(t)

                              Split, 183

 

                        185  (u,t) e yx & u=f(t) => (u,t) e g

                              Split, 183

 

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

                              Detach, 184, 180

 

                        187  (u,t) e yx

                              Split, 186

 

                        188  u=f(t)

                              Split, 186

 

                        189  f(t)=u

                              Sym, 188

 

              As Required:

 

                  190  g(u)=t => f(t)=u

                        4 Conclusion, 173

 

                  191  [g(u)=t => f(t)=u] & [f(t)=u => g(u)=t]

                        Join, 190, 172

 

                  192  g(u)=t <=> f(t)=u

                        Iff-And, 191

 

          As Required:

         

          g is the inverse of f

 

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

                  4 Conclusion, 146

 

            194  ALL(c):ALL(d):[c e x & d e y => [g(d)=c <=> f(c)=d]]

                  Rename, 193

 

          Apply definition of Bijection

 

            195  ALL(a):ALL(b):[Bijection(g,a,b) <=> Injection(g,a,b) & Surjection(g,a,b)]

                  U Spec, 3

 

            196  ALL(b):[Bijection(g,y,b) <=> Injection(g,y,b) & Surjection(g,y,b)]

                  U Spec, 195

 

            197  Bijection(g,y,x) <=> Injection(g,y,x) & Surjection(g,y,x)

                  U Spec, 196

 

            198  [Bijection(g,y,x) => Injection(g,y,x) & Surjection(g,y,x)]

              & [Injection(g,y,x) & Surjection(g,y,x) => Bijection(g,y,x)]

                  Iff-And, 197

 

            199  Bijection(g,y,x) => Injection(g,y,x) & Surjection(g,y,x)

                  Split, 198

 

          Sufficient: Bijection(g,y,x)

 

            200  Injection(g,y,x) & Surjection(g,y,x) => Bijection(g,y,x)

                  Split, 198

 

          Apply definition of Injection

 

            201  ALL(a):ALL(b):[Injection(g,a,b) <=> ALL(c):ALL(d):[c e a & d e a => [g(c)=g(d) => c=d]]]

                  U Spec, 1

 

            202  ALL(b):[Injection(g,y,b) <=> ALL(c):ALL(d):[c e y & d e y => [g(c)=g(d) => c=d]]]

                  U Spec, 201

 

            203  Injection(g,y,x) <=> ALL(c):ALL(d):[c e y & d e y => [g(c)=g(d) => c=d]]

                  U Spec, 202

 

            204  [Injection(g,y,x) => ALL(c):ALL(d):[c e y & d e y => [g(c)=g(d) => c=d]]]

              & [ALL(c):ALL(d):[c e y & d e y => [g(c)=g(d) => c=d]] => Injection(g,y,x)]

                  Iff-And, 203

 

            205  Injection(g,y,x) => ALL(c):ALL(d):[c e y & d e y => [g(c)=g(d) => c=d]]

                  Split, 204

 

          Sufficient: Injection(g,y,x)

 

            206  ALL(c):ALL(d):[c e y & d e y => [g(c)=g(d) => c=d]] => Injection(g,y,x)

                  Split, 204

 

             

              Prove: ALL(c):ALL(d):[c e y & d e y => [g(c)=g(d) => c=d]]

             

              Suppose...

 

                  207  t e y & u e y

                        Premise

 

                  208  t e y

                        Split, 207

 

                  209  u e y

                        Split, 207

 

                  

                   Prove: g(t)=g(u) => t=u

                  

                   Suppose...

 

                        210  g(t)=g(u)

                              Premise

 

                   Apply previous result

 

                        211  ALL(b):[g(u) e x & b e y => [g(b)=g(u) <=> f(g(u))=b]]

                              U Spec, 193

 

                        212  g(u) e x & t e y => [g(t)=g(u) <=> f(g(u))=t]

                              U Spec, 211

 

                        213  g(u) e x & u e y => [g(u)=g(u) <=> f(g(u))=u]

                              U Spec, 211

 

                        214  u e y => g(u) e x

                              U Spec, 144

 

                        215  g(u) e x

                              Detach, 214, 209

 

                        216  g(u) e x & t e y

                              Join, 215, 208

 

                        217  g(t)=g(u) <=> f(g(u))=t

                              Detach, 212, 216

 

                        218  [g(t)=g(u) => f(g(u))=t] & [f(g(u))=t => g(t)=g(u)]

                              Iff-And, 217

 

                        219  g(t)=g(u) => f(g(u))=t

                              Split, 218

 

                        220  f(g(u))=t => g(t)=g(u)

                              Split, 218

 

                        221  f(g(u))=t

                              Detach, 219, 210

 

                        222  g(u) e x & u e y

                              Join, 215, 209

 

                        223  g(u)=g(u) <=> f(g(u))=u

                              Detach, 213, 222

 

                        224  [g(u)=g(u) => f(g(u))=u] & [f(g(u))=u => g(u)=g(u)]

                              Iff-And, 223

 

                        225  g(u)=g(u) => f(g(u))=u

                              Split, 224

 

                        226  f(g(u))=u => g(u)=g(u)

                              Split, 224

 

                        227  g(u)=g(u)

                              Reflex

 

                        228  f(g(u))=u

                              Detach, 225, 227

 

                        229  t=u

                              Substitute, 221, 228

 

              As Required:

 

                  230  g(t)=g(u) => t=u

                        4 Conclusion, 210

 

          As Required:

 

            231  ALL(c):ALL(d):[c e y & d e y => [g(c)=g(d) => c=d]]

                  4 Conclusion, 207

 

          As Required:

 

            232  Injection(g,y,x)

                  Detach, 206, 231

 

          Apply definition of Surjection

 

            233  ALL(a):ALL(b):[Surjection(g,a,b) <=> ALL(c):[c e b => EXIST(d):[d e a & g(d)=c]]]

                  U Spec, 2

 

            234  ALL(b):[Surjection(g,y,b) <=> ALL(c):[c e b => EXIST(d):[d e y & g(d)=c]]]

                  U Spec, 233

 

            235  Surjection(g,y,x) <=> ALL(c):[c e x => EXIST(d):[d e y & g(d)=c]]

                  U Spec, 234

 

            236  [Surjection(g,y,x) => ALL(c):[c e x => EXIST(d):[d e y & g(d)=c]]]

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

                  Iff-And, 235

 

            237  Surjection(g,y,x) => ALL(c):[c e x => EXIST(d):[d e y & g(d)=c]]

                  Split, 236

 

          Sufficient: Surjection(g,y,x)

 

            238  ALL(c):[c e x => EXIST(d):[d e y & g(d)=c]] => Surjection(g,y,x)

                  Split, 236

 

             

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

             

              Suppose...

 

                  239  t e x

                        Premise

 

                  240  t e x => f(t) e y

                        U Spec, 7

 

                  241  f(t) e y

                        Detach, 240, 239

 

              Apply previous result

 

                  242  ALL(b):[t e x & b e y => [g(b)=t <=> f(t)=b]]

                        U Spec, 193

 

                  243  t e x & f(t) e y => [g(f(t))=t <=> f(t)=f(t)]

                        U Spec, 242

 

                  244  t e x & f(t) e y

                        Join, 239, 241

 

                  245  g(f(t))=t <=> f(t)=f(t)

                        Detach, 243, 244

 

                  246  [g(f(t))=t => f(t)=f(t)] & [f(t)=f(t) => g(f(t))=t]

                        Iff-And, 245

 

                  247  g(f(t))=t => f(t)=f(t)

                        Split, 246

 

                  248  f(t)=f(t) => g(f(t))=t

                        Split, 246

 

                  249  f(t)=f(t)

                        Reflex

 

                  250  g(f(t))=t

                        Detach, 248, 249

 

                  251  f(t) e y & g(f(t))=t

                        Join, 241, 250

 

                  252  EXIST(d):[d e y & g(d)=t]

                        E Gen, 251

 

          As Required:

 

            253  ALL(c):[c e x => EXIST(d):[d e y & g(d)=c]]

                  4 Conclusion, 239

 

            254  Surjection(g,y,x)

                  Detach, 238, 253

 

            255  Injection(g,y,x) & Surjection(g,y,x)

                  Join, 232, 254

 

            256  Bijection(g,y,x)

                  Detach, 200, 255

 

            257  ALL(a):[a e y => g(a) e x]

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

                  Join, 144, 193

 

            258  ALL(a):[a e y => g(a) e x]

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

              & Bijection(g,y,x)

                  Join, 257, 256

 

            259  ALL(c):[c e y => g(c) e x]

              & ALL(c):ALL(d):[c e x & d e y => [g(d)=c <=> f(c)=d]]

                  Join, 145, 194

 

            260  ALL(c):[c e y => g(c) e x]

              & ALL(c):ALL(d):[c e x & d e y => [g(d)=c <=> f(c)=d]]

              & Bijection(g,y,x)

                  Join, 259, 256

 

     As Required:

 

      261  Bijection(f,x,y)

          => EXIST(g):[ALL(c):[c e y => g(c) e x]

          & ALL(c):ALL(d):[c e x & d e y => [g(d)=c <=> f(c)=d]]

          & Bijection(g,y,x)]

            4 Conclusion, 8

 

As Required:

 

262  ALL(a):ALL(b):ALL(f):[Set(a) & Set(b) & ALL(c):[c e a => f(c) e b]

     => [Bijection(f,a,b)

     => EXIST(g):[ALL(c):[c e b => g(c) e a]

     & ALL(c):ALL(d):[c e a & d e b => [g(d)=c <=> f(c)=d]]

     & Bijection(g,b,a)]]]

      4 Conclusion, 4