THEOREM

*******

 

Suppose we have functions f1: x --> y and f2: y --> z

 

Then there exists a composition of f1 and f2, f2 o f1: x --> z

 

 

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

 

 

AXIOM

*****

 

Function Axiom for 1 variable

 

1     ALL(f):ALL(a):ALL(b):[Set'(f) & Set(a) & Set(b)

    => [ALL(c):ALL(d):[(c,d) e f => c e a & d e b]

    & ALL(c):[c e a => EXIST(d):[d e b & (c,d) e f]]

    & ALL(c):ALL(d1):ALL(d2):[(c,d1) e f & (c,d2) e f => d1=d2]

    => ALL(c):ALL(d):[c e a & d e b => [d=f(c) <=> (c,d) e f]]]]

      Axiom

 

   

    PROOF

    *****

   

    Suppose...

 

      2     Set(x) & Set(y) & Set(z)

         & ALL(d):[d e x => f1(d) e y]

         & ALL(d):[d e y => f2(d) e z]

            Premise

 

      3     Set(x)

            Split, 2

 

      4     Set(y)

            Split, 2

 

      5     Set(z)

            Split, 2

 

      6     ALL(d):[d e x => f1(d) e y]

            Split, 2

 

      7     ALL(d):[d e y => f2(d) e z]

            Split, 2

 

    Apply Cartesian Product Axiom

 

      8     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

 

      9     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, 8

 

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

            U Spec, 9

 

      11   Set(x) & Set(z)

            Join, 3, 5

 

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

            Detach, 10, 11

 

      13   Set'(xz) & ALL(c1):ALL(c2):[(c1,c2) e xz <=> c1 e x & c2 e z]

            E Spec, 12

 

    Define: xz

 

      14   Set'(xz)

            Split, 13

 

      15   ALL(c1):ALL(c2):[(c1,c2) e xz <=> c1 e x & c2 e z]

            Split, 13

 

    Apply Subset Axiom

 

      16   EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e xz & b=f2(f1(a))]]

            Subset, 14

 

      17   Set'(f2f1) & ALL(a):ALL(b):[(a,b) e f2f1 <=> (a,b) e xz & b=f2(f1(a))]

            E Spec, 16

 

    Define: f2f1

 

      18   Set'(f2f1)

            Split, 17

 

      19   ALL(a):ALL(b):[(a,b) e f2f1 <=> (a,b) e xz & b=f2(f1(a))]

            Split, 17

 

    Apply Function Axiom

 

      20   ALL(a):ALL(b):[Set'(f2f1) & Set(a) & Set(b)

         => [ALL(c):ALL(d):[(c,d) e f2f1 => c e a & d e b]

         & ALL(c):[c e a => EXIST(d):[d e b & (c,d) e f2f1]]

         & ALL(c):ALL(d1):ALL(d2):[(c,d1) e f2f1 & (c,d2) e f2f1 => d1=d2]

         => ALL(c):ALL(d):[c e a & d e b => [d=f2f1(c) <=> (c,d) e f2f1]]]]

            U Spec, 1

 

      21   ALL(b):[Set'(f2f1) & Set(x) & Set(b)

         => [ALL(c):ALL(d):[(c,d) e f2f1 => c e x & d e b]

         & ALL(c):[c e x => EXIST(d):[d e b & (c,d) e f2f1]]

         & ALL(c):ALL(d1):ALL(d2):[(c,d1) e f2f1 & (c,d2) e f2f1 => d1=d2]

         => ALL(c):ALL(d):[c e x & d e b => [d=f2f1(c) <=> (c,d) e f2f1]]]]

            U Spec, 20

 

      22   Set'(f2f1) & Set(x) & Set(z)

         => [ALL(c):ALL(d):[(c,d) e f2f1 => c e x & d e z]

         & ALL(c):[c e x => EXIST(d):[d e z & (c,d) e f2f1]]

         & ALL(c):ALL(d1):ALL(d2):[(c,d1) e f2f1 & (c,d2) e f2f1 => d1=d2]

         => ALL(c):ALL(d):[c e x & d e z => [d=f2f1(c) <=> (c,d) e f2f1]]]

            U Spec, 21

 

      23   Set'(f2f1) & Set(x)

            Join, 18, 3

 

      24   Set'(f2f1) & Set(x) & Set(z)

            Join, 23, 5

 

   

    Sufficient: For functionality of f2f1

 

      25   ALL(c):ALL(d):[(c,d) e f2f1 => c e x & d e z]

         & ALL(c):[c e x => EXIST(d):[d e z & (c,d) e f2f1]]

         & ALL(c):ALL(d1):ALL(d2):[(c,d1) e f2f1 & (c,d2) e f2f1 => d1=d2]

         => ALL(c):ALL(d):[c e x & d e z => [d=f2f1(c) <=> (c,d) e f2f1]]

            Detach, 22, 24

 

        

         Prove: ALL(c):ALL(d):[(c,d) e f2f1 => c e x & d e z]

        

         Suppose...

 

            26   (p,q) e f2f1

                  Premise

 

            27   ALL(b):[(p,b) e f2f1 <=> (p,b) e xz & b=f2(f1(p))]

                  U Spec, 19

 

            28   (p,q) e f2f1 <=> (p,q) e xz & q=f2(f1(p))

                  U Spec, 27

 

            29   [(p,q) e f2f1 => (p,q) e xz & q=f2(f1(p))]

             & [(p,q) e xz & q=f2(f1(p)) => (p,q) e f2f1]

                  Iff-And, 28

 

            30   (p,q) e f2f1 => (p,q) e xz & q=f2(f1(p))

                  Split, 29

 

            31   (p,q) e xz & q=f2(f1(p)) => (p,q) e f2f1

                  Split, 29

 

            32   (p,q) e xz & q=f2(f1(p))

                  Detach, 30, 26

 

            33   (p,q) e xz

                  Split, 32

 

            34   q=f2(f1(p))

                  Split, 32

 

            35   ALL(c2):[(p,c2) e xz <=> p e x & c2 e z]

                  U Spec, 15

 

            36   (p,q) e xz <=> p e x & q e z

                  U Spec, 35

 

            37   [(p,q) e xz => p e x & q e z]

             & [p e x & q e z => (p,q) e xz]

                  Iff-And, 36

 

            38   (p,q) e xz => p e x & q e z

                  Split, 37

 

            39   p e x & q e z => (p,q) e xz

                  Split, 37

 

            40   p e x & q e z

                  Detach, 38, 33

 

    Functionality - Part 1

 

      41   ALL(c):ALL(d):[(c,d) e f2f1 => c e x & d e z]

            4 Conclusion, 26

 

        

         Prove: ALL(c):[c e x => EXIST(d):[d e z & (c,d) e f2f1]]

        

         Suppose...

 

            42   p e x

                  Premise

 

            43   ALL(b):[(p,b) e f2f1 <=> (p,b) e xz & b=f2(f1(p))]

                  U Spec, 19

 

            44   (p,f2(f1(p))) e f2f1 <=> (p,f2(f1(p))) e xz & f2(f1(p))=f2(f1(p))

                  U Spec, 43

 

            45   [(p,f2(f1(p))) e f2f1 => (p,f2(f1(p))) e xz & f2(f1(p))=f2(f1(p))]

             & [(p,f2(f1(p))) e xz & f2(f1(p))=f2(f1(p)) => (p,f2(f1(p))) e f2f1]

                  Iff-And, 44

 

            46   (p,f2(f1(p))) e f2f1 => (p,f2(f1(p))) e xz & f2(f1(p))=f2(f1(p))

                  Split, 45

 

         Sufficient: For (p,f2(f1(p))) e f2f1

 

            47   (p,f2(f1(p))) e xz & f2(f1(p))=f2(f1(p)) => (p,f2(f1(p))) e f2f1

                  Split, 45

 

            48   ALL(c2):[(p,c2) e xz <=> p e x & c2 e z]

                  U Spec, 15

 

            49   (p,f2(f1(p))) e xz <=> p e x & f2(f1(p)) e z

                  U Spec, 48

 

            50   [(p,f2(f1(p))) e xz => p e x & f2(f1(p)) e z]

             & [p e x & f2(f1(p)) e z => (p,f2(f1(p))) e xz]

                  Iff-And, 49

 

         Sufficient: For f2(f1(p)) e z

 

            51   (p,f2(f1(p))) e xz => p e x & f2(f1(p)) e z

                  Split, 50

 

            52   p e x & f2(f1(p)) e z => (p,f2(f1(p))) e xz

                  Split, 50

 

            53   ALL(c2):[(p,c2) e xz <=> p e x & c2 e z]

                  U Spec, 15

 

            54   (p,f2(f1(p))) e xz <=> p e x & f2(f1(p)) e z

                  U Spec, 53

 

            55   [(p,f2(f1(p))) e xz => p e x & f2(f1(p)) e z]

             & [p e x & f2(f1(p)) e z => (p,f2(f1(p))) e xz]

                  Iff-And, 54

 

            56   (p,f2(f1(p))) e xz => p e x & f2(f1(p)) e z

                  Split, 55

 

         Sufficient: For (p,f2(f1(p))) e xz

 

            57   p e x & f2(f1(p)) e z => (p,f2(f1(p))) e xz

                  Split, 55

 

            58   p e x => f1(p) e y

                  U Spec, 6

 

            59   f1(p) e y

                  Detach, 58, 42

 

            60   f1(p) e y => f2(f1(p)) e z

                  U Spec, 7

 

            61   f2(f1(p)) e z

                  Detach, 60, 59

 

            62   p e x & f2(f1(p)) e z

                  Join, 42, 61

 

            63   (p,f2(f1(p))) e xz

                  Detach, 57, 62

 

            64   p e x & f2(f1(p)) e z

                  Detach, 51, 63

 

            65   p e x

                  Split, 64

 

            66   f2(f1(p)) e z

                  Split, 64

 

            67   f2(f1(p))=f2(f1(p))

                  Reflex

 

            68   (p,f2(f1(p))) e xz & f2(f1(p))=f2(f1(p))

                  Join, 63, 67

 

            69   (p,f2(f1(p))) e f2f1

                  Detach, 47, 68

 

            70   f2(f1(p)) e z & (p,f2(f1(p))) e f2f1

                  Join, 66, 69

 

            71   EXIST(d):[d e z & (p,d) e f2f1]

                  E Gen, 70

 

    Functionality - Part 2

 

      72   ALL(c):[c e x => EXIST(d):[d e z & (c,d) e f2f1]]

            4 Conclusion, 42

 

        

         Prove: ALL(c):ALL(d1):ALL(d2):[(c,d1) e f2f1 & (c,d2) e f2f1 => d1=d2]

        

         Suppose...

 

            73   (p,q1) e f2f1 & (p,q2) e f2f1

                  Premise

 

            74   (p,q1) e f2f1

                  Split, 73

 

            75   (p,q2) e f2f1

                  Split, 73

 

            76   ALL(b):[(p,b) e f2f1 <=> (p,b) e xz & b=f2(f1(p))]

                  U Spec, 19

 

            77   (p,q1) e f2f1 <=> (p,q1) e xz & q1=f2(f1(p))

                  U Spec, 76

 

            78   [(p,q1) e f2f1 => (p,q1) e xz & q1=f2(f1(p))]

             & [(p,q1) e xz & q1=f2(f1(p)) => (p,q1) e f2f1]

                  Iff-And, 77

 

            79   (p,q1) e f2f1 => (p,q1) e xz & q1=f2(f1(p))

                  Split, 78

 

            80   (p,q1) e xz & q1=f2(f1(p)) => (p,q1) e f2f1

                  Split, 78

 

            81   (p,q1) e xz & q1=f2(f1(p))

                  Detach, 79, 74

 

            82   (p,q1) e xz

                  Split, 81

 

            83   q1=f2(f1(p))

                  Split, 81

 

            84   (p,q2) e f2f1 <=> (p,q2) e xz & q2=f2(f1(p))

                  U Spec, 76

 

            85   [(p,q2) e f2f1 => (p,q2) e xz & q2=f2(f1(p))]

             & [(p,q2) e xz & q2=f2(f1(p)) => (p,q2) e f2f1]

                  Iff-And, 84

 

            86   (p,q2) e f2f1 => (p,q2) e xz & q2=f2(f1(p))

                  Split, 85

 

            87   (p,q2) e xz & q2=f2(f1(p)) => (p,q2) e f2f1

                  Split, 85

 

            88   (p,q2) e xz & q2=f2(f1(p))

                  Detach, 86, 75

 

            89   (p,q2) e xz

                  Split, 88

 

            90   q2=f2(f1(p))

                  Split, 88

 

            91   q1=q2

                  Substitute, 90, 83

 

    Functionality - Part 3

 

      92   ALL(c):ALL(d1):ALL(d2):[(c,d1) e f2f1 & (c,d2) e f2f1 => d1=d2]

            4 Conclusion, 73

 

      93   ALL(c):ALL(d):[(c,d) e f2f1 => c e x & d e z]

         & ALL(c):[c e x => EXIST(d):[d e z & (c,d) e f2f1]]

            Join, 41, 72

 

      94   ALL(c):ALL(d):[(c,d) e f2f1 => c e x & d e z]

         & ALL(c):[c e x => EXIST(d):[d e z & (c,d) e f2f1]]

         & ALL(c):ALL(d1):ALL(d2):[(c,d1) e f2f1 & (c,d2) e f2f1 => d1=d2]

            Join, 93, 92

 

   

    f2f1 is a function

   

    As Required:

 

      95   ALL(c):ALL(d):[c e x & d e z => [d=f2f1(c) <=> (c,d) e f2f1]]

            Detach, 25, 94

 

        

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

        

         Suppose...

 

            96   p e x

                  Premise

 

            97   p e x => EXIST(d):[d e z & (p,d) e f2f1]

                  U Spec, 72

 

            98   EXIST(d):[d e z & (p,d) e f2f1]

                  Detach, 97, 96

 

            99   q e z & (p,q) e f2f1

                  E Spec, 98

 

            100  q e z

                  Split, 99

 

            101  (p,q) e f2f1

                  Split, 99

 

            102  ALL(d):[p e x & d e z => [d=f2f1(p) <=> (p,d) e f2f1]]

                  U Spec, 95

 

            103  p e x & q e z => [q=f2f1(p) <=> (p,q) e f2f1]

                  U Spec, 102

 

            104  p e x & q e z

                  Join, 96, 100

 

            105  q=f2f1(p) <=> (p,q) e f2f1

                  Detach, 103, 104

 

            106  [q=f2f1(p) => (p,q) e f2f1]

             & [(p,q) e f2f1 => q=f2f1(p)]

                  Iff-And, 105

 

            107  q=f2f1(p) => (p,q) e f2f1

                  Split, 106

 

            108  (p,q) e f2f1 => q=f2f1(p)

                  Split, 106

 

            109  q=f2f1(p)

                  Detach, 108, 101

 

            110  f2f1(p) e z

                  Substitute, 109, 100

 

   

    As Required:

 

      111  ALL(a):[a e x => f2f1(a) e z]

            4 Conclusion, 96

 

    As Required:

 

      112  ALL(d):[d e x => f2f1(d) e z]

            Rename, 111

 

        

         Prove: ALL(d):[d e x => f2f1(d)=f2(f1(d))]

        

         Suppose...

 

            113  p e x

                  Premise

 

            114  p e x => EXIST(d):[d e z & (p,d) e f2f1]

                  U Spec, 72

 

            115  EXIST(d):[d e z & (p,d) e f2f1]

                  Detach, 114, 113

 

            116  q e z & (p,q) e f2f1

                  E Spec, 115

 

            117  q e z

                  Split, 116

 

            118  (p,q) e f2f1

                  Split, 116

 

            119  ALL(d):[p e x & d e z => [d=f2f1(p) <=> (p,d) e f2f1]]

                  U Spec, 95

 

            120  p e x & q e z => [q=f2f1(p) <=> (p,q) e f2f1]

                  U Spec, 119

 

            121  p e x & q e z

                  Join, 113, 117

 

            122  q=f2f1(p) <=> (p,q) e f2f1

                  Detach, 120, 121

 

            123  [q=f2f1(p) => (p,q) e f2f1]

             & [(p,q) e f2f1 => q=f2f1(p)]

                  Iff-And, 122

 

            124  q=f2f1(p) => (p,q) e f2f1

                  Split, 123

 

            125  (p,q) e f2f1 => q=f2f1(p)

                  Split, 123

 

            126  q=f2f1(p)

                  Detach, 125, 118

 

            127  ALL(b):[(p,b) e f2f1 <=> (p,b) e xz & b=f2(f1(p))]

                  U Spec, 19

 

            128  (p,q) e f2f1 <=> (p,q) e xz & q=f2(f1(p))

                  U Spec, 127

 

            129  [(p,q) e f2f1 => (p,q) e xz & q=f2(f1(p))]

             & [(p,q) e xz & q=f2(f1(p)) => (p,q) e f2f1]

                  Iff-And, 128

 

            130  (p,q) e f2f1 => (p,q) e xz & q=f2(f1(p))

                  Split, 129

 

            131  (p,q) e xz & q=f2(f1(p)) => (p,q) e f2f1

                  Split, 129

 

            132  (p,q) e xz & q=f2(f1(p))

                  Detach, 130, 118

 

            133  (p,q) e xz

                  Split, 132

 

            134  q=f2(f1(p))

                  Split, 132

 

            135  f2f1(p)=f2(f1(p))

                  Substitute, 126, 134

 

    As Required:

 

      136  ALL(d):[d e x => f2f1(d)=f2(f1(d))]

            4 Conclusion, 113

 

      137  ALL(d):[d e x => f2f1(d) e z]

         & ALL(d):[d e x => f2f1(d)=f2(f1(d))]

            Join, 112, 136

 

As Required:

 

138  ALL(a):ALL(b):ALL(c):ALL(f1):ALL(f2):[Set(a) & Set(b) & Set(c)

    & ALL(d):[d e a => f1(d) e b]

    & ALL(d):[d e b => f2(d) e c]

    => EXIST(f2f1):[ALL(d):[d e a => f2f1(d) e c]

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

      4 Conclusion, 2