THEOREM

*******

 

Given any non-empty set x, there exists a unique identity function idx: x --> x.

 

  ALL(x):[Set(x) & EXIST(a):a e x

 

  => EXIST(idx):[ALL(a):[a e x => idx(a) e x]   <-- Existence

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

 

  & ALL(idx'):[ALL(a):[a e x => idx'(a)=a]      <-- Uniqueness

  => ALL(a):[a e x => idx'(a)=idx(a)]]]]

 

By Dan Christensen

2022-02-01

 

This machine-verified, formal proof was written with the aid of the author's DC Proof 2.0 freeware available at http://www.dcproof.com

 

PROOF

*****

 

    Let x be non-empty set

 

      1     Set(x) & EXIST(a):a e x

            Premise

 

      2     Set(x)

            Split, 1

 

      3     EXIST(a):a e x

            Split, 1

 

    Apply Cartesian Product Axiom

 

      4     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

 

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

            U Spec, 4

 

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

            U Spec, 5

 

      7     Set(x) & Set(x)

            Join, 2, 2

 

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

            Detach, 6, 7

 

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

            E Spec, 8

 

   

    Define: x2

 

      10   Set'(x2)

            Split, 9

 

      11   ALL(c1):ALL(c2):[(c1,c2) e x2 <=> c1 e x & c2 e x]

            Split, 9

 

   

    Apply Subset Axiom

 

      12   EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e x2 & a=b]]

            Subset, 10

 

      13   Set'(eqx) & ALL(a):ALL(b):[(a,b) e eqx <=> (a,b) e x2 & a=b]

            E Spec, 12

 

   

    Define: eqx  (equality relation on x)

 

      14   Set'(eqx)

            Split, 13

 

      15   ALL(a):ALL(b):[(a,b) e eqx <=> (a,b) e x2 & a=b]

            Split, 13

 

   

    Apply Function Axiom

 

      16   ALL(dom):ALL(cod):ALL(gra):[Set(dom) & EXIST(a1):a1 e dom

         & Set(cod) & EXIST(a):a e cod & Set'(gra)

         => [ALL(a1):ALL(b):[(a1,b) e gra => a1 e dom & b e cod]

         & ALL(a1):[a1 e dom => EXIST(b):[b e cod & (a1,b) e gra]]

         & ALL(a1):ALL(b1):ALL(b2):[a1 e dom & b1 e cod & b2 e cod

         => [(a1,b1) e gra & (a1,b2) e gra => b1=b2]]

         => EXIST(fun):ALL(a1):ALL(b):[a1 e dom & b e cod

         => [fun(a1)=b <=> (a1,b) e gra]]]]

            Function

 

      17   ALL(cod):ALL(gra):[Set(x) & EXIST(a1):a1 e x

         & Set(cod) & EXIST(a):a e cod & Set'(gra)

         => [ALL(a1):ALL(b):[(a1,b) e gra => a1 e x & b e cod]

         & ALL(a1):[a1 e x => EXIST(b):[b e cod & (a1,b) e gra]]

         & ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e cod & b2 e cod

         => [(a1,b1) e gra & (a1,b2) e gra => b1=b2]]

         => EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e cod

         => [fun(a1)=b <=> (a1,b) e gra]]]]

            U Spec, 16

 

      18   ALL(gra):[Set(x) & EXIST(a1):a1 e x

         & Set(x) & EXIST(a):a e x & Set'(gra)

         => [ALL(a1):ALL(b):[(a1,b) e gra => a1 e x & b e x]

         & ALL(a1):[a1 e x => EXIST(b):[b e x & (a1,b) e gra]]

         & ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e x & b2 e x

         => [(a1,b1) e gra & (a1,b2) e gra => b1=b2]]

         => EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e x

         => [fun(a1)=b <=> (a1,b) e gra]]]]

            U Spec, 17

 

      19   Set(x) & EXIST(a1):a1 e x

         & Set(x) & EXIST(a):a e x & Set'(eqx)

         => [ALL(a1):ALL(b):[(a1,b) e eqx => a1 e x & b e x]

         & ALL(a1):[a1 e x => EXIST(b):[b e x & (a1,b) e eqx]]

         & ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e x & b2 e x

         => [(a1,b1) e eqx & (a1,b2) e eqx => b1=b2]]

         => EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e x

         => [fun(a1)=b <=> (a1,b) e eqx]]]

            U Spec, 18

 

      20   Set(x) & EXIST(a):a e x & Set(x)

            Join, 1, 2

 

      21   Set(x) & EXIST(a):a e x & Set(x) & EXIST(a):a e x

            Join, 20, 3

 

      22   Set(x) & EXIST(a):a e x & Set(x) & EXIST(a):a e x

         & Set'(eqx)

            Join, 21, 14

 

   

    Sufficient: For existence of function on x

 

      23   ALL(a1):ALL(b):[(a1,b) e eqx => a1 e x & b e x]

         & ALL(a1):[a1 e x => EXIST(b):[b e x & (a1,b) e eqx]]

         & ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e x & b2 e x

         => [(a1,b1) e eqx & (a1,b2) e eqx => b1=b2]]

         => EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e x

         => [fun(a1)=b <=> (a1,b) e eqx]]

            Detach, 19, 22

 

        

         Part 1

        

         Prove: ALL(a1):ALL(b):[(a1,b) e eqx => a1 e x & b e x]

        

         Suppose...

 

            24   (t,u) e eqx

                  Premise

 

         Apply definition of eqx

 

            25   ALL(b):[(t,b) e eqx <=> (t,b) e x2 & t=b]

                  U Spec, 15

 

            26   (t,u) e eqx <=> (t,u) e x2 & t=u

                  U Spec, 25

 

            27   [(t,u) e eqx => (t,u) e x2 & t=u]

             & [(t,u) e x2 & t=u => (t,u) e eqx]

                  Iff-And, 26

 

            28   (t,u) e eqx => (t,u) e x2 & t=u

                  Split, 27

 

            29   (t,u) e x2 & t=u

                  Detach, 28, 24

 

            30   (t,u) e x2

                  Split, 29

 

         Apply definition of x2

 

            31   ALL(c2):[(t,c2) e x2 <=> t e x & c2 e x]

                  U Spec, 11

 

            32   (t,u) e x2 <=> t e x & u e x

                  U Spec, 31

 

            33   [(t,u) e x2 => t e x & u e x]

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

                  Iff-And, 32

 

            34   (t,u) e x2 => t e x & u e x

                  Split, 33

 

            35   t e x & u e x

                  Detach, 34, 30

 

    Part 1

   

    As Required:

 

      36   ALL(a1):ALL(b):[(a1,b) e eqx => a1 e x & b e x]

            4 Conclusion, 24

 

        

         Part 2

        

         Prove: ALL(a1):[a1 e x => EXIST(b):[b e x & (a1,b) e eqx]]

        

         Suppose...

 

            37   t e x

                  Premise

 

         Apply definiton of eqx

 

            38   ALL(b):[(t,b) e eqx <=> (t,b) e x2 & t=b]

                  U Spec, 15

 

            39   (t,t) e eqx <=> (t,t) e x2 & t=t

                  U Spec, 38

 

            40   [(t,t) e eqx => (t,t) e x2 & t=t]

             & [(t,t) e x2 & t=t => (t,t) e eqx]

                  Iff-And, 39

 

            41   (t,t) e x2 & t=t => (t,t) e eqx

                  Split, 40

 

            42   ALL(c2):[(t,c2) e x2 <=> t e x & c2 e x]

                  U Spec, 11

 

            43   (t,t) e x2 <=> t e x & t e x

                  U Spec, 42

 

            44   [(t,t) e x2 => t e x & t e x]

             & [t e x & t e x => (t,t) e x2]

                  Iff-And, 43

 

            45   t e x & t e x => (t,t) e x2

                  Split, 44

 

            46   t e x & t e x

                  Join, 37, 37

 

            47   (t,t) e x2

                  Detach, 45, 46

 

            48   t=t

                  Reflex

 

            49   (t,t) e x2 & t=t

                  Join, 47, 48

 

            50   (t,t) e eqx

                  Detach, 41, 49

 

            51   t e x & (t,t) e eqx

                  Join, 37, 50

 

            52   EXIST(b):[b e x & (t,b) e eqx]

                  E Gen, 51

 

    Part 2

   

    As Required:

 

      53   ALL(a1):[a1 e x => EXIST(b):[b e x & (a1,b) e eqx]]

            4 Conclusion, 37

 

        

         Part 3

        

         Prove: ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e x & b2 e x

                => [(a1,b1) e eqx & (a1,b2) e eqx => b1=b2]]

        

         Suppose...

 

            54   t e x & u e x & v e x

                  Premise

 

            55   t e x

                  Split, 54

 

            56   u e x

                  Split, 54

 

            57   v e x

                  Split, 54

 

            

             Prove: (t,u) e eqx & (t,v) e eqx => u=v

            

             Suppose...

 

                  58   (t,u) e eqx & (t,v) e eqx

                        Premise

 

                  59   (t,u) e eqx

                        Split, 58

 

                  60   (t,v) e eqx

                        Split, 58

 

             Apply definiton of eqx

 

                  61   ALL(b):[(t,b) e eqx <=> (t,b) e x2 & t=b]

                        U Spec, 15

 

                  62   (t,u) e eqx <=> (t,u) e x2 & t=u

                        U Spec, 61

 

                  63   [(t,u) e eqx => (t,u) e x2 & t=u]

                 & [(t,u) e x2 & t=u => (t,u) e eqx]

                        Iff-And, 62

 

                  64   (t,u) e eqx => (t,u) e x2 & t=u

                        Split, 63

 

                  65   (t,u) e x2 & t=u

                        Detach, 64, 59

 

                  66   t=u

                        Split, 65

 

                  67   (t,v) e eqx <=> (t,v) e x2 & t=v

                        U Spec, 61

 

                  68   [(t,v) e eqx => (t,v) e x2 & t=v]

                 & [(t,v) e x2 & t=v => (t,v) e eqx]

                        Iff-And, 67

 

                  69   (t,v) e eqx => (t,v) e x2 & t=v

                        Split, 68

 

                  70   (t,v) e x2 & t=v

                        Detach, 69, 60

 

                  71   t=v

                        Split, 70

 

                  72   u=v

                        Substitute, 66, 71

 

         As Required:

 

            73   (t,u) e eqx & (t,v) e eqx => u=v

                  4 Conclusion, 58

 

   

    Part 3

   

    As Required:

 

      74   ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e x & b2 e x

         => [(a1,b1) e eqx & (a1,b2) e eqx => b1=b2]]

            4 Conclusion, 54

 

      75   ALL(a1):ALL(b):[(a1,b) e eqx => a1 e x & b e x]

         & ALL(a1):[a1 e x => EXIST(b):[b e x & (a1,b) e eqx]]

            Join, 36, 53

 

      76   ALL(a1):ALL(b):[(a1,b) e eqx => a1 e x & b e x]

         & ALL(a1):[a1 e x => EXIST(b):[b e x & (a1,b) e eqx]]

         & ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e x & b2 e x

         => [(a1,b1) e eqx & (a1,b2) e eqx => b1=b2]]

            Join, 75, 74

 

      77   EXIST(fun):ALL(a1):ALL(b):[a1 e x & b e x

         => [fun(a1)=b <=> (a1,b) e eqx]]

            Detach, 23, 76

 

   

    Define: idx  (identity function on x)

 

      78   ALL(a1):ALL(b):[a1 e x & b e x

         => [idx(a1)=b <=> (a1,b) e eqx]]

            E Spec, 77

 

        

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

        

         Suppose...

 

            79   t e x

                  Premise

 

         Apply definiton of eqx

 

            80   t e x => EXIST(b):[b e x & (t,b) e eqx]

                  U Spec, 53

 

            81   EXIST(b):[b e x & (t,b) e eqx]

                  Detach, 80, 79

 

            82   u e x & (t,u) e eqx

                  E Spec, 81

 

            83   u e x

                  Split, 82

 

            84   (t,u) e eqx

                  Split, 82

 

         Apply definition of idx

 

            85   ALL(b):[t e x & b e x

             => [idx(t)=b <=> (t,b) e eqx]]

                  U Spec, 78

 

            86   t e x & u e x

             => [idx(t)=u <=> (t,u) e eqx]

                  U Spec, 85

 

            87   t e x & u e x

                  Join, 79, 83

 

            88   idx(t)=u <=> (t,u) e eqx

                  Detach, 86, 87

 

            89   [idx(t)=u => (t,u) e eqx] & [(t,u) e eqx => idx(t)=u]

                  Iff-And, 88

 

            90   (t,u) e eqx => idx(t)=u

                  Split, 89

 

            91   idx(t)=u

                  Detach, 90, 84

 

            92   idx(t) e x

                  Substitute, 91, 83

 

    As Required:

 

      93   ALL(a):[a e x => idx(a) e x]

            4 Conclusion, 79

 

        

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

        

         Suppose...

 

            94   t e x

                  Premise

 

            95   t e x => EXIST(b):[b e x & (t,b) e eqx]

                  U Spec, 53

 

            96   EXIST(b):[b e x & (t,b) e eqx]

                  Detach, 95, 94

 

            97   u e x & (t,u) e eqx

                  E Spec, 96

 

            98   u e x

                  Split, 97

 

            99   (t,u) e eqx

                  Split, 97

 

            100  ALL(b):[t e x & b e x

             => [idx(t)=b <=> (t,b) e eqx]]

                  U Spec, 78

 

            101  t e x & u e x

             => [idx(t)=u <=> (t,u) e eqx]

                  U Spec, 100

 

            102  t e x & u e x

                  Join, 94, 98

 

            103  idx(t)=u <=> (t,u) e eqx

                  Detach, 101, 102

 

            104  [idx(t)=u => (t,u) e eqx] & [(t,u) e eqx => idx(t)=u]

                  Iff-And, 103

 

            105  (t,u) e eqx => idx(t)=u

                  Split, 104

 

            106  idx(t)=u

                  Detach, 105, 99

 

            107  ALL(b):[(t,b) e eqx <=> (t,b) e x2 & t=b]

                  U Spec, 15

 

            108  (t,u) e eqx <=> (t,u) e x2 & t=u

                  U Spec, 107

 

            109  [(t,u) e eqx => (t,u) e x2 & t=u]

             & [(t,u) e x2 & t=u => (t,u) e eqx]

                  Iff-And, 108

 

            110  (t,u) e eqx => (t,u) e x2 & t=u

                  Split, 109

 

            111  (t,u) e x2 & t=u

                  Detach, 110, 99

 

            112  t=u

                  Split, 111

 

            113  idx(t)=t

                  Substitute, 112, 106

 

    As Required:

 

      114  ALL(a):[a e x => idx(a)=a]

            4 Conclusion, 94

 

        

         Prove: idx is a unique function on set x

        

         Let idx' be a function like idx such that...

 

            115  ALL(a):[a e x => idx'(a)=a]

                  Premise

 

            

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

            

             Suppose...

 

                  116  t e x

                        Premise

 

                  117  t e x => idx(t)=t

                        U Spec, 114

 

                  118  idx(t)=t

                        Detach, 117, 116

 

                  119  t e x => idx'(t)=t

                        U Spec, 115

 

                  120  idx'(t)=t

                        Detach, 119, 116

 

                  121  idx'(t)=idx(t)

                        Substitute, 118, 120

 

         As Required:

 

            122  ALL(a):[a e x => idx'(a)=idx(a)]

                  4 Conclusion, 116

 

    As Required:

   

    idx is a unique function on set x

 

      123  ALL(idx'):[ALL(a):[a e x => idx'(a)=a]

         => ALL(a):[a e x => idx'(a)=idx(a)]]

            4 Conclusion, 115

 

 

    Joining results...

 

      124  ALL(a):[a e x => idx(a) e x]

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

            Join, 93, 114

 

      125  ALL(a):[a e x => idx(a) e x]

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

         & ALL(idx'):[ALL(a):[a e x => idx'(a)=a]

         => ALL(a):[a e x => idx'(a)=idx(a)]]

            Join, 124, 123

 

As Required:

 

126  ALL(x):[Set(x) & EXIST(a):a e x

    => EXIST(idx):[ALL(a):[a e x => idx(a) e x]

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

    & ALL(idx'):[ALL(a):[a e x => idx'(a)=a]

    => ALL(a):[a e x => idx'(a)=idx(a)]]]]

      4 Conclusion, 1