THEOREM

*******

 

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

=> EXIST(fxy):[Set(fxy) & ALL(f):[f e fxy <=> ALL(a1):[a1 e x => f(a1) e y]]

 

& ALL(fxy'):[Set(fxy') & ALL(f):[f e fxy' <=> ALL(a1):[a1 e x => f(a1) e y]] => fxy'=fxy]]]

 

 

By Dan Christensen

2022-03-23

 

http://www.dcproof.com

 

 

PROOF

*****

 

    Suppose x and y are sets

 

      1     Set(x) & Set(y)

            Premise

 

    Apply Function Set Axiom (for 1 variable)

 

      2     ALL(dom):ALL(cod):[Set(dom) & Set(cod)

         => EXIST(fsp):[Set(fsp) & ALL(f):[f e fsp <=> ALL(a1):[a1 e dom => f(a1) e cod]]]]

            Fn Space

 

      3     ALL(cod):[Set(x) & Set(cod)

         => EXIST(fsp):[Set(fsp) & ALL(f):[f e fsp <=> ALL(a1):[a1 e x => f(a1) e cod]]]]

            U Spec, 2

 

      4     Set(x) & Set(y)

         => EXIST(fsp):[Set(fsp) & ALL(f):[f e fsp <=> ALL(a1):[a1 e x => f(a1) e y]]]

            U Spec, 3

 

      5     EXIST(fsp):[Set(fsp) & ALL(f):[f e fsp <=> ALL(a1):[a1 e x => f(a1) e y]]]

            Detach, 4, 1

 

      6     Set(fxy) & ALL(f):[f e fxy <=> ALL(a1):[a1 e x => f(a1) e y]]

            E Spec, 5

 

   

    Define: fxy  (Function space of all functions f: x --> y)

 

      7     Set(fxy)

            Split, 6

 

      8     ALL(f):[f e fxy <=> ALL(a1):[a1 e x => f(a1) e y]]

            Split, 6

 

        

        

         Define: fxy'  (Another function space of all functions f: x --> y)

 

            9     Set(fxy') & ALL(f):[f e fxy' <=> ALL(a1):[a1 e x => f(a1) e y]]

                  Premise

 

        

         Define: fxy'

 

            10   Set(fxy')

                  Split, 9

 

            11   ALL(f):[f e fxy' <=> ALL(a1):[a1 e x => f(a1) e y]]

                  Split, 9

 

        

         Sufficient: For fxy'=fxy

 

            18   ALL(c):[c e fxy' <=> c e fxy] => fxy'=fxy

                  Split, 17

 

         As Required:

 

            28   ALL(f):[f e fxy' => f e fxy]

                  5 Conclusion, 19

 

         As Required:

 

            38   ALL(f):[f e fxy => f e fxy']

                  5 Conclusion, 29

 

            40   ALL(f):[f e fxy' <=> f e fxy]

                  Iff-And, 39

 

            41   fxy'=fxy

                  Detach, 18, 40

 

      42   ALL(fxy'):[Set(fxy') & ALL(f):[f e fxy' <=> ALL(a1):[a1 e x => f(a1) e y]]

         => fxy'=fxy]

            4 Conclusion, 9

 

    Joining results...

 

      43   Set(fxy) & ALL(f):[f e fxy <=> ALL(a1):[a1 e x => f(a1) e y]]

         & ALL(fxy'):[Set(fxy') & ALL(f):[f e fxy' <=> ALL(a1):[a1 e x => f(a1) e y]]

         => fxy'=fxy]

            Join, 6, 42

 

 

As Required:

 

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

    => EXIST(fxy):[Set(fxy) & ALL(f):[f e fxy <=> ALL(a1):[a1 e x => f(a1) e y]]

    & ALL(fxy'):[Set(fxy') & ALL(f):[f e fxy' <=> ALL(a1):[a1 e x => f(a1) e y]]

    => fxy'=fxy]]]

      4 Conclusion, 1