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