INTRODUCTION

************

Using only the rules of logic, we formally derive a simple consequence of the definition of a partial function f of one variable mapping a subset of x to y.

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

Dan Christensen

2014-04-27

This proof was written with aid of the author's DC Proof 2.0 software available free at http://www.dcproof.com

AXIOMS

******

Although only PF3 is used in this proof, PF1 and PF2 are included for completeness.

PF1: f is a subset of the Cartesian product of sets x and y

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

      Axiom

PF2: f is a partial function of one variable

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

      Axiom

PF3:  Definition of f(a)=b

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

      Axiom

     PROOF

     *****

     Suppose...

      4     t e x

            Premise

          '=>'

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

          Suppose...

            5     f(t) e y

                  Premise

          Apply equivalence of noation

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

                  U Spec, 3

            7     t e x & f(t) e y => [f(t)=f(t) <=> (t,f(t)) e f]

                  U Spec, 6

            8     t e x & f(t) e y

                  Join, 4, 5

            9     f(t)=f(t) <=> (t,f(t)) e f

                  Detach, 7, 8

            10    [f(t)=f(t) => (t,f(t)) e f]

              & [(t,f(t)) e f => f(t)=f(t)]

                  Iff-And, 9

            11    f(t)=f(t) => (t,f(t)) e f

                  Split, 10

            12    (t,f(t)) e f => f(t)=f(t)

                  Split, 10

            13    f(t)=f(t)

                  Reflex

            14    (t,f(t)) e f

                  Detach, 11, 13

            15    f(t) e y & (t,f(t)) e f

                  Join, 5, 14

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

                  E Gen, 15

     As Required:

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

            4 Conclusion, 5

          '<='

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

          Suppose...

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

                  Premise

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

                  E Spec, 18

            20    u e y

                  Split, 19

            21    (t,u) e f

                  Split, 19

          Apply equivalence of notation

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

                  U Spec, 3

            23    t e x & u e y => [f(t)=u <=> (t,u) e f]

                  U Spec, 22

            24    t e x & u e y

                  Join, 4, 20

            25    f(t)=u <=> (t,u) e f

                  Detach, 23, 24

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

                  Iff-And, 25

            27    f(t)=u => (t,u) e f

                  Split, 26

            28    (t,u) e f => f(t)=u

                  Split, 26

            29    f(t)=u

                  Detach, 28, 21

            30    f(t) e y

                  Substitute, 29, 20

     As Required:

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

            4 Conclusion, 18

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

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

            Join, 17, 31

      33    f(t) e y <=> EXIST(b):[b e y & (t,b) e f]

            Iff-And, 32

As Required:

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

      4 Conclusion, 4