"Definition 3.3.1 (Functions). Let X, Y be sets, and let P(x, y) be a property pertaining to an object x e  X and an object y e  Y, such that for every x e X, there is exactly one y e  Y for which P(x, y) is true (this is sometimes known as the vertical line test). Then we define the function f : X e  Y defined by P on the domain X and range Y to be the object which, given any input x e X, assigns an output f(x) e Y, defined to be the unique object f(x) for which P(x, f(x)) is true. Thus, for any x e X and y e Y, y = f(x) <=> P(x, y) is true."

 

Terence Tao, "Analysis I," p.49

 

THEOREM

*******

 

We can formalize Tao’s definition here and prove it as theorem in DC Proof:

 

   ALL(x):ALL(y):[Set(x) & Set(y)

   & ALL(a):[a e x => EXIST(b):[b e y & P(a,b)]]

   & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y => [P(a,b) & P(a,c) => b=c]]

 

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

 

By Dan Christensen

2022-01-10

 

 

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

 

 

PROOF

*****

 

The proof makes use (on line 52) of the following Function Axiom (for one variable):

 

   ALL(f):ALL(dom):ALL(cod):[Set'(f) & Set(dom) & Set(cod)

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

   & ALL(a1):ALL(b1):ALL(b2):[a1 e dom & b1 e cod & b2 e cod => [(a1,b1) e f & (a1,b2) e f => b1=b2]]

 

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

 

where

 

   f = a set of ordered pairs

   dom = the domain of the required function

   cod = the codomain of the required function

   fun = the name of the required function

 

This axiom gives the sufficient conditions for the existence of a function mapping the domain set to the codomain set.

 

   

    Suppose we have sets x and y and binary predicate P such that...

 

      1     Set(x) & Set(y)

         & ALL(a):[a e x => EXIST(b):[b e y & P(a,b)]]

         & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y => [P(a,b) & P(a,c) => b=c]]

            Premise

 

    x is a set

 

      2     Set(x)

            Split, 1

 

    y is a set

 

      3     Set(y)

            Split, 1

 

    P is binary predicate such that:

 

      4     ALL(a):[a e x => EXIST(b):[b e y & P(a,b)]]

            Split, 1

 

      5     ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y => [P(a,b) & P(a,c) => b=c]]

            Split, 1

 

   

    Apply Cartesian Product Axiom

 

      6     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

 

      7     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, 6

 

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

            U Spec, 7

 

      9     Set(x) & Set(y)

            Join, 2, 3

 

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

            Detach, 8, 9

 

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

            E Spec, 10

 

   

    Define: xy

 

      12   Set'(xy)

            Split, 11

 

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

            Split, 11

 

    Apply Subset Axiom

 

      14   EXIST(p):[Set'(p) & ALL(a):ALL(b):[(a,b) e p <=> (a,b) e xy & P(a,b)]]

            Subset, 12

 

      15   Set'(p) & ALL(a):ALL(b):[(a,b) e p <=> (a,b) e xy & P(a,b)]

            E Spec, 14

 

   

    Define: p

 

      16   Set'(p)

            Split, 15

 

      17   ALL(a):ALL(b):[(a,b) e p <=> (a,b) e xy & P(a,b)]

            Split, 15

 

        

         Recast without to reference to xy

        

         Suppose...

 

            18   (t,u) e p

                  Premise

 

            19   ALL(b):[(t,b) e p <=> (t,b) e xy & P(t,b)]

                  U Spec, 17

 

         Apply definition of p

 

            20   (t,u) e p <=> (t,u) e xy & P(t,u)

                  U Spec, 19

 

            21   [(t,u) e p => (t,u) e xy & P(t,u)]

             & [(t,u) e xy & P(t,u) => (t,u) e p]

                  Iff-And, 20

 

            22   (t,u) e p => (t,u) e xy & P(t,u)

                  Split, 21

 

            23   (t,u) e xy & P(t,u)

                  Detach, 22, 18

 

            24   (t,u) e xy

                  Split, 23

 

            25   P(t,u)

                  Split, 23

 

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

                  U Spec, 13

 

         Apply definition of xy

 

            27   (t,u) e xy <=> t e x & u e y

                  U Spec, 26

 

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

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

                  Iff-And, 27

 

            29   (t,u) e xy => t e x & u e y

                  Split, 28

 

            30   t e x & u e y

                  Detach, 29, 24

 

            31   t e x & u e y & P(t,u)

                  Join, 30, 25

 

    As Required:

 

      32   ALL(a):ALL(b):[(a,b) e p => a e x & b e y & P(a,b)]

            4 Conclusion, 18

 

        

         Prove: ALL(a):ALL(b):[a e x & b e y & P(a,b) => (a,b) e p]

        

         Suppose...

 

            33   t e x & u e y & P(t,u)

                  Premise

 

            34   t e x

                  Split, 33

 

            35   u e y

                  Split, 33

 

            36   P(t,u)

                  Split, 33

 

         Apply definition of p

 

            37   ALL(b):[(t,b) e p <=> (t,b) e xy & P(t,b)]

                  U Spec, 17

 

            38   (t,u) e p <=> (t,u) e xy & P(t,u)

                  U Spec, 37

 

            39   [(t,u) e p => (t,u) e xy & P(t,u)]

             & [(t,u) e xy & P(t,u) => (t,u) e p]

                  Iff-And, 38

 

            40   (t,u) e xy & P(t,u) => (t,u) e p

                  Split, 39

 

         Apply definition of xy

 

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

                  U Spec, 13

 

            42   (t,u) e xy <=> t e x & u e y

                  U Spec, 41

 

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

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

                  Iff-And, 42

 

            44   t e x & u e y => (t,u) e xy

                  Split, 43

 

            45   t e x & u e y

                  Join, 34, 35

 

            46   (t,u) e xy

                  Detach, 44, 45

 

            47   (t,u) e xy & P(t,u)

                  Join, 46, 36

 

            48   (t,u) e p

                  Detach, 40, 47

 

    As Required:

 

      49   ALL(a):ALL(b):[a e x & b e y & P(a,b) => (a,b) e p]

            4 Conclusion, 33

 

      50   ALL(a):ALL(b):[[(a,b) e p => a e x & b e y & P(a,b)] & [a e x & b e y & P(a,b) => (a,b) e p]]

            Join, 32, 49

 

    Alternatively Define: p

 

      51   ALL(a):ALL(b):[(a,b) e p <=> a e x & b e y & P(a,b)]

            Iff-And, 50

 

    Apply Function Axiom

 

      52   ALL(f):ALL(dom):ALL(cod):[Set'(f) & Set(dom) & Set(cod)

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

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

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

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

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

            Function

 

      53   ALL(dom):ALL(cod):[Set'(p) & Set(dom) & Set(cod)

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

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

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

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

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

            U Spec, 52

 

      54   ALL(cod):[Set'(p) & Set(x) & Set(cod)

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

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

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

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

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

            U Spec, 53

 

      55   Set'(p) & Set(x) & Set(y)

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

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

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

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

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

            U Spec, 54

 

      56   Set'(p) & Set(x)

            Join, 16, 2

 

      57   Set'(p) & Set(x) & Set(y)

            Join, 56, 3

 

   

    Sufficient: For existence of function

 

      58   ALL(a1):[a1 e x => EXIST(b):[b e y & (a1,b) e p]]

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

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

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

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

            Detach, 55, 57

 

        

         Part 1

        

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

        

         Suppose...

 

            59   t e x

                  Premise

 

         Apply initial premise

 

            60   t e x => EXIST(b):[b e y & P(t,b)]

                  U Spec, 4

 

            61   EXIST(b):[b e y & P(t,b)]

                  Detach, 60, 59

 

            62   u e y & P(t,u)

                  E Spec, 61

 

            63   u e y

                  Split, 62

 

            64   P(t,u)

                  Split, 62

 

         Apply alternative definition of p

 

            65   ALL(b):[(t,b) e p <=> t e x & b e y & P(t,b)]

                  U Spec, 51

 

            66   (t,u) e p <=> t e x & u e y & P(t,u)

                  U Spec, 65

 

            67   [(t,u) e p => t e x & u e y & P(t,u)]

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

                  Iff-And, 66

 

            68   (t,u) e p => t e x & u e y & P(t,u)

                  Split, 67

 

            69   t e x & u e y & P(t,u) => (t,u) e p

                  Split, 67

 

            70   t e x & u e y

                  Join, 59, 63

 

            71   t e x & u e y & P(t,u)

                  Join, 70, 64

 

            72   (t,u) e p

                  Detach, 69, 71

 

            73   u e y & (t,u) e p

                  Join, 63, 72

 

    As Required:

 

      74   ALL(a):[a e x => EXIST(b):[b e y & (a,b) e p]]

            4 Conclusion, 59

 

        

         Part 2

        

         Prove: ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e y & b2 e y => [(a1,b1) e p & (a1,b2) e p => b1=b2]]

        

         Suppose...

 

            75   t e x & u1 e y & u2 e y

                  Premise

 

            76   t e x

                  Split, 75

 

            77   u1 e y

                  Split, 75

 

            78   u2 e y

                  Split, 75

 

            

             Prove: (t,u1) e p & (t,u2) e p => u1=u2

            

             Suppose...

 

                  79   (t,u1) e p & (t,u2) e p

                        Premise

 

                  80   (t,u1) e p

                        Split, 79

 

                  81   (t,u2) e p

                        Split, 79

 

             Apply initial premise

 

                  82   ALL(b):ALL(c):[t e x & b e y & c e y => [P(t,b) & P(t,c) => b=c]]

                        U Spec, 5

 

                  83   ALL(c):[t e x & u1 e y & c e y => [P(t,u1) & P(t,c) => u1=c]]

                        U Spec, 82

 

                  84   t e x & u1 e y & u2 e y => [P(t,u1) & P(t,u2) => u1=u2]

                        U Spec, 83

 

             Sufficient: For u1=u2

 

                  85   P(t,u1) & P(t,u2) => u1=u2

                        Detach, 84, 75

 

             Apply definition of p

 

                  86   ALL(b):[(t,b) e p <=> t e x & b e y & P(t,b)]

                        U Spec, 51

 

                  87   (t,u1) e p <=> t e x & u1 e y & P(t,u1)

                        U Spec, 86

 

                  88   [(t,u1) e p => t e x & u1 e y & P(t,u1)]

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

                        Iff-And, 87

 

                  89   (t,u1) e p => t e x & u1 e y & P(t,u1)

                        Split, 88

 

                  90   t e x & u1 e y & P(t,u1)

                        Detach, 89, 80

 

                  91   P(t,u1)

                        Split, 90

 

                  92   (t,u2) e p <=> t e x & u2 e y & P(t,u2)

                        U Spec, 86

 

                  93   [(t,u2) e p => t e x & u2 e y & P(t,u2)]

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

                        Iff-And, 92

 

                  94   (t,u2) e p => t e x & u2 e y & P(t,u2)

                        Split, 93

 

                  95   t e x & u2 e y & P(t,u2)

                        Detach, 94, 81

 

                  96   P(t,u2)

                        Split, 95

 

                  97   P(t,u1) & P(t,u2)

                        Join, 91, 96

 

                  98   u1=u2

                        Detach, 85, 97

 

         As Required:

 

            99   (t,u1) e p & (t,u2) e p => u1=u2

                  4 Conclusion, 79

 

    As Required:

 

      100  ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

         => [(a,b) e p & (a,c) e p => b=c]]

            4 Conclusion, 75

 

   

    Joining results...

 

      101  ALL(a):[a e x => EXIST(b):[b e y & (a,b) e p]]

         & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y

         => [(a,b) e p & (a,c) e p => b=c]]

            Join, 74, 100

 

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

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

            Detach, 58, 101

 

   

    Define: f

 

      103  ALL(a1):ALL(b):[a1 e x & b e y

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

            E Spec, 102

 

        

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

        

         Suppose...

 

            104  t e x & u e y

                  Premise

 

         Apply definition of f

 

            105  ALL(b):[t e x & b e y

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

                  U Spec, 103

 

            106  t e x & u e y

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

                  U Spec, 105

 

            107  f(t)=u <=> (t,u) e p

                  Detach, 106, 104

 

            

             Prove: f(t)=u => P(t,u)

            

             Suppose...

 

                  108  f(t)=u

                        Premise

 

                  109  [f(t)=u => (t,u) e p] & [(t,u) e p => f(t)=u]

                        Iff-And, 107

 

                  110  f(t)=u => (t,u) e p

                        Split, 109

 

                  111  (t,u) e p

                        Detach, 110, 108

 

             Apply definition of p

 

                  112  ALL(b):[(t,b) e p <=> t e x & b e y & P(t,b)]

                        U Spec, 51

 

                  113  (t,u) e p <=> t e x & u e y & P(t,u)

                        U Spec, 112

 

                  114  [(t,u) e p => t e x & u e y & P(t,u)]

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

                        Iff-And, 113

 

                  115  (t,u) e p => t e x & u e y & P(t,u)

                        Split, 114

 

                  116  t e x & u e y & P(t,u)

                        Detach, 115, 111

 

                  117  P(t,u)

                        Split, 116

 

         As Required:

 

            118  f(t)=u => P(t,u)

                  4 Conclusion, 108

 

            

             Prove: P(t,y) => f(t)=u

            

             Suppose...

 

                  119  P(t,u)

                        Premise

 

             Apply definition of f

 

                  120  ALL(b):[t e x & b e y

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

                        U Spec, 103

 

                  121  t e x & u e y

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

                        U Spec, 120

 

                  122  f(t)=u <=> (t,u) e p

                        Detach, 121, 104

 

                  123  [f(t)=u => (t,u) e p] & [(t,u) e p => f(t)=u]

                        Iff-And, 122

 

                  124  (t,u) e p => f(t)=u

                        Split, 123

 

             Apply definition of p

 

                  125  ALL(b):[(t,b) e p <=> t e x & b e y & P(t,b)]

                        U Spec, 51

 

                  126  (t,u) e p <=> t e x & u e y & P(t,u)

                        U Spec, 125

 

                  127  [(t,u) e p => t e x & u e y & P(t,u)]

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

                        Iff-And, 126

 

                  128  (t,u) e p => t e x & u e y & P(t,u)

                        Split, 127

 

                  129  t e x & u e y & P(t,u) => (t,u) e p

                        Split, 127

 

                  130  t e x & u e y & P(t,u)

                        Join, 104, 119

 

                  131  (t,u) e p

                        Detach, 129, 130

 

                  132  f(t)=u

                        Detach, 124, 131

 

         As Required:

 

            133  P(t,u) => f(t)=u

                  4 Conclusion, 119

 

        

         Joining results...

 

            134  [f(t)=u => P(t,u)] & [P(t,u) => f(t)=u]

                  Join, 118, 133

 

            135  f(t)=u <=> P(t,u)

                  Iff-And, 134

 

    As Required:

 

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

            4 Conclusion, 104

 

 

As Required:

 

137  ALL(x):ALL(y):[Set(x) & Set(y)

    & ALL(a):[a e x => EXIST(b):[b e y & P(a,b)]]

    & ALL(a):ALL(b):ALL(c):[a e x & b e y & c e y => [P(a,b) & P(a,c) => b=c]]

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

      4 Conclusion, 1