Introduction                           <------  User Comment (blue)

------------

Here, we prove that if f is a function mapping x to y, and g is a function

mapping y to z, then the composition of g and f maps x to z.

Logical Symbols

---------------

xey         means x is an element of y

f(x)        is the image of x under the function f

g(x)        is the image of x under the function g

ALL(x):     means "for all x, we have..."

=>          means "implies"

<=>         means "if and only if"

~           means "not"

Proof

-----

Suppose f is a function mapping the set x to the set y.

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

      Premise

Suppose further that g is a function mapping the set y to the set z.

2     ALL(a):[a e y => g(a) e z]

      Premise

     Prove: p e x => g(f(p)) e z

     Suppose...

      3     p e x

            Premise

     Applying the definition of f...

      4     p e x => f(p) e y

            U Spec, 1

      5     f(p) e y

            Detach, 4, 3

     Applying the defintion of g...

      6     f(p) e y => g(f(p)) e z

            U Spec, 2

      7     g(f(p)) e z

            Detach, 6, 5

As Required:

8     p e x => g(f(p)) e z            <-------- Universal generalization possible,

      4 Conclusion, 3                     for green variables, not for red variables.

Generalizing...

9     ALL(a):[a e x => g(f(a)) e z]   <-------- Universal generalization

      U Gen, 8