THEOREM

*******

 

On every set, there is exists a unique empty function

 

     ALL(x):[Set(x)

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

     & ALL(f1):ALL(f2):[ALL(a):[a e null => f1(a) e x] & ALL(a):[a e null => f2(a) e x] => f1=f2]]

 

OUTLINE

*******

 

1. Prove: EXIST(f):ALL(a):[a e null => f(a) e x] (Line 1-71)

 

2. ALL(f1):ALL(f2):[ALL(a):[a e null => f1(a) e x] & ALL(a):[a e null => f2(a) e x] => f1=f2] (Line 72-95)

 

 

By Dan Christensen

2022-04-02

 

Homepage: http://www.dcproof.com

 

 

PROOF

*****

 

Define: Equality of functions (1 variable)

 

Only functions with the same domain and codomain are comparable here.

 

1     ALL(dom):ALL(cod):ALL(f):ALL(g):[Set(dom) & Set(cod) & ALL(a):[a e dom => f(a) e cod] & ALL(a):[a e dom => g(a) e cod]

    => [f=g <=> ALL(a):[a e dom => f(a)=g(a)]]]

      Axiom

 

 

Define: null  (The empty set)

 

2     Set(null)

      Axiom

 

3     ALL(a):~a e null

      Axiom

 

   

    Prove: ALL(x):[Set(x)

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

           & ALL(f1):ALL(f2):[ALL(a):[a e null => f1(a) e x] & ALL(a):[a e null => f2(a) e x] => f1=f2]]

   

    Let x be an arbitrary set

 

      4     Set(x)

            Premise

 

    Apply the Cartesian Producut Axiom

 

      5     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

 

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

            U Spec, 5

 

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

            U Spec, 6

 

      8     Set(null) & Set(x)

            Join, 2, 4

 

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

            Detach, 7, 8

 

      10   Set'(nx) & ALL(c1):ALL(c2):[(c1,c2) e nx <=> c1 e null & c2 e x]

            E Spec, 9

 

   

    Define: nx  (The Cartesian product of null and x)

 

      11   Set'(nx)

            Split, 10

 

      12   ALL(c1):ALL(c2):[(c1,c2) e nx <=> c1 e null & c2 e x]

            Split, 10

 

        

         Prove: nx is an empty set of ordered pairs

        

         Suppose to the contrary...

 

            13   (t,u) e nx

                  Premise

 

         Apply the definition of nx

 

            14   ALL(c2):[(t,c2) e nx <=> t e null & c2 e x]

                  U Spec, 12

 

            15   (t,u) e nx <=> t e null & u e x

                  U Spec, 14

 

            16   [(t,u) e nx => t e null & u e x]

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

                  Iff-And, 15

 

            17   (t,u) e nx => t e null & u e x

                  Split, 16

 

            18   t e null & u e x

                  Detach, 17, 13

 

            19   t e null

                  Split, 18

 

            20   ~t e null

                  U Spec, 3

 

            21   t e null & ~t e null

                  Join, 19, 20

 

    As Required:

 

      22   ~EXIST(a):EXIST(b):(a,b) e nx

            4 Conclusion, 13

 

      23   ~~ALL(a):~EXIST(b):(a,b) e nx

            Quant, 22

 

      24   ALL(a):~EXIST(b):(a,b) e nx

            Rem DNeg, 23

 

      25   ALL(a):~~ALL(b):~(a,b) e nx

            Quant, 24

 

   

    nx is an empty set of ordered pairs

 

      26   ALL(a):ALL(b):~(a,b) e nx

            Rem DNeg, 25

 

   

    Prove: nx is the graph of an empty function

   

    Apply Function Axiom (1 variable)

 

      27   ALL(dom):ALL(cod):ALL(gra):[Set(dom) & Set(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

 

      28   ALL(cod):ALL(gra):[Set(null) & Set(cod) & Set'(gra)

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

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

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

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

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

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

            U Spec, 27

 

      29   ALL(gra):[Set(null) & Set(x) & Set'(gra)

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

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

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

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

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

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

            U Spec, 28

 

      30   Set(null) & Set(x) & Set'(nx)

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

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

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

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

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

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

            U Spec, 29

 

      31   Set(null) & Set(x)

            Join, 2, 4

 

      32   Set(null) & Set(x) & Set'(nx)

            Join, 31, 11

 

   

    Sufficient: For functionality of nx  (Each precondition is vacuously true)

 

      33   ALL(a1):ALL(b):[(a1,b) e nx => a1 e null & b e x]

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

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

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

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

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

            Detach, 30, 32

 

        

         Part 1

        

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

        

         Suppose...

 

            34   (t,u) e nx

                  Premise

 

            35   ALL(b):~(t,b) e nx

                  U Spec, 26

 

            36   ~(t,u) e nx

                  U Spec, 35

 

            37   ~(t,u) e nx => t e null & u e x

                  Arb Cons, 34

 

            38   t e null & u e x

                  Detach, 37, 36

 

    Part 1

   

    As Required:

 

      39   ALL(a1):ALL(b):[(a1,b) e nx => a1 e null & b e x]

            4 Conclusion, 34

 

        

         Part 2

        

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

        

         Suppose...

 

            40   t e null

                  Premise

 

            41   ~t e null

                  U Spec, 3

 

            42   ~t e null => EXIST(b):[b e x & (t,b) e nx]

                  Arb Cons, 40

 

            43   EXIST(b):[b e x & (t,b) e nx]

                  Detach, 42, 41

 

    Part 2

   

    As Required:

 

      44   ALL(a1):[a1 e null => EXIST(b):[b e x & (a1,b) e nx]]

            4 Conclusion, 40

 

        

         Part 3

        

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

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

        

         Suppose...

 

            45   t e null & u1 e x & u2 e x

                  Premise

 

            46   t e null

                  Split, 45

 

            47   ~t e null

                  U Spec, 3

 

            48   ~t e null => [(t,u1) e nx & (t,u2) e nx => u1=u2]

                  Arb Cons, 46

 

            49   (t,u1) e nx & (t,u2) e nx => u1=u2

                  Detach, 48, 47

 

    Part 3

   

    As Required:

 

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

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

            4 Conclusion, 45

 

   

    Joining results...

 

      51   ALL(a1):ALL(b):[(a1,b) e nx => a1 e null & b e x]

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

            Join, 39, 44

 

      52   ALL(a1):ALL(b):[(a1,b) e nx => a1 e null & b e x]

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

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

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

            Join, 51, 50

 

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

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

            Detach, 33, 52

 

   

    Define: f  (in terms of nx)

 

      54   ALL(a1):ALL(b):[a1 e null & b e x

         => [f(a1)=b <=> (a1,b) e nx]]

            E Spec, 53

 

        

         Prove: ALL(a):[a e null => f(a) e x]  (f is an empty function)

        

         Suppose...

 

            55   t e null

                  Premise

 

         Apply previous result

 

            56   t e null => EXIST(b):[b e x & (t,b) e nx]

                  U Spec, 44

 

            57   EXIST(b):[b e x & (t,b) e nx]

                  Detach, 56, 55

 

            58   u e x & (t,u) e nx

                  E Spec, 57

 

            59   u e x

                  Split, 58

 

            60   (t,u) e nx

                  Split, 58

 

         Apply definition of f

 

            61   ALL(b):[t e null & b e x

             => [f(t)=b <=> (t,b) e nx]]

                  U Spec, 54

 

            62   t e null & u e x

             => [f(t)=u <=> (t,u) e nx]

                  U Spec, 61

 

            63   t e null & u e x

                  Join, 55, 59

 

            64   f(t)=u <=> (t,u) e nx

                  Detach, 62, 63

 

            65   [f(t)=u => (t,u) e nx] & [(t,u) e nx => f(t)=u]

                  Iff-And, 64

 

            66   f(t)=u => (t,u) e nx

                  Split, 65

 

            67   (t,u) e nx => f(t)=u

                  Split, 65

 

            68   f(t)=u

                  Detach, 67, 60

 

            69   f(t) e x

                  Substitute, 68, 59

 

    As Required:

 

      70   ALL(a):[a e null => f(a) e x]

            4 Conclusion, 55

 

   

    As Required:

 

      71   EXIST(f):ALL(a):[a e null => f(a) e x]

            E Gen, 70

 

        

         Prove: ALL(f1):ALL(f2):[ALL(a):[a e null => f1(a) e x] & ALL(a):[a e null => f2(a) e x] => f1=f2]

        

         Suppose...

 

            72   ALL(a):[a e null => f1(a) e x] & ALL(a):[a e null => f2(a) e x]

                  Premise

 

            73   ALL(a):[a e null => f1(a) e x]

                  Split, 72

 

            74   ALL(a):[a e null => f2(a) e x]

                  Split, 72

 

         Apply definition of function equality

 

            75   ALL(cod):ALL(f):ALL(g):[Set(null) & Set(cod) & ALL(a):[a e null => f(a) e cod] & ALL(a):[a e null => g(a) e cod]

             => [f=g <=> ALL(a):[a e null => f(a)=g(a)]]]

                  U Spec, 1

 

            76   ALL(f):ALL(g):[Set(null) & Set(x) & ALL(a):[a e null => f(a) e x] & ALL(a):[a e null => g(a) e x]

             => [f=g <=> ALL(a):[a e null => f(a)=g(a)]]]

                  U Spec, 75

 

            77   ALL(g):[Set(null) & Set(x) & ALL(a):[a e null => f1(a) e x] & ALL(a):[a e null => g(a) e x]

             => [f1=g <=> ALL(a):[a e null => f1(a)=g(a)]]]

                  U Spec, 76

 

            78   Set(null) & Set(x) & ALL(a):[a e null => f1(a) e x] & ALL(a):[a e null => f2(a) e x]

             => [f1=f2 <=> ALL(a):[a e null => f1(a)=f2(a)]]

                  U Spec, 77

 

            79   Set(null) & Set(x)

                  Join, 2, 4

 

            80   Set(null) & Set(x)

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

                  Join, 79, 73

 

            81   Set(null) & Set(x)

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

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

                  Join, 80, 74

 

            82   f1=f2 <=> ALL(a):[a e null => f1(a)=f2(a)]

                  Detach, 78, 81

 

            83   [f1=f2 => ALL(a):[a e null => f1(a)=f2(a)]]

             & [ALL(a):[a e null => f1(a)=f2(a)] => f1=f2]

                  Iff-And, 82

 

            84   ALL(a):[a e null => f1(a)=f2(a)] => f1=f2

                  Split, 83

 

            

             Prove: ALL(a):[a e null => f1(a)=f2(a)]

            

             Suppose...

 

                  85   t e null

                        Premise

 

             Apply definition of f1

 

                  86   t e null => f1(t) e x

                        U Spec, 73

 

                  87   f1(t) e x

                        Detach, 86, 85

 

             Apply definition of f2

 

                  88   t e null => f2(t) e x

                        U Spec, 74

 

                  89   f2(t) e x

                        Detach, 88, 85

 

                  90   ~t e null

                        U Spec, 3

 

                  91   ~t e null => f1(t)=f2(t)

                        Arb Cons, 85

 

                  92   f1(t)=f2(t)

                        Detach, 91, 90

 

         As Required:

 

            93   ALL(a):[a e null => f1(a)=f2(a)]

                  4 Conclusion, 85

 

            94   f1=f2

                  Detach, 84, 93

 

    As Required:

 

      95   ALL(f1):ALL(f2):[ALL(a):[a e null => f1(a) e x] & ALL(a):[a e null => f2(a) e x]

         => f1=f2]

            4 Conclusion, 72

 

    Joining results...

 

      96   EXIST(f):ALL(a):[a e null => f(a) e x]

         & ALL(f1):ALL(f2):[ALL(a):[a e null => f1(a) e x] & ALL(a):[a e null => f2(a) e x]

         => f1=f2]

            Join, 71, 95

 

 

As Required:

 

97   ALL(x):[Set(x)

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

    & ALL(f1):ALL(f2):[ALL(a):[a e null => f1(a) e x] & ALL(a):[a e null => f2(a) e x]

    => f1=f2]]

      4 Conclusion, 4