THEOREM

*******

 

Given sets x and y we can construct the set fs consisting of all those function-like subsets of the Cartesian product of x and y.

 

For each element f e fs, we can prove the existence of a unique function g: x --> y such that g(a)=b <=> (a, b) in f.

 

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

     => EXIST(fs):[ALL(f):[f e fs

     <=> Set'(f)

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

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

     & ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y => [(a,b1) e f & (a,b2) e f => b1=b2]]]]

 

     & ALL(f):[f e fs => EXIST(g):[ALL(a):[a e x => g(a) e y]

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

 

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

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

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

 

 

By Dan Christensen

2022-01-06

 

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

 

 

PROOF

*****

 

    Let x and y be sets

 

      1     Set(x) & Set(y)

            Premise

 

      2     Set(x)

            Split, 1

 

      3     Set(y)

            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(y) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e y]]

            U Spec, 5

 

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

            Detach, 6, 1

 

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

            E Spec, 7

 

   

    Define: xy

 

      9     Set'(xy)

            Split, 8

 

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

            Split, 8

 

    Apply Powerset Axiom

 

      11   ALL(a):[Set'(a) => EXIST(b):[Set(b)

         & ALL(c):[c e b <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e a]]]]

            Power Set

 

      12   Set'(xy) => EXIST(b):[Set(b)

         & ALL(c):[c e b <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e xy]]]

            U Spec, 11

 

      13   EXIST(b):[Set(b)

         & ALL(c):[c e b <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e xy]]]

            Detach, 12, 9

 

      14   Set(pxy)

         & ALL(c):[c e pxy <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e xy]]

            E Spec, 13

 

   

    Define: pxy

 

      15   Set(pxy)

            Split, 14

 

      16   ALL(c):[c e pxy <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e xy]]

            Split, 14

 

   

    Apply Subset Axiom

 

      17   EXIST(fs):[Set(fs) & ALL(f):[f e fs <=> f e pxy & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e f]]

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

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

            Subset, 15

 

      18   Set(fs) & ALL(f):[f e fs <=> f e pxy & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e f]]

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

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

            E Spec, 17

 

   

    Define: fs

 

      19   Set(fs)

            Split, 18

 

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

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

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

            Split, 18

 

        

         Prove: ALL(f):[f e fs

                => Set'(f)

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

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

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

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

        

         Suppose...

 

            21   t e fs

                  Premise

 

         Apply definition of fs to get rid of pxy reference

 

            22   t e fs <=> t e pxy & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e t]]

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

             => [(a,b1) e t & (a,b2) e t => b1=b2]]]

                  U Spec, 20

 

            23   [t e fs => t e pxy & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e t]]

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

             => [(a,b1) e t & (a,b2) e t => b1=b2]]]]

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

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

             => [(a,b1) e t & (a,b2) e t => b1=b2]]] => t e fs]

                  Iff-And, 22

 

            24   t e fs => t e pxy & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e t]]

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

             => [(a,b1) e t & (a,b2) e t => b1=b2]]]

                  Split, 23

 

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

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

             => [(a,b1) e t & (a,b2) e t => b1=b2]]]

                  Detach, 24, 21

 

            26   t e pxy

                  Split, 25

 

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

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

             => [(a,b1) e t & (a,b2) e t => b1=b2]]

                  Split, 25

 

         Apply definition of pxy

 

            28   t e pxy <=> Set'(t) & ALL(d1):ALL(d2):[(d1,d2) e t => (d1,d2) e xy]

                  U Spec, 16

 

            29   [t e pxy => Set'(t) & ALL(d1):ALL(d2):[(d1,d2) e t => (d1,d2) e xy]]

             & [Set'(t) & ALL(d1):ALL(d2):[(d1,d2) e t => (d1,d2) e xy] => t e pxy]

                  Iff-And, 28

 

            30   t e pxy => Set'(t) & ALL(d1):ALL(d2):[(d1,d2) e t => (d1,d2) e xy]

                  Split, 29

 

            31   Set'(t) & ALL(d1):ALL(d2):[(d1,d2) e t => (d1,d2) e xy]

                  Detach, 30, 26

 

            32   Set'(t)

                  Split, 31

 

            33   ALL(d1):ALL(d2):[(d1,d2) e t => (d1,d2) e xy]

                  Split, 31

 

            

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

            

             Suppose...

 

                  34   (u,v) e t

                        Premise

 

             Apply definition of xy

 

                  35   ALL(d2):[(u,d2) e t => (u,d2) e xy]

                        U Spec, 33

 

                  36   (u,v) e t => (u,v) e xy

                        U Spec, 35

 

                  37   (u,v) e xy

                        Detach, 36, 34

 

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

                        U Spec, 10

 

                  39   (u,v) e xy <=> u e x & v e y

                        U Spec, 38

 

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

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

                        Iff-And, 39

 

                  41   (u,v) e xy => u e x & v e y

                        Split, 40

 

                  42   u e x & v e y

                        Detach, 41, 37

 

         As Required:

 

            43   ALL(a):ALL(b):[(a,b) e t => a e x & b e y]

                  4 Conclusion, 34

 

            44   Set'(t)

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

                  Join, 32, 43

 

            45   Set'(t)

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

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

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

             => [(a,b1) e t & (a,b2) e t => b1=b2]]]

                  Join, 44, 27

 

    As Required:

 

      46   ALL(f):[f e fs

         => Set'(f)

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

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

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

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

            4 Conclusion, 21

 

        

         Prove: ALL(f):[Set'(f)

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

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

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

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

                => f e fs]

        

         Suppose...

 

            47   Set'(t)

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

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

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

             => [(a,b1) e t & (a,b2) e t => b1=b2]]]

                  Premise

 

            48   Set'(t)

                  Split, 47

 

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

                  Split, 47

 

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

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

             => [(a,b1) e t & (a,b2) e t => b1=b2]]

                  Split, 47

 

         Apply definition of fs

 

            51   t e fs <=> t e pxy & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e t]]

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

             => [(a,b1) e t & (a,b2) e t => b1=b2]]]

                  U Spec, 20

 

            52   [t e fs => t e pxy & [ALL(a):[a e x => EXIST(b):[b e y & (a,b) e t]]

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

             => [(a,b1) e t & (a,b2) e t => b1=b2]]]]

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

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

             => [(a,b1) e t & (a,b2) e t => b1=b2]]] => t e fs]

                  Iff-And, 51

 

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

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

             => [(a,b1) e t & (a,b2) e t => b1=b2]]] => t e fs

                  Split, 52

 

         Apply definition of pxy

 

            54   t e pxy <=> Set'(t) & ALL(d1):ALL(d2):[(d1,d2) e t => (d1,d2) e xy]

                  U Spec, 16

 

            55   [t e pxy => Set'(t) & ALL(d1):ALL(d2):[(d1,d2) e t => (d1,d2) e xy]]

             & [Set'(t) & ALL(d1):ALL(d2):[(d1,d2) e t => (d1,d2) e xy] => t e pxy]

                  Iff-And, 54

 

         Sufficient: For t e pxy

 

            56   Set'(t) & ALL(d1):ALL(d2):[(d1,d2) e t => (d1,d2) e xy] => t e pxy

                  Split, 55

 

            

             Prove: ALL(a):ALL(b):[(a,b) e t => (a,b) e xy]

            

             Suppose...

 

                  57   (u,v) e t

                        Premise

 

             Apply definition of xy

 

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

                        U Spec, 10

 

                  59   (u,v) e xy <=> u e x & v e y

                        U Spec, 58

 

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

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

                        Iff-And, 59

 

                  61   u e x & v e y => (u,v) e xy

                        Split, 60

 

                  62   ALL(b):[(u,b) e t => u e x & b e y]

                        U Spec, 49

 

                  63   (u,v) e t => u e x & v e y

                        U Spec, 62

 

                  64   u e x & v e y

                        Detach, 63, 57

 

                  65   (u,v) e xy

                        Detach, 61, 64

 

         As Required:

 

            66   ALL(a):ALL(b):[(a,b) e t => (a,b) e xy]

                  4 Conclusion, 57

 

            67   Set'(t) & ALL(a):ALL(b):[(a,b) e t => (a,b) e xy]

                  Join, 48, 66

 

            68   t e pxy

                  Detach, 56, 67

 

            69   t e pxy

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

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

             => [(a,b1) e t & (a,b2) e t => b1=b2]]]

                  Join, 68, 50

 

            70   t e fs

                  Detach, 53, 69

 

    As Required:

 

      71   ALL(f):[Set'(f)

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

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

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

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

         => f e fs]

            4 Conclusion, 47

 

      72   ALL(f):[[f e fs

         => Set'(f)

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

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

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

         => [(a,b1) e f & (a,b2) e f => b1=b2]]]] & [Set'(f)

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

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

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

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

         => f e fs]]

            Join, 46, 71

 

    Alternatively Define: fs  (without pxy)

 

      73   ALL(f):[f e fs

         <=> Set'(f)

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

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

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

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

            Iff-And, 72

 

        

         Prove: ALL(f):[f e fs

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

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

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

        

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

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

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

        

         Suppose...

 

            74   f e fs

                  Premise

 

         Apply definition of fs

 

            75   f e fs

             <=> Set'(f)

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

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

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

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

                  U Spec, 73

 

            76   [f e fs => Set'(f)

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

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

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

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

             & [Set'(f)

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

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

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

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

                  Iff-And, 75

 

            77   f e fs => Set'(f)

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

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

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

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

                  Split, 76

 

            78   Set'(f)

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

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

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

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

                  Detach, 77, 74

 

            79   Set'(f)

                  Split, 78

 

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

                  Split, 78

 

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

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

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

                  Split, 78

 

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

                  Split, 81

 

            83   ALL(a):ALL(b1):ALL(b2):[a e x & b1 e y & b2 e y

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

                  Split, 81

 

         Apply Function Axiom

 

            84   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

 

            85   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]]]]

                  U Spec, 84

 

            86   ALL(cod):[Set'(f) & Set(x) & Set(cod)

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

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

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

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

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

                  U Spec, 85

 

            87   Set'(f) & Set(x) & Set(y)

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

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

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

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

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

                  U Spec, 86

 

            88   Set'(f) & Set(x)

                  Join, 79, 2

 

            89   Set'(f) & Set(x) & Set(y)

                  Join, 88, 3

 

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

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

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

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

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

                  Detach, 87, 89

 

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

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

                  Detach, 90, 81

 

         Define: g

 

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

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

                  E Spec, 91

 

            

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

            

             Suppose...

 

                  93   t e x

                        Premise

 

                  94   t e x => EXIST(b):[b e y & (t,b) e f]

                        U Spec, 82

 

                  95   EXIST(b):[b e y & (t,b) e f]

                        Detach, 94, 93

 

                  96   u e y & (t,u) e f

                        E Spec, 95

 

                  97   u e y

                        Split, 96

 

                  98   (t,u) e f

                        Split, 96

 

             Apply definition of g

 

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

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

                        U Spec, 92

 

                  100  t e x & u e y

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

                        U Spec, 99

 

                  101  t e x & u e y

                        Join, 93, 97

 

                  102  g(t)=u <=> (t,u) e f

                        Detach, 100, 101

 

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

                        Iff-And, 102

 

                  104  (t,u) e f => g(t)=u

                        Split, 103

 

                  105  g(t)=u

                        Detach, 104, 98

 

                  106  g(t) e y

                        Substitute, 105, 97

 

         As Required:

 

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

                  4 Conclusion, 93

 

            

             Prove: g is unique

            

             Suppose we have function g' such that...

 

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

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

                        Premise

 

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

                        Split, 108

 

                  110  ALL(a1):ALL(b):[a1 e x & b e y => [g'(a1)=b <=> (a1,b) e f]]

                        Split, 108

 

                

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

                

                 Suppose...

 

                        111  t e x

                              Premise

 

                        112  t e x => EXIST(b):[b e y & (t,b) e f]

                              U Spec, 82

 

                        113  EXIST(b):[b e y & (t,b) e f]

                              Detach, 112, 111

 

                        114  u e y & (t,u) e f

                              E Spec, 113

 

                        115  u e y

                              Split, 114

 

                        116  (t,u) e f

                              Split, 114

 

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

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

                              U Spec, 92

 

                        118  t e x & u e y

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

                              U Spec, 117

 

                        119  t e x & u e y

                              Join, 111, 115

 

                        120  g(t)=u <=> (t,u) e f

                              Detach, 118, 119

 

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

                              Iff-And, 120

 

                        122  (t,u) e f => g(t)=u

                              Split, 121

 

                        123  g(t)=u

                              Detach, 122, 116

 

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

                              U Spec, 110

 

                        125  t e x & u e y => [g'(t)=u <=> (t,u) e f]

                              U Spec, 124

 

                        126  t e x & u e y

                              Join, 111, 115

 

                        127  g'(t)=u <=> (t,u) e f

                              Detach, 125, 126

 

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

                              Iff-And, 127

 

                        129  (t,u) e f => g'(t)=u

                              Split, 128

 

                        130  g'(t)=u

                              Detach, 129, 116

 

                        131  g'(t)=g(t)

                              Substitute, 123, 130

 

             As Required:

 

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

                        4 Conclusion, 111

 

         As Required:

 

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

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

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

                  4 Conclusion, 108

 

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

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

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

                  Join, 107, 92

 

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

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

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

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

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

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

                  Join, 134, 133

 

    As Required:

 

      136  ALL(f):[f e fs

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

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

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

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

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

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

            4 Conclusion, 74

 

    Joining results...

 

      137  ALL(f):[f e fs

         <=> Set'(f)

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

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

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

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

         & ALL(f):[f e fs

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

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

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

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

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

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

            Join, 73, 136

 

 

As Required:

 

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

    => EXIST(fs):[ALL(f):[f e fs

    <=> Set'(f)

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

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

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

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

    & ALL(f):[f e fs

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

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

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

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

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

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

      4 Conclusion, 1