THEOREM (Cantor-Bernstein-Schroeder)

*******

 

Suppose we have sets x and y, and injections f: x -> y and g: y -> x

 

  Set(x)                          (x is a set)

  & Set(y)                        (y is a set)

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

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

  & Injection(f,x,y)              (f is an injection)

  & Injection(g,y,x)              (g is an injection)

 

then there exists bijection k: x -> y

 

  ALL(a):[a e x => k(a) e y]      (k: x -> y)

  & Bijection(k,x,y)              (k is a bijection)

 

 

This proof written with the aid of, and mechanically verified by the author's DC Proof 2.0 software available at http://www.dcproof.com

 

 

Outline

*******

 

We start with sets x and y, injections f: x -> y and g: y -> x

 

From these, we construct, using the axioms of set theory and previously established lemmas, various sets and functions

that will be required:

 

px      = the power set of x

py      = the power set of y

px2     = the Cartesian prouduct of px with itself

xy      = the Cartesian prouduct of x and y

imgF(s) = the image of s under f

imgG(s) = the image of s under g

cx(s)   = the complement of s relative to x

cy(s)   = the complement of s relative to y

h(s)    = cx(imgG(cy(imgF(s))))

g'      = the inverse of a suitable restriction (subset) of g

 

Then we prove that for subsets s1 and s1 of x, if s1 is a subset of s2, then h(s1) is also a subset of h(s2). We say

that h is increasing.

 

Using the Knaster-Tarski Fixed-Point Lemma, we establish the existence of a subset z of x such h(z)=z.

 

Then we construct the function k: x -> y such that

 

k(a) = f(a)  if a e z

     = g'(a) otherwise

 

Finally, we prove that k is required bijection.

 

 

DEFINITIONS & PREVIOUS RESULTS

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

 

Define: Subset

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

 

1     ALL(a):ALL(b):[Subset(a,b) <=> ALL(c):[c e a => c e b]]

      Axiom

 

 

Define: Injection

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

 

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

      Axiom

 

 

Define: Surjection

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

 

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

      Axiom

 

Define: Bijection

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

 

Both arguments a and b should represent a Set, and f should represent a function mapping a to b.

 

4     ALL(f):ALL(a):ALL(b):[Bijection(f,a,b) <=> Injection(f,a,b) & Surjection(f,a,b)]

      Axiom

 

 

Knaster-Tarski Fixed-Point Lemma  Proof

 

5     ALL(s):ALL(ps):ALL(f):[Set(s)

     & Set(ps)

     & ALL(a):[a e ps <=> Set(a) & Subset(a,s)]

     & ALL(a):[a e ps => f(a) e ps]

     & ALL(a):ALL(b):[a e ps & b e ps

     => [Subset(a,b) => Subset(f(a),f(b))]]

     => EXIST(a):[Set(a) & Subset(a,s) & f(a)=a]]

      Axiom

 

Complement Function Lemma  Proof

 

6     ALL(s1):ALL(ps1):[Set(s1) & Set(ps1)

     & ALL(a):[a e ps1 <=> Set(a) & ALL(b):[b e a => b e s1]]

     => EXIST(f1):[ALL(a):[a e ps1 => f1(a) e ps1]

     & ALL(a):[a e ps1 => ALL(c):[c e s1 => [c e f1(a) <=> ~c e a]]]]]

      Axiom

 

Image Function Lemma  Proof

 

7     ALL(s1):ALL(s2):ALL(ps1):ALL(ps2):ALL(f1):[Set(s1) & Set(s2) & Set(ps1) & Set(ps2)

     & ALL(a):[a e s1 => f1(a) e s2]

     & ALL(a):[a e ps1 <=> Set(a) & ALL(b):[b e a => b e s1]]

     & ALL(a):[a e ps2 <=> Set(a) & ALL(b):[b e a => b e s2]]

     => EXIST(f2):[ALL(a):[a e ps1 => f2(a) e ps2]

     & ALL(a):[a e ps1

     => ALL(c):[c e f2(a) <=> EXIST(d):[d e a & f1(d)=c]]]]]

      Axiom

 

Complement of a Complement Lemma   Proof

 

8     ALL(s):ALL(ps):ALL(f):[Set(s)

     & Set(ps)

     & ALL(a):[a e ps <=> Set(a) & ALL(b):[b e a => b e s]]

     & ALL(a):[a e ps => f(a) e ps]

     & ALL(a):[a e ps => ALL(b):[b e s => [b e f(a) <=> ~b e a]]]

     => ALL(a):[a e ps => f(f(a))=a]]

      Axiom

 

Existence of Inverse Function Lemma  Proof

 

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

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

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

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

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

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

      Axiom

 

Inverses are Bijections Lemma   Proof

 

10    ALL(set1):ALL(set2):ALL(func):ALL(inv):[Set(set1) & Set(set2)

     & ALL(a):[a e set1 => func(a) e set2]

     & ALL(a):[a e set2 => inv(a) e set1]

     & ALL(a):ALL(b):[a e set1 & b e set2 => [inv(b)=a <=> func(a)=b]]

     => ALL(a):ALL(b):[a e set2 & b e set2 => [inv(a)=inv(b) => a=b]]

     & ALL(a):[a e set1 => EXIST(b):[b e set2 & inv(b)=a]]]

      Axiom

 

    

     Suppose...

 

      11    Set(x)

          & Set(y)

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

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

          & Injection(f,x,y)

          & Injection(g,y,x)

            Premise

 

     Splitting out this premise into its component parts...

 

      12    Set(x)

            Split, 11

 

      13    Set(y)

            Split, 11

 

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

            Split, 11

 

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

            Split, 11

 

      16    Injection(f,x,y)

            Split, 11

 

      17    Injection(g,y,x)

            Split, 11

 

    

     Apply the Power Set axiom  (twice)

 

      18    ALL(a):[Set(a) => EXIST(b):[Set(b)

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

            Power Set

 

      19    Set(x) => EXIST(b):[Set(b)

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

            U Spec, 18

 

      20    EXIST(b):[Set(b)

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

            Detach, 19, 12

 

      21    Set(px)

          & ALL(c):[c e px <=> Set(c) & ALL(d):[d e c => d e x]]

            E Spec, 20

 

    

     Define: px  (the power set of x)

     **********

 

      22    Set(px)

            Split, 21

 

      23    ALL(c):[c e px <=> Set(c) & ALL(d):[d e c => d e x]]

            Split, 21

 

      24    Set(y) => EXIST(b):[Set(b)

          & ALL(c):[c e b <=> Set(c) & ALL(d):[d e c => d e y]]]

            U Spec, 18

 

      25    EXIST(b):[Set(b)

          & ALL(c):[c e b <=> Set(c) & ALL(d):[d e c => d e y]]]

            Detach, 24, 13

 

      26    Set(py)

          & ALL(c):[c e py <=> Set(c) & ALL(d):[d e c => d e y]]

            E Spec, 25

 

    

     Define: py  (the power set of y)

     **********

 

      27    Set(py)

            Split, 26

 

      28    ALL(c):[c e py <=> Set(c) & ALL(d):[d e c => d e y]]

            Split, 26

 

    

     Apply the Cartesian Product axiom

 

      29    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

 

      30    ALL(a2):[Set(px) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e px & c2 e a2]]]

            U Spec, 29

 

      31    Set(px) & Set(px) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e px & c2 e px]]

            U Spec, 30

 

      32    Set(px) & Set(px)

            Join, 22, 22

 

      33    EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e px & c2 e px]]

            Detach, 31, 32

 

      34    Set'(px2) & ALL(c1):ALL(c2):[(c1,c2) e px2 <=> c1 e px & c2 e px]

            E Spec, 33

 

    

     Define: px2  (the Cartesian Product of px with itself)

     ***********

 

      35    Set'(px2)

            Split, 34

 

      36    ALL(c1):ALL(c2):[(c1,c2) e px2 <=> c1 e px & c2 e px]

            Split, 34

 

    

     Apply the Image Function Lemma

 

      37    ALL(s2):ALL(ps1):ALL(ps2):ALL(f1):[Set(x) & Set(s2) & Set(ps1) & Set(ps2)

          & ALL(a):[a e x => f1(a) e s2]

          & ALL(a):[a e ps1 <=> Set(a) & ALL(b):[b e a => b e x]]

          & ALL(a):[a e ps2 <=> Set(a) & ALL(b):[b e a => b e s2]]

          => EXIST(f2):[ALL(a):[a e ps1 => f2(a) e ps2]

          & ALL(a):[a e ps1

          => ALL(c):[c e f2(a) <=> EXIST(d):[d e a & f1(d)=c]]]]]

            U Spec, 7

 

      38    ALL(ps1):ALL(ps2):ALL(f1):[Set(x) & Set(y) & Set(ps1) & Set(ps2)

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

          & ALL(a):[a e ps1 <=> Set(a) & ALL(b):[b e a => b e x]]

          & ALL(a):[a e ps2 <=> Set(a) & ALL(b):[b e a => b e y]]

          => EXIST(f2):[ALL(a):[a e ps1 => f2(a) e ps2]

          & ALL(a):[a e ps1

          => ALL(c):[c e f2(a) <=> EXIST(d):[d e a & f1(d)=c]]]]]

            U Spec, 37

 

      39    ALL(ps2):ALL(f1):[Set(x) & Set(y) & Set(px) & Set(ps2)

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

          & ALL(a):[a e px <=> Set(a) & ALL(b):[b e a => b e x]]

          & ALL(a):[a e ps2 <=> Set(a) & ALL(b):[b e a => b e y]]

          => EXIST(f2):[ALL(a):[a e px => f2(a) e ps2]

          & ALL(a):[a e px

          => ALL(c):[c e f2(a) <=> EXIST(d):[d e a & f1(d)=c]]]]]

            U Spec, 38

 

      40    ALL(f1):[Set(x) & Set(y) & Set(px) & Set(py)

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

          & ALL(a):[a e px <=> Set(a) & ALL(b):[b e a => b e x]]

          & ALL(a):[a e py <=> Set(a) & ALL(b):[b e a => b e y]]

          => EXIST(f2):[ALL(a):[a e px => f2(a) e py]

          & ALL(a):[a e px

          => ALL(c):[c e f2(a) <=> EXIST(d):[d e a & f1(d)=c]]]]]

            U Spec, 39

 

      41    Set(x) & Set(y) & Set(px) & Set(py)

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

          & ALL(a):[a e px <=> Set(a) & ALL(b):[b e a => b e x]]

          & ALL(a):[a e py <=> Set(a) & ALL(b):[b e a => b e y]]

          => EXIST(f2):[ALL(a):[a e px => f2(a) e py]

          & ALL(a):[a e px

          => ALL(c):[c e f2(a) <=> EXIST(d):[d e a & f(d)=c]]]]

            U Spec, 40

 

      42    Set(x) & Set(y)

            Join, 12, 13

 

      43    Set(x) & Set(y) & Set(px)

            Join, 42, 22

 

      44    Set(x) & Set(y) & Set(px) & Set(py)

            Join, 43, 27

 

      45    Set(x) & Set(y) & Set(px) & Set(py)

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

            Join, 44, 14

 

      46    Set(x) & Set(y) & Set(px) & Set(py)

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

          & ALL(c):[c e px <=> Set(c) & ALL(d):[d e c => d e x]]

            Join, 45, 23

 

      47    Set(x) & Set(y) & Set(px) & Set(py)

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

          & ALL(c):[c e px <=> Set(c) & ALL(d):[d e c => d e x]]

          & ALL(c):[c e py <=> Set(c) & ALL(d):[d e c => d e y]]

            Join, 46, 28

 

      48    EXIST(f2):[ALL(a):[a e px => f2(a) e py]

          & ALL(a):[a e px

          => ALL(c):[c e f2(a) <=> EXIST(d):[d e a & f(d)=c]]]]

            Detach, 41, 47

 

      49    ALL(a):[a e px => imgF(a) e py]

          & ALL(a):[a e px

          => ALL(c):[c e imgF(a) <=> EXIST(d):[d e a & f(d)=c]]]

            E Spec, 48

 

    

     Define: imgF   (function mapping subsets of x to their image under f)

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

 

      50    ALL(a):[a e px => imgF(a) e py]

            Split, 49

 

      51    ALL(a):[a e px

          => ALL(c):[c e imgF(a) <=> EXIST(d):[d e a & f(d)=c]]]

            Split, 49

 

    

     Apply Image Function Lemma

 

      52    ALL(s2):ALL(ps1):ALL(ps2):ALL(f1):[Set(y) & Set(s2) & Set(ps1) & Set(ps2)

          & ALL(a):[a e y => f1(a) e s2]

          & ALL(a):[a e ps1 <=> Set(a) & ALL(b):[b e a => b e y]]

          & ALL(a):[a e ps2 <=> Set(a) & ALL(b):[b e a => b e s2]]

          => EXIST(f2):[ALL(a):[a e ps1 => f2(a) e ps2]

          & ALL(a):[a e ps1

          => ALL(c):[c e f2(a) <=> EXIST(d):[d e a & f1(d)=c]]]]]

            U Spec, 7

 

      53    ALL(ps1):ALL(ps2):ALL(f1):[Set(y) & Set(x) & Set(ps1) & Set(ps2)

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

          & ALL(a):[a e ps1 <=> Set(a) & ALL(b):[b e a => b e y]]

          & ALL(a):[a e ps2 <=> Set(a) & ALL(b):[b e a => b e x]]

          => EXIST(f2):[ALL(a):[a e ps1 => f2(a) e ps2]

          & ALL(a):[a e ps1

          => ALL(c):[c e f2(a) <=> EXIST(d):[d e a & f1(d)=c]]]]]

            U Spec, 52

 

      54    ALL(ps2):ALL(f1):[Set(y) & Set(x) & Set(py) & Set(ps2)

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

          & ALL(a):[a e py <=> Set(a) & ALL(b):[b e a => b e y]]

          & ALL(a):[a e ps2 <=> Set(a) & ALL(b):[b e a => b e x]]

          => EXIST(f2):[ALL(a):[a e py => f2(a) e ps2]

          & ALL(a):[a e py

          => ALL(c):[c e f2(a) <=> EXIST(d):[d e a & f1(d)=c]]]]]

            U Spec, 53

 

      55    ALL(f1):[Set(y) & Set(x) & Set(py) & Set(px)

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

          & ALL(a):[a e py <=> Set(a) & ALL(b):[b e a => b e y]]

          & ALL(a):[a e px <=> Set(a) & ALL(b):[b e a => b e x]]

          => EXIST(f2):[ALL(a):[a e py => f2(a) e px]

          & ALL(a):[a e py

          => ALL(c):[c e f2(a) <=> EXIST(d):[d e a & f1(d)=c]]]]]

            U Spec, 54

 

      56    Set(y) & Set(x) & Set(py) & Set(px)

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

          & ALL(a):[a e py <=> Set(a) & ALL(b):[b e a => b e y]]

          & ALL(a):[a e px <=> Set(a) & ALL(b):[b e a => b e x]]

          => EXIST(f2):[ALL(a):[a e py => f2(a) e px]

          & ALL(a):[a e py

          => ALL(c):[c e f2(a) <=> EXIST(d):[d e a & g(d)=c]]]]

            U Spec, 55

 

      57    Set(y) & Set(x)

            Join, 13, 12

 

      58    Set(y) & Set(x) & Set(py)

            Join, 57, 27

 

      59    Set(y) & Set(x) & Set(py) & Set(px)

            Join, 58, 22

 

      60    Set(y) & Set(x) & Set(py) & Set(px)

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

            Join, 59, 15

 

      61    Set(y) & Set(x) & Set(py) & Set(px)

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

          & ALL(c):[c e py <=> Set(c) & ALL(d):[d e c => d e y]]

            Join, 60, 28

 

      62    Set(y) & Set(x) & Set(py) & Set(px)

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

          & ALL(c):[c e py <=> Set(c) & ALL(d):[d e c => d e y]]

          & ALL(c):[c e px <=> Set(c) & ALL(d):[d e c => d e x]]

            Join, 61, 23

 

      63    EXIST(f2):[ALL(a):[a e py => f2(a) e px]

          & ALL(a):[a e py

          => ALL(c):[c e f2(a) <=> EXIST(d):[d e a & g(d)=c]]]]

            Detach, 56, 62

 

      64    ALL(a):[a e py => imgG(a) e px]

          & ALL(a):[a e py

          => ALL(c):[c e imgG(a) <=> EXIST(d):[d e a & g(d)=c]]]

            E Spec, 63

 

    

     Define: imgG  (function mapping subsets of y to their image under g)

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

 

      65    ALL(a):[a e py => imgG(a) e px]

            Split, 64

 

      66    ALL(a):[a e py

          => ALL(c):[c e imgG(a) <=> EXIST(d):[d e a & g(d)=c]]]

            Split, 64

 

    

     Apply Complement Function Lemma

 

      67    ALL(ps1):[Set(x) & Set(ps1)

          & ALL(a):[a e ps1 <=> Set(a) & ALL(b):[b e a => b e x]]

          => EXIST(f1):[ALL(a):[a e ps1 => f1(a) e ps1]

          & ALL(a):[a e ps1 => ALL(c):[c e x => [c e f1(a) <=> ~c e a]]]]]

            U Spec, 6

 

      68    Set(x) & Set(px)

          & ALL(a):[a e px <=> Set(a) & ALL(b):[b e a => b e x]]

          => EXIST(f1):[ALL(a):[a e px => f1(a) e px]

          & ALL(a):[a e px => ALL(c):[c e x => [c e f1(a) <=> ~c e a]]]]

            U Spec, 67

 

      69    Set(x) & Set(px)

            Join, 12, 22

 

      70    Set(x) & Set(px)

          & ALL(c):[c e px <=> Set(c) & ALL(d):[d e c => d e x]]

            Join, 69, 23

 

      71    EXIST(f1):[ALL(a):[a e px => f1(a) e px]

          & ALL(a):[a e px => ALL(c):[c e x => [c e f1(a) <=> ~c e a]]]]

            Detach, 68, 70

 

      72    ALL(a):[a e px => cx(a) e px]

          & ALL(a):[a e px => ALL(c):[c e x => [c e cx(a) <=> ~c e a]]]

            E Spec, 71

 

    

     Define: cx  (function mapping subsets of x to their complements wrt x)

     **********

 

      73    ALL(a):[a e px => cx(a) e px]

            Split, 72

 

      74    ALL(a):[a e px => ALL(c):[c e x => [c e cx(a) <=> ~c e a]]]

            Split, 72

 

    

     Apply Complement Function Lemma

 

      75    ALL(ps1):[Set(y) & Set(ps1)

          & ALL(a):[a e ps1 <=> Set(a) & ALL(b):[b e a => b e y]]

          => EXIST(f1):[ALL(a):[a e ps1 => f1(a) e ps1]

          & ALL(a):[a e ps1 => ALL(c):[c e y => [c e f1(a) <=> ~c e a]]]]]

            U Spec, 6

 

      76    Set(y) & Set(py)

          & ALL(a):[a e py <=> Set(a) & ALL(b):[b e a => b e y]]

          => EXIST(f1):[ALL(a):[a e py => f1(a) e py]

          & ALL(a):[a e py => ALL(c):[c e y => [c e f1(a) <=> ~c e a]]]]

            U Spec, 75

 

      77    Set(y) & Set(py)

            Join, 13, 27

 

      78    Set(y) & Set(py)

          & ALL(c):[c e py <=> Set(c) & ALL(d):[d e c => d e y]]

            Join, 77, 28

 

      79    EXIST(f1):[ALL(a):[a e py => f1(a) e py]

          & ALL(a):[a e py => ALL(c):[c e y => [c e f1(a) <=> ~c e a]]]]

            Detach, 76, 78

 

      80    ALL(a):[a e py => cy(a) e py]

          & ALL(a):[a e py => ALL(c):[c e y => [c e cy(a) <=> ~c e a]]]

            E Spec, 79

 

    

     Define: cy  (function mapping subsets of y to their complements wrt y

     **********

 

      81    ALL(a):[a e py => cy(a) e py]

            Split, 80

 

      82    ALL(a):[a e py => ALL(c):[c e y => [c e cy(a) <=> ~c e a]]]

            Split, 80

 

    

     Apply Subset axiom

 

      83    EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e px2 & b=cx(imgG(cy(imgF(a))))]]

            Subset, 35

 

      84    Set'(h) & ALL(a):ALL(b):[(a,b) e h <=> (a,b) e px2 & b=cx(imgG(cy(imgF(a))))]

            E Spec, 83

 

    

     Define: h 

     *********

 

      85    Set'(h)

            Split, 84

 

      86    ALL(a):ALL(b):[(a,b) e h <=> (a,b) e px2 & b=cx(imgG(cy(imgF(a))))]

            Split, 84

 

    

     Apply Function axiom

 

      87    ALL(f):ALL(a):ALL(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):[d=f(c) <=> (c,d) e f]]

            Function

 

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

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

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

          => ALL(c):ALL(d):[d=h(c) <=> (c,d) e h]]

            U Spec, 87

 

      89    ALL(b):[ALL(c):ALL(d):[(c,d) e h => c e px & d e b]

          & ALL(c):[c e px => EXIST(d):[d e b & (c,d) e h]]

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

          => ALL(c):ALL(d):[d=h(c) <=> (c,d) e h]]

            U Spec, 88

 

    

     Sufficient: For functionality of h

 

      90    ALL(c):ALL(d):[(c,d) e h => c e px & d e px]

          & ALL(c):[c e px => EXIST(d):[d e px & (c,d) e h]]

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

          => ALL(c):ALL(d):[d=h(c) <=> (c,d) e h]

            U Spec, 89

 

         

          Prove: ALL(c):ALL(d):[(c,d) e h => c e px & d e px]

         

          Suppose...

 

            91    (p,q) e h

                  Premise

 

          Apply definition of h

 

            92    ALL(b):[(p,b) e h <=> (p,b) e px2 & b=cx(imgG(cy(imgF(p))))]

                  U Spec, 86

 

            93    (p,q) e h <=> (p,q) e px2 & q=cx(imgG(cy(imgF(p))))

                  U Spec, 92

 

            94    [(p,q) e h => (p,q) e px2 & q=cx(imgG(cy(imgF(p))))]

              & [(p,q) e px2 & q=cx(imgG(cy(imgF(p)))) => (p,q) e h]

                  Iff-And, 93

 

            95    (p,q) e h => (p,q) e px2 & q=cx(imgG(cy(imgF(p))))

                  Split, 94

 

            96    (p,q) e px2 & q=cx(imgG(cy(imgF(p)))) => (p,q) e h

                  Split, 94

 

            97    (p,q) e px2 & q=cx(imgG(cy(imgF(p))))

                  Detach, 95, 91

 

            98    (p,q) e px2

                  Split, 97

 

            99    q=cx(imgG(cy(imgF(p))))

                  Split, 97

 

          Apply definition of px2

 

            100  ALL(c2):[(p,c2) e px2 <=> p e px & c2 e px]

                  U Spec, 36

 

            101  (p,q) e px2 <=> p e px & q e px

                  U Spec, 100

 

            102  [(p,q) e px2 => p e px & q e px]

              & [p e px & q e px => (p,q) e px2]

                  Iff-And, 101

 

            103  (p,q) e px2 => p e px & q e px

                  Split, 102

 

            104  p e px & q e px => (p,q) e px2

                  Split, 102

 

            105  p e px & q e px

                  Detach, 103, 98

 

     As Required:

 

      106  ALL(c):ALL(d):[(c,d) e h => c e px & d e px]

            4 Conclusion, 91

 

         

          Prove: ALL(c):[c e px => EXIST(d):[d e px & (c,d) e h]]

         

          Suppose...

 

            107  p e px

                  Premise

 

          Apply definition of h

 

            108  ALL(b):[(p,b) e h <=> (p,b) e px2 & b=cx(imgG(cy(imgF(p))))]

                  U Spec, 86

 

            109  (p,cx(imgG(cy(imgF(p))))) e h <=> (p,cx(imgG(cy(imgF(p))))) e px2 & cx(imgG(cy(imgF(p))))=cx(imgG(cy(imgF(p))))

                  U Spec, 108

 

            110  [(p,cx(imgG(cy(imgF(p))))) e h => (p,cx(imgG(cy(imgF(p))))) e px2 & cx(imgG(cy(imgF(p))))=cx(imgG(cy(imgF(p))))]

              & [(p,cx(imgG(cy(imgF(p))))) e px2 & cx(imgG(cy(imgF(p))))=cx(imgG(cy(imgF(p)))) => (p,cx(imgG(cy(imgF(p))))) e h]

                  Iff-And, 109

 

            111  (p,cx(imgG(cy(imgF(p))))) e h => (p,cx(imgG(cy(imgF(p))))) e px2 & cx(imgG(cy(imgF(p))))=cx(imgG(cy(imgF(p))))

                  Split, 110

 

            112  (p,cx(imgG(cy(imgF(p))))) e px2 & cx(imgG(cy(imgF(p))))=cx(imgG(cy(imgF(p)))) => (p,cx(imgG(cy(imgF(p))))) e h

                  Split, 110

 

          Apply definition of px2

 

            113  ALL(c2):[(p,c2) e px2 <=> p e px & c2 e px]

                  U Spec, 36

 

            114  (p,cx(imgG(cy(imgF(p))))) e px2 <=> p e px & cx(imgG(cy(imgF(p)))) e px

                  U Spec, 113

 

            115  [(p,cx(imgG(cy(imgF(p))))) e px2 => p e px & cx(imgG(cy(imgF(p)))) e px]

              & [p e px & cx(imgG(cy(imgF(p)))) e px => (p,cx(imgG(cy(imgF(p))))) e px2]

                  Iff-And, 114

 

            116  (p,cx(imgG(cy(imgF(p))))) e px2 => p e px & cx(imgG(cy(imgF(p)))) e px

                  Split, 115

 

            117  p e px & cx(imgG(cy(imgF(p)))) e px => (p,cx(imgG(cy(imgF(p))))) e px2

                  Split, 115

 

          Apply definition of imgF function

 

            118  p e px => imgF(p) e py

                  U Spec, 50

 

            119  imgF(p) e py

                  Detach, 118, 107

 

            120  imgF(p) e py => cy(imgF(p)) e py

                  U Spec, 81

 

            121  cy(imgF(p)) e py

                  Detach, 120, 119

 

          Apply definition of cy function

 

            122  cy(imgF(p)) e py => imgG(cy(imgF(p))) e px

                  U Spec, 65

 

            123  imgG(cy(imgF(p))) e px

                  Detach, 122, 121

 

          Apply definition of imgG function

 

            124  imgG(cy(imgF(p))) e px => cx(imgG(cy(imgF(p)))) e px

                  U Spec, 73

 

            125  cx(imgG(cy(imgF(p)))) e px

                  Detach, 124, 123

 

            126  p e px & cx(imgG(cy(imgF(p)))) e px

                  Join, 107, 125

 

            127  (p,cx(imgG(cy(imgF(p))))) e px2

                  Detach, 117, 126

 

            128  cx(imgG(cy(imgF(p))))=cx(imgG(cy(imgF(p))))

                  Reflex

 

            129  (p,cx(imgG(cy(imgF(p))))) e px2

              & cx(imgG(cy(imgF(p))))=cx(imgG(cy(imgF(p))))

                  Join, 127, 128

 

            130  (p,cx(imgG(cy(imgF(p))))) e h

                  Detach, 112, 129

 

            131  cx(imgG(cy(imgF(p)))) e px

              & (p,cx(imgG(cy(imgF(p))))) e h

                  Join, 125, 130

 

            132  EXIST(d):[d e px

              & (p,d) e h]

                  E Gen, 131

 

     As Required:

 

      133  ALL(c):[c e px => EXIST(d):[d e px

          & (c,d) e h]]

            4 Conclusion, 107

 

         

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

         

          Suppose...

 

            134  (p,q1) e h & (p,q2) e h

                  Premise

 

            135  (p,q1) e h

                  Split, 134

 

            136  (p,q2) e h

                  Split, 134

 

          Apply definition of h

 

            137  ALL(b):[(p,b) e h <=> (p,b) e px2 & b=cx(imgG(cy(imgF(p))))]

                  U Spec, 86

 

            138  (p,q1) e h <=> (p,q1) e px2 & q1=cx(imgG(cy(imgF(p))))

                  U Spec, 137

 

            139  [(p,q1) e h => (p,q1) e px2 & q1=cx(imgG(cy(imgF(p))))]

              & [(p,q1) e px2 & q1=cx(imgG(cy(imgF(p)))) => (p,q1) e h]

                  Iff-And, 138

 

            140  (p,q1) e h => (p,q1) e px2 & q1=cx(imgG(cy(imgF(p))))

                  Split, 139

 

            141  (p,q1) e px2 & q1=cx(imgG(cy(imgF(p)))) => (p,q1) e h

                  Split, 139

 

            142  (p,q1) e px2 & q1=cx(imgG(cy(imgF(p))))

                  Detach, 140, 135

 

            143  (p,q1) e px2

                  Split, 142

 

            144  q1=cx(imgG(cy(imgF(p))))

                  Split, 142

 

            145  (p,q2) e h <=> (p,q2) e px2 & q2=cx(imgG(cy(imgF(p))))

                  U Spec, 137

 

            146  [(p,q2) e h => (p,q2) e px2 & q2=cx(imgG(cy(imgF(p))))]

              & [(p,q2) e px2 & q2=cx(imgG(cy(imgF(p)))) => (p,q2) e h]

                  Iff-And, 145

 

            147  (p,q2) e h => (p,q2) e px2 & q2=cx(imgG(cy(imgF(p))))

                  Split, 146

 

            148  (p,q2) e px2 & q2=cx(imgG(cy(imgF(p)))) => (p,q2) e h

                  Split, 146

 

            149  (p,q2) e px2 & q2=cx(imgG(cy(imgF(p))))

                  Detach, 147, 136

 

            150  (p,q2) e px2

                  Split, 149

 

            151  q2=cx(imgG(cy(imgF(p))))

                  Split, 149

 

            152  q1=q2

                  Substitute, 151, 144

 

     As Required:

 

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

            4 Conclusion, 134

 

      154  ALL(c):ALL(d):[(c,d) e h => c e px & d e px]

          & ALL(c):[c e px => EXIST(d):[d e px

          & (c,d) e h]]

            Join, 106, 133

 

      155  ALL(c):ALL(d):[(c,d) e h => c e px & d e px]

          & ALL(c):[c e px => EXIST(d):[d e px

          & (c,d) e h]]

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

            Join, 154, 153

 

    

     h is a function

 

      156  ALL(c):ALL(d):[d=h(c) <=> (c,d) e h]

            Detach, 90, 155

 

         

          Prove: ALL(a):[a e px => h(a) e px]

         

          Suppose...

 

            157  p e px

                  Premise

 

          Apply previous result

 

            158  p e px => EXIST(d):[d e px

              & (p,d) e h]

                  U Spec, 133

 

            159  EXIST(d):[d e px

              & (p,d) e h]

                  Detach, 158, 157

 

            160  q e px

              & (p,q) e h

                  E Spec, 159

 

            161  q e px

                  Split, 160

 

            162  (p,q) e h

                  Split, 160

 

          Apply previous result

 

            163  ALL(d):[d=h(p) <=> (p,d) e h]

                  U Spec, 156

 

            164  q=h(p) <=> (p,q) e h

                  U Spec, 163

 

            165  [q=h(p) => (p,q) e h] & [(p,q) e h => q=h(p)]

                  Iff-And, 164

 

            166  q=h(p) => (p,q) e h

                  Split, 165

 

            167  (p,q) e h => q=h(p)

                  Split, 165

 

            168  q=h(p)

                  Detach, 167, 162

 

            169  h(p) e px

                  Substitute, 168, 161

 

     As Required:

 

      170  ALL(a):[a e px => h(a) e px]

            4 Conclusion, 157

 

         

          Prove: ALL(a):[a e px => h(a)=cx(imgG(cy(imgF(a))))]

         

          Suppose...

 

            171  p e px

                  Premise

 

          Apply previous result

 

            172  p e px => EXIST(d):[d e px

              & (p,d) e h]

                  U Spec, 133

 

            173  EXIST(d):[d e px

              & (p,d) e h]

                  Detach, 172, 171

 

            174  q e px

              & (p,q) e h

                  E Spec, 173

 

            175  q e px

                  Split, 174

 

            176  (p,q) e h

                  Split, 174

 

          Apply definition of h

 

            177  ALL(b):[(p,b) e h <=> (p,b) e px2 & b=cx(imgG(cy(imgF(p))))]

                  U Spec, 86

 

            178  (p,q) e h <=> (p,q) e px2 & q=cx(imgG(cy(imgF(p))))

                  U Spec, 177

 

            179  [(p,q) e h => (p,q) e px2 & q=cx(imgG(cy(imgF(p))))]

              & [(p,q) e px2 & q=cx(imgG(cy(imgF(p)))) => (p,q) e h]

                  Iff-And, 178

 

            180  (p,q) e h => (p,q) e px2 & q=cx(imgG(cy(imgF(p))))

                  Split, 179

 

            181  (p,q) e px2 & q=cx(imgG(cy(imgF(p)))) => (p,q) e h

                  Split, 179

 

            182  (p,q) e px2 & q=cx(imgG(cy(imgF(p))))

                  Detach, 180, 176

 

            183  (p,q) e px2

                  Split, 182

 

            184  q=cx(imgG(cy(imgF(p))))

                  Split, 182

 

            185  ALL(d):[d=h(p) <=> (p,d) e h]

                  U Spec, 156

 

          Apply previous result

 

            186  q=h(p) <=> (p,q) e h

                  U Spec, 185

 

            187  [q=h(p) => (p,q) e h] & [(p,q) e h => q=h(p)]

                  Iff-And, 186

 

            188  q=h(p) => (p,q) e h

                  Split, 187

 

            189  (p,q) e h => q=h(p)

                  Split, 187

 

            190  q=h(p)

                  Detach, 189, 176

 

            191  h(p)=cx(imgG(cy(imgF(p))))

                  Substitute, 190, 184

 

     As Required:

 

      192  ALL(a):[a e px => h(a)=cx(imgG(cy(imgF(a))))]

            4 Conclusion, 171

 

    

     Apply the Knaster-Tarski Fixed-Point Lemma

 

      193  ALL(ps):ALL(f):[Set(x)

          & Set(ps)

          & ALL(a):[a e ps <=> Set(a) & Subset(a,x)]

          & ALL(a):[a e ps => f(a) e ps]

          & ALL(a):ALL(b):[a e ps & b e ps

          => [Subset(a,b) => Subset(f(a),f(b))]]

          => EXIST(a):[Set(a) & Subset(a,x) & f(a)=a]]

            U Spec, 5

 

      194  ALL(f):[Set(x)

          & Set(px)

          & ALL(a):[a e px <=> Set(a) & Subset(a,x)]

          & ALL(a):[a e px => f(a) e px]

          & ALL(a):ALL(b):[a e px & b e px

          => [Subset(a,b) => Subset(f(a),f(b))]]

          => EXIST(a):[Set(a) & Subset(a,x) & f(a)=a]]

            U Spec, 193

 

    

     Sufficient: For EXIST(a):[Set(a) & Subset(a,x) & h(a)=a]

 

      195  Set(x)

          & Set(px)

          & ALL(a):[a e px <=> Set(a) & Subset(a,x)]

          & ALL(a):[a e px => h(a) e px]

          & ALL(a):ALL(b):[a e px & b e px

          => [Subset(a,b) => Subset(h(a),h(b))]]

          => EXIST(a):[Set(a) & Subset(a,x) & h(a)=a]

            U Spec, 194

 

         

          Prove that if p and q are subsets of x, and Subset(p,q) then Subset(h(p),h(q)).

         

          Suppose...

 

            196  p e px & q e px

                  Premise

 

            197  p e px

                  Split, 196

 

            198  q e px

                  Split, 196

 

             

               Suppose...

 

                  199  Subset(p,q)

                        Premise

 

                  200  ALL(b):[Subset(p,b) <=> ALL(c):[c e p => c e b]]

                        U Spec, 1

 

                  201  Subset(p,q) <=> ALL(c):[c e p => c e q]

                        U Spec, 200

 

                  202  [Subset(p,q) => ALL(c):[c e p => c e q]]

                   & [ALL(c):[c e p => c e q] => Subset(p,q)]

                        Iff-And, 201

 

                  203  Subset(p,q) => ALL(c):[c e p => c e q]

                        Split, 202

 

                  204  ALL(c):[c e p => c e q] => Subset(p,q)

                        Split, 202

 

                  205  ALL(c):[c e p => c e q]

                        Detach, 203, 199

 

                  206  p e px

                   => ALL(c):[c e imgF(p) <=> EXIST(d):[d e p & f(d)=c]]

                        U Spec, 51

 

                  207  ALL(c):[c e imgF(p) <=> EXIST(d):[d e p & f(d)=c]]

                        Detach, 206, 197

 

                  208  q e px

                   => ALL(c):[c e imgF(q) <=> EXIST(d):[d e q & f(d)=c]]

                        U Spec, 51

 

                  209  ALL(c):[c e imgF(q) <=> EXIST(d):[d e q & f(d)=c]]

                        Detach, 208, 198

 

                  

                   Suppose...

 

                        210  r e imgF(p)

                              Premise

 

                        211  r e imgF(p) <=> EXIST(d):[d e p & f(d)=r]

                              U Spec, 207

 

                        212  [r e imgF(p) => EXIST(d):[d e p & f(d)=r]]

                        & [EXIST(d):[d e p & f(d)=r] => r e imgF(p)]

                              Iff-And, 211

 

                        213  r e imgF(p) => EXIST(d):[d e p & f(d)=r]

                              Split, 212

 

                        214  EXIST(d):[d e p & f(d)=r] => r e imgF(p)

                              Split, 212

 

                        215  EXIST(d):[d e p & f(d)=r]

                              Detach, 213, 210

 

                        216  s e p & f(s)=r

                              E Spec, 215

 

                        217  s e p

                              Split, 216

 

                        218  f(s)=r

                              Split, 216

 

                        219  r e imgF(q) <=> EXIST(d):[d e q & f(d)=r]

                              U Spec, 209

 

                        220  [r e imgF(q) => EXIST(d):[d e q & f(d)=r]]

                        & [EXIST(d):[d e q & f(d)=r] => r e imgF(q)]

                              Iff-And, 219

 

                        221  r e imgF(q) => EXIST(d):[d e q & f(d)=r]

                              Split, 220

 

                        222  EXIST(d):[d e q & f(d)=r] => r e imgF(q)

                              Split, 220

 

                        223  s e p => s e q

                              U Spec, 205

 

                        224  s e q

                              Detach, 223, 217

 

                        225  s e q & f(s)=r

                              Join, 224, 218

 

                        226  EXIST(d):[d e q & f(d)=r]

                              E Gen, 225

 

                        227  r e imgF(q)

                              Detach, 222, 226

 

              As Required:

 

                  228  ALL(c):[c e imgF(p) => c e imgF(q)]

                        4 Conclusion, 210

 

                  

                   Suppose...

 

                        229  r e cy(imgF(q))

                              Premise

 

                        230  imgF(q) e py => ALL(c):[c e y => [c e cy(imgF(q)) <=> ~c e imgF(q)]]

                              U Spec, 82

 

                        231  imgF(p) e py => ALL(c):[c e y => [c e cy(imgF(p)) <=> ~c e imgF(p)]]

                              U Spec, 82

 

                        232  q e px => imgF(q) e py

                              U Spec, 50

 

                        233  imgF(q) e py

                              Detach, 232, 198

 

                        234  ALL(c):[c e y => [c e cy(imgF(q)) <=> ~c e imgF(q)]]

                              Detach, 230, 233

 

                        235  r e y => [r e cy(imgF(q)) <=> ~r e imgF(q)]

                              U Spec, 234

 

                        236  imgF(q) e py => cy(imgF(q)) e py

                              U Spec, 81

 

                        237  cy(imgF(q)) e py

                              Detach, 236, 233

 

                        238  cy(imgF(q)) e py <=> Set(cy(imgF(q))) & ALL(d):[d e cy(imgF(q)) => d e y]

                              U Spec, 28

 

                        239  [cy(imgF(q)) e py => Set(cy(imgF(q))) & ALL(d):[d e cy(imgF(q)) => d e y]]

                        & [Set(cy(imgF(q))) & ALL(d):[d e cy(imgF(q)) => d e y] => cy(imgF(q)) e py]

                              Iff-And, 238

 

                        240  cy(imgF(q)) e py => Set(cy(imgF(q))) & ALL(d):[d e cy(imgF(q)) => d e y]

                              Split, 239

 

                        241  Set(cy(imgF(q))) & ALL(d):[d e cy(imgF(q)) => d e y] => cy(imgF(q)) e py

                              Split, 239

 

                        242  Set(cy(imgF(q))) & ALL(d):[d e cy(imgF(q)) => d e y]

                              Detach, 240, 237

 

                        243  Set(cy(imgF(q)))

                              Split, 242

 

                        244  ALL(d):[d e cy(imgF(q)) => d e y]

                              Split, 242

 

                        245  r e cy(imgF(q)) => r e y

                              U Spec, 244

 

                        246  r e y

                              Detach, 245, 229

 

                        247  r e cy(imgF(q)) <=> ~r e imgF(q)

                              Detach, 235, 246

 

                        248  [r e cy(imgF(q)) => ~r e imgF(q)]

                        & [~r e imgF(q) => r e cy(imgF(q))]

                              Iff-And, 247

 

                        249  r e cy(imgF(q)) => ~r e imgF(q)

                              Split, 248

 

                        250  ~r e imgF(q) => r e cy(imgF(q))

                              Split, 248

 

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

 

                        251  ~r e imgF(q)

                              Detach, 249, 229

 

                        252  p e px => imgF(p) e py

                              U Spec, 50

 

                        253  imgF(p) e py

                              Detach, 252, 197

 

                        254  ALL(c):[c e y => [c e cy(imgF(p)) <=> ~c e imgF(p)]]

                              Detach, 231, 253

 

                        255  r e y => [r e cy(imgF(p)) <=> ~r e imgF(p)]

                              U Spec, 254

 

                        256  r e cy(imgF(p)) <=> ~r e imgF(p)

                              Detach, 255, 246

 

                        257  [r e cy(imgF(p)) => ~r e imgF(p)]

                        & [~r e imgF(p) => r e cy(imgF(p))]

                              Iff-And, 256

 

                        258  r e cy(imgF(p)) => ~r e imgF(p)

                              Split, 257

 

                   Sufficient:

 

                        259  ~r e imgF(p) => r e cy(imgF(p))

                              Split, 257

 

                        260  r e imgF(p) => r e imgF(q)

                              U Spec, 228

 

                        261  ~r e imgF(q) => ~r e imgF(p)

                              Contra, 260

 

                        262  ~r e imgF(p)

                              Detach, 261, 251

 

                        263  r e cy(imgF(p))

                              Detach, 259, 262

 

              As Required:

 

                  264  ALL(a):[a e cy(imgF(q)) => a e cy(imgF(p))]

                        4 Conclusion, 229

 

                  

                   Suppose...

 

                        265  r e imgG(cy(imgF(q)))

                              Premise

 

                        266  cy(imgF(q)) e py

                        => ALL(c):[c e imgG(cy(imgF(q))) <=> EXIST(d):[d e cy(imgF(q)) & g(d)=c]]

                              U Spec, 66

 

                        267  q e px => imgF(q) e py

                              U Spec, 50

 

                        268  imgF(q) e py

                              Detach, 267, 198

 

                        269  imgF(q) e py => cy(imgF(q)) e py

                              U Spec, 81

 

                        270  cy(imgF(q)) e py

                              Detach, 269, 268

 

                        271  ALL(c):[c e imgG(cy(imgF(q))) <=> EXIST(d):[d e cy(imgF(q)) & g(d)=c]]

                              Detach, 266, 270

 

                        272  r e imgG(cy(imgF(q))) <=> EXIST(d):[d e cy(imgF(q)) & g(d)=r]

                              U Spec, 271

 

                        273  [r e imgG(cy(imgF(q))) => EXIST(d):[d e cy(imgF(q)) & g(d)=r]]

                        & [EXIST(d):[d e cy(imgF(q)) & g(d)=r] => r e imgG(cy(imgF(q)))]

                              Iff-And, 272

 

                        274  r e imgG(cy(imgF(q))) => EXIST(d):[d e cy(imgF(q)) & g(d)=r]

                              Split, 273

 

                        275  EXIST(d):[d e cy(imgF(q)) & g(d)=r] => r e imgG(cy(imgF(q)))

                              Split, 273

 

                        276  EXIST(d):[d e cy(imgF(q)) & g(d)=r]

                              Detach, 274, 265

 

                        277  s e cy(imgF(q)) & g(s)=r

                              E Spec, 276

 

                        278  s e cy(imgF(q))

                              Split, 277

 

                        279  g(s)=r

                              Split, 277

 

                        280  cy(imgF(p)) e py

                        => ALL(c):[c e imgG(cy(imgF(p))) <=> EXIST(d):[d e cy(imgF(p)) & g(d)=c]]

                              U Spec, 66

 

                        281  p e px => imgF(p) e py

                              U Spec, 50

 

                        282  imgF(p) e py

                              Detach, 281, 197

 

                        283  imgF(p) e py => cy(imgF(p)) e py

                              U Spec, 81

 

                        284  cy(imgF(p)) e py

                              Detach, 283, 282

 

                        285  ALL(c):[c e imgG(cy(imgF(p))) <=> EXIST(d):[d e cy(imgF(p)) & g(d)=c]]

                              Detach, 280, 284

 

                        286  r e imgG(cy(imgF(p))) <=> EXIST(d):[d e cy(imgF(p)) & g(d)=r]

                              U Spec, 285

 

                        287  [r e imgG(cy(imgF(p))) => EXIST(d):[d e cy(imgF(p)) & g(d)=r]]

                        & [EXIST(d):[d e cy(imgF(p)) & g(d)=r] => r e imgG(cy(imgF(p)))]

                              Iff-And, 286

 

                        288  r e imgG(cy(imgF(p))) => EXIST(d):[d e cy(imgF(p)) & g(d)=r]

                              Split, 287

 

                        289  EXIST(d):[d e cy(imgF(p)) & g(d)=r] => r e imgG(cy(imgF(p)))

                              Split, 287

 

                        290  s e cy(imgF(q)) => s e cy(imgF(p))

                              U Spec, 264

 

                        291  s e cy(imgF(p))

                              Detach, 290, 278

 

                        292  s e cy(imgF(p)) & g(s)=r

                              Join, 291, 279

 

                        293  EXIST(d):[d e cy(imgF(p)) & g(d)=r]

                              E Gen, 292

 

                        294  r e imgG(cy(imgF(p)))

                              Detach, 289, 293

 

              As Required:

 

                  295  ALL(a):[a e imgG(cy(imgF(q))) => a e imgG(cy(imgF(p)))]

                        4 Conclusion, 265

 

                  

                   Suppose...

 

                        296  r e cx(imgG(cy(imgF(p))))

                              Premise

 

                        297  imgG(cy(imgF(p))) e px => ALL(c):[c e x => [c e cx(imgG(cy(imgF(p)))) <=> ~c e imgG(cy(imgF(p)))]]

                              U Spec, 74

 

                        298  imgG(cy(imgF(q))) e px => ALL(c):[c e x => [c e cx(imgG(cy(imgF(q)))) <=> ~c e imgG(cy(imgF(q)))]]

                              U Spec, 74

 

                        299  p e px => imgF(p) e py

                              U Spec, 50

 

                        300  imgF(p) e py

                              Detach, 299, 197

 

                        301  imgF(p) e py => cy(imgF(p)) e py

                              U Spec, 81

 

                        302  cy(imgF(p)) e py

                              Detach, 301, 300

 

                        303  cy(imgF(p)) e py => imgG(cy(imgF(p))) e px

                              U Spec, 65

 

                        304  imgG(cy(imgF(p))) e px

                              Detach, 303, 302

 

                        305  imgG(cy(imgF(p))) e px => cx(imgG(cy(imgF(p)))) e px

                              U Spec, 73

 

                        306  cx(imgG(cy(imgF(p)))) e px

                              Detach, 305, 304

 

                        307  ALL(c):[c e x => [c e cx(imgG(cy(imgF(p)))) <=> ~c e imgG(cy(imgF(p)))]]

                              Detach, 297, 304

 

                        308  r e x => [r e cx(imgG(cy(imgF(p)))) <=> ~r e imgG(cy(imgF(p)))]

                              U Spec, 307

 

                        309  cx(imgG(cy(imgF(p)))) e px <=> Set(cx(imgG(cy(imgF(p))))) & ALL(d):[d e cx(imgG(cy(imgF(p)))) => d e x]

                              U Spec, 23

 

                        310  [cx(imgG(cy(imgF(p)))) e px => Set(cx(imgG(cy(imgF(p))))) & ALL(d):[d e cx(imgG(cy(imgF(p)))) => d e x]]

                        & [Set(cx(imgG(cy(imgF(p))))) & ALL(d):[d e cx(imgG(cy(imgF(p)))) => d e x] => cx(imgG(cy(imgF(p)))) e px]

                              Iff-And, 309

 

                        311  cx(imgG(cy(imgF(p)))) e px => Set(cx(imgG(cy(imgF(p))))) & ALL(d):[d e cx(imgG(cy(imgF(p)))) => d e x]

                              Split, 310

 

                        312  Set(cx(imgG(cy(imgF(p))))) & ALL(d):[d e cx(imgG(cy(imgF(p)))) => d e x] => cx(imgG(cy(imgF(p)))) e px

                              Split, 310

 

                        313  Set(cx(imgG(cy(imgF(p))))) & ALL(d):[d e cx(imgG(cy(imgF(p)))) => d e x]

                              Detach, 311, 306

 

                        314  Set(cx(imgG(cy(imgF(p)))))

                              Split, 313

 

                        315  ALL(d):[d e cx(imgG(cy(imgF(p)))) => d e x]

                              Split, 313

 

                        316  r e cx(imgG(cy(imgF(p)))) => r e x

                              U Spec, 315

 

                        317  r e x

                              Detach, 316, 296

 

                        318  r e cx(imgG(cy(imgF(p)))) <=> ~r e imgG(cy(imgF(p)))

                              Detach, 308, 317

 

                        319  [r e cx(imgG(cy(imgF(p)))) => ~r e imgG(cy(imgF(p)))]

                        & [~r e imgG(cy(imgF(p))) => r e cx(imgG(cy(imgF(p))))]

                              Iff-And, 318

 

                        320  r e cx(imgG(cy(imgF(p)))) => ~r e imgG(cy(imgF(p)))

                              Split, 319

 

                        321  ~r e imgG(cy(imgF(p))) => r e cx(imgG(cy(imgF(p))))

                              Split, 319

 

                        322  ~r e imgG(cy(imgF(p)))

                              Detach, 320, 296

 

                        323  q e px => imgF(q) e py

                              U Spec, 50

 

                        324  imgF(q) e py

                              Detach, 323, 198

 

                        325  imgF(q) e py => cy(imgF(q)) e py

                              U Spec, 81

 

                        326  cy(imgF(q)) e py

                              Detach, 325, 324

 

                        327  cy(imgF(q)) e py => imgG(cy(imgF(q))) e px

                              U Spec, 65

 

                        328  imgG(cy(imgF(q))) e px

                              Detach, 327, 326

 

                        329  imgG(cy(imgF(q))) e px => cx(imgG(cy(imgF(q)))) e px

                              U Spec, 73

 

                        330  cx(imgG(cy(imgF(q)))) e px

                              Detach, 329, 328

 

                        331  ALL(c):[c e x => [c e cx(imgG(cy(imgF(q)))) <=> ~c e imgG(cy(imgF(q)))]]

                              Detach, 298, 328

 

                        332  r e x => [r e cx(imgG(cy(imgF(q)))) <=> ~r e imgG(cy(imgF(q)))]

                              U Spec, 331

 

                        333  r e cx(imgG(cy(imgF(q)))) <=> ~r e imgG(cy(imgF(q)))

                              Detach, 332, 317

 

                        334  [r e cx(imgG(cy(imgF(q)))) => ~r e imgG(cy(imgF(q)))]

                        & [~r e imgG(cy(imgF(q))) => r e cx(imgG(cy(imgF(q))))]

                              Iff-And, 333

 

                        335  r e cx(imgG(cy(imgF(q)))) => ~r e imgG(cy(imgF(q)))

                              Split, 334

 

                        336  ~r e imgG(cy(imgF(q))) => r e cx(imgG(cy(imgF(q))))

                              Split, 334

 

                        337  r e imgG(cy(imgF(q))) => r e imgG(cy(imgF(p)))

                              U Spec, 295

 

                        338  ~r e imgG(cy(imgF(p))) => ~r e imgG(cy(imgF(q)))

                              Contra, 337

 

                        339  ~r e imgG(cy(imgF(q)))

                              Detach, 338, 322

 

                        340  r e cx(imgG(cy(imgF(q))))

                              Detach, 336, 339

 

              As Required:

 

                  341  ALL(a):[a e cx(imgG(cy(imgF(p))))

                   => a e cx(imgG(cy(imgF(q))))]

                        4 Conclusion, 296

 

                  342  p e px => h(p)=cx(imgG(cy(imgF(p))))

                        U Spec, 192

 

                  343  h(p)=cx(imgG(cy(imgF(p))))

                        Detach, 342, 197

 

                  344  q e px => h(q)=cx(imgG(cy(imgF(q))))

                        U Spec, 192

 

                  345  h(q)=cx(imgG(cy(imgF(q))))

                        Detach, 344, 198

 

                  346  ALL(a):[a e h(p)

                   => a e cx(imgG(cy(imgF(q))))]

                        Substitute, 343, 341

 

                  347  ALL(a):[a e h(p)

                   => a e h(q)]

                        Substitute, 345, 346

 

                  348  ALL(b):[Subset(h(p),b) <=> ALL(c):[c e h(p) => c e b]]

                        U Spec, 1

 

                  349  Subset(h(p),h(q)) <=> ALL(c):[c e h(p) => c e h(q)]

                        U Spec, 348

 

                  350  [Subset(h(p),h(q)) => ALL(c):[c e h(p) => c e h(q)]]

                   & [ALL(c):[c e h(p) => c e h(q)] => Subset(h(p),h(q))]

                        Iff-And, 349

 

                  351  Subset(h(p),h(q)) => ALL(c):[c e h(p) => c e h(q)]

                        Split, 350

 

                  352  ALL(c):[c e h(p) => c e h(q)] => Subset(h(p),h(q))

                        Split, 350

 

                  353  Subset(h(p),h(q))

                        Detach, 352, 347

 

            354  Subset(p,q) => Subset(h(p),h(q))

                  4 Conclusion, 199

 

     As Required:

 

      355  ALL(a):ALL(b):[a e px & b e px => [Subset(a,b) => Subset(h(a),h(b))]]

            4 Conclusion, 196

 

         

          Prove: ALL(a):[a e px => Set(a) & Subset(a,x)]

         

          Suppose...

 

            356  p e px

                  Premise

 

            357  p e px <=> Set(p) & ALL(d):[d e p => d e x]

                  U Spec, 23

 

            358  [p e px => Set(p) & ALL(d):[d e p => d e x]]

              & [Set(p) & ALL(d):[d e p => d e x] => p e px]

                  Iff-And, 357

 

            359  p e px => Set(p) & ALL(d):[d e p => d e x]

                  Split, 358

 

            360  Set(p) & ALL(d):[d e p => d e x] => p e px

                  Split, 358

 

            361  Set(p) & ALL(d):[d e p => d e x]

                  Detach, 359, 356

 

            362  Set(p)

                  Split, 361

 

            363  ALL(d):[d e p => d e x]

                  Split, 361

 

            364  ALL(b):[Subset(p,b) <=> ALL(c):[c e p => c e b]]

                  U Spec, 1

 

            365  Subset(p,x) <=> ALL(c):[c e p => c e x]

                  U Spec, 364

 

            366  [Subset(p,x) => ALL(c):[c e p => c e x]]

              & [ALL(c):[c e p => c e x] => Subset(p,x)]

                  Iff-And, 365

 

            367  Subset(p,x) => ALL(c):[c e p => c e x]

                  Split, 366

 

            368  ALL(c):[c e p => c e x] => Subset(p,x)

                  Split, 366

 

            369  Subset(p,x)

                  Detach, 368, 363

 

            370  Set(p) & Subset(p,x)

                  Join, 362, 369

 

     As Required:

 

      371  ALL(a):[a e px => Set(a) & Subset(a,x)]

            4 Conclusion, 356

 

      372  Set(x) & Set(px)

            Join, 12, 22

 

      373  Set(x) & Set(px)

          & ALL(a):[a e px => Set(a) & Subset(a,x)]

            Join, 372, 371

 

      374  Set(x) & Set(px)

          & ALL(a):[a e px => Set(a) & Subset(a,x)]

          & ALL(a):[a e px => h(a) e px]

            Join, 373, 170

 

         

          Prove: ALL(a):[Set(a) & Subset(a,x) => a e px]

         

          Suppose...

 

            375  Set(p) & Subset(p,x)

                  Premise

 

            376  Set(p)

                  Split, 375

 

            377  Subset(p,x)

                  Split, 375

 

            378  ALL(b):[Subset(p,b) <=> ALL(c):[c e p => c e b]]

                  U Spec, 1

 

            379  Subset(p,x) <=> ALL(c):[c e p => c e x]

                  U Spec, 378

 

            380  [Subset(p,x) => ALL(c):[c e p => c e x]]

              & [ALL(c):[c e p => c e x] => Subset(p,x)]

                  Iff-And, 379

 

            381  Subset(p,x) => ALL(c):[c e p => c e x]

                  Split, 380

 

            382  ALL(c):[c e p => c e x] => Subset(p,x)

                  Split, 380

 

            383  ALL(c):[c e p => c e x]

                  Detach, 381, 377

 

            384  p e px <=> Set(p) & ALL(d):[d e p => d e x]

                  U Spec, 23

 

            385  [p e px => Set(p) & ALL(d):[d e p => d e x]]

              & [Set(p) & ALL(d):[d e p => d e x] => p e px]

                  Iff-And, 384

 

            386  p e px => Set(p) & ALL(d):[d e p => d e x]

                  Split, 385

 

            387  Set(p) & ALL(d):[d e p => d e x] => p e px

                  Split, 385

 

            388  Set(p) & ALL(c):[c e p => c e x]

                  Join, 376, 383

 

            389  p e px

                  Detach, 387, 388

 

     As Required:

 

      390  ALL(a):[Set(a) & Subset(a,x) => a e px]

            4 Conclusion, 375

 

      391  ALL(a):[[a e px => Set(a) & Subset(a,x)] & [Set(a) & Subset(a,x) => a e px]]

            Join, 371, 390

 

     As Required:

 

      392  ALL(a):[a e px <=> Set(a) & Subset(a,x)]

            Iff-And, 391

 

      393  Set(x) & Set(px)

            Join, 12, 22

 

      394  Set(x) & Set(px)

          & ALL(a):[a e px <=> Set(a) & Subset(a,x)]

            Join, 393, 392

 

      395  Set(x) & Set(px)

          & ALL(a):[a e px <=> Set(a) & Subset(a,x)]

          & ALL(a):[a e px => h(a) e px]

            Join, 394, 170

 

      396  Set(x) & Set(px)

          & ALL(a):[a e px <=> Set(a) & Subset(a,x)]

          & ALL(a):[a e px => h(a) e px]

          & ALL(a):ALL(b):[a e px & b e px => [Subset(a,b) => Subset(h(a),h(b))]]

            Join, 395, 355

 

      397  EXIST(a):[Set(a) & Subset(a,x) & h(a)=a]

            Detach, 195, 396

 

      398  Set(z) & Subset(z,x) & h(z)=z

            E Spec, 397

 

    

     Define: z  (the fixed point)

     *********

 

      399  Set(z)

            Split, 398

 

      400  Subset(z,x)

            Split, 398

 

      401  h(z)=z

            Split, 398

 

      402  z e px => h(z)=cx(imgG(cy(imgF(z))))

            U Spec, 192

 

      403  ALL(b):[Subset(z,b) <=> ALL(c):[c e z => c e b]]

            U Spec, 1

 

      404  Subset(z,x) <=> ALL(c):[c e z => c e x]

            U Spec, 403

 

      405  [Subset(z,x) => ALL(c):[c e z => c e x]]

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

            Iff-And, 404

 

      406  Subset(z,x) => ALL(c):[c e z => c e x]

            Split, 405

 

      407  ALL(c):[c e z => c e x] => Subset(z,x)

            Split, 405

 

      408  ALL(c):[c e z => c e x]

            Detach, 406, 400

 

      409  z e px <=> Set(z) & ALL(d):[d e z => d e x]

            U Spec, 23

 

      410  [z e px => Set(z) & ALL(d):[d e z => d e x]]

          & [Set(z) & ALL(d):[d e z => d e x] => z e px]

            Iff-And, 409

 

      411  z e px => Set(z) & ALL(d):[d e z => d e x]

            Split, 410

 

      412  Set(z) & ALL(d):[d e z => d e x] => z e px

            Split, 410

 

      413  Set(z) & ALL(c):[c e z => c e x]

            Join, 399, 408

 

     As Required:

 

      414  z e px

            Detach, 412, 413

 

      415  h(z)=cx(imgG(cy(imgF(z))))

            Detach, 402, 414

 

      416  z=cx(imgG(cy(imgF(z))))

            Substitute, 401, 415

 

      417  cx(z)=cx(z)

            Reflex

 

     As Required:

 

      418  cx(cx(imgG(cy(imgF(z)))))=cx(z)

            Substitute, 416, 417

 

      419  z e px => imgF(z) e py

            U Spec, 50

 

      420  imgF(z) e py

            Detach, 419, 414

 

      421  imgF(z) e py => cy(imgF(z)) e py

            U Spec, 81

 

      422  cy(imgF(z)) e py

            Detach, 421, 420

 

      423  cy(imgF(z)) e py => imgG(cy(imgF(z))) e px

            U Spec, 65

 

     As Required:

 

      424  imgG(cy(imgF(z))) e px

            Detach, 423, 422

 

      425  ALL(b):[Subset(imgG(cy(imgF(z))),b) <=> ALL(c):[c e imgG(cy(imgF(z))) => c e b]]

            U Spec, 1

 

      426  Subset(imgG(cy(imgF(z))),x) <=> ALL(c):[c e imgG(cy(imgF(z))) => c e x]

            U Spec, 425

 

      427  [Subset(imgG(cy(imgF(z))),x) => ALL(c):[c e imgG(cy(imgF(z))) => c e x]]

          & [ALL(c):[c e imgG(cy(imgF(z))) => c e x] => Subset(imgG(cy(imgF(z))),x)]

            Iff-And, 426

 

      428  Subset(imgG(cy(imgF(z))),x) => ALL(c):[c e imgG(cy(imgF(z))) => c e x]

            Split, 427

 

      429  ALL(c):[c e imgG(cy(imgF(z))) => c e x] => Subset(imgG(cy(imgF(z))),x)

            Split, 427

 

      430  imgG(cy(imgF(z))) e px <=> Set(imgG(cy(imgF(z)))) & ALL(d):[d e imgG(cy(imgF(z))) => d e x]

            U Spec, 23

 

      431  [imgG(cy(imgF(z))) e px => Set(imgG(cy(imgF(z)))) & ALL(d):[d e imgG(cy(imgF(z))) => d e x]]

          & [Set(imgG(cy(imgF(z)))) & ALL(d):[d e imgG(cy(imgF(z))) => d e x] => imgG(cy(imgF(z))) e px]

            Iff-And, 430

 

      432  imgG(cy(imgF(z))) e px => Set(imgG(cy(imgF(z)))) & ALL(d):[d e imgG(cy(imgF(z))) => d e x]

            Split, 431

 

      433  Set(imgG(cy(imgF(z)))) & ALL(d):[d e imgG(cy(imgF(z))) => d e x] => imgG(cy(imgF(z))) e px

            Split, 431

 

      434  Set(imgG(cy(imgF(z)))) & ALL(d):[d e imgG(cy(imgF(z))) => d e x]

            Detach, 432, 424

 

      435  Set(imgG(cy(imgF(z))))

            Split, 434

 

      436  ALL(d):[d e imgG(cy(imgF(z))) => d e x]

            Split, 434

 

     As Required:

 

      437  Subset(imgG(cy(imgF(z))),x)

            Detach, 429, 436

 

     Apply Complement of a Complement Lemma

 

      438  ALL(ps):ALL(f):[Set(x)

          & Set(ps)

          & ALL(a):[a e ps <=> Set(a) & ALL(b):[b e a => b e x]]

          & ALL(a):[a e ps => f(a) e ps]

          & ALL(a):[a e ps => ALL(b):[b e x => [b e f(a) <=> ~b e a]]]

          => ALL(a):[a e ps => f(f(a))=a]]

            U Spec, 8

 

      439  ALL(f):[Set(x)

          & Set(px)

          & ALL(a):[a e px <=> Set(a) & ALL(b):[b e a => b e x]]

          & ALL(a):[a e px => f(a) e px]

          & ALL(a):[a e px => ALL(b):[b e x => [b e f(a) <=> ~b e a]]]

          => ALL(a):[a e px => f(f(a))=a]]

            U Spec, 438

 

      440  Set(x)

          & Set(px)

          & ALL(a):[a e px <=> Set(a) & ALL(b):[b e a => b e x]]

          & ALL(a):[a e px => cx(a) e px]

          & ALL(a):[a e px => ALL(b):[b e x => [b e cx(a) <=> ~b e a]]]

          => ALL(a):[a e px => cx(cx(a))=a]

            U Spec, 439

 

      441  Set(x) & Set(px)

            Join, 12, 22

 

      442  Set(x) & Set(px)

          & ALL(c):[c e px <=> Set(c) & ALL(d):[d e c => d e x]]

            Join, 441, 23

 

      443  Set(x) & Set(px)

          & ALL(c):[c e px <=> Set(c) & ALL(d):[d e c => d e x]]

          & ALL(a):[a e px => cx(a) e px]

            Join, 442, 73

 

      444  Set(x) & Set(px)

          & ALL(c):[c e px <=> Set(c) & ALL(d):[d e c => d e x]]

          & ALL(a):[a e px => cx(a) e px]

          & ALL(a):[a e px => ALL(c):[c e x => [c e cx(a) <=> ~c e a]]]

            Join, 443, 74

 

      445  ALL(a):[a e px => cx(cx(a))=a]

            Detach, 440, 444

 

      446  imgG(cy(imgF(z))) e px => cx(cx(imgG(cy(imgF(z)))))=imgG(cy(imgF(z)))

            U Spec, 445

 

     As Required:

 

      447  cx(cx(imgG(cy(imgF(z)))))=imgG(cy(imgF(z)))

            Detach, 446, 424

 

     As Required:

 

      448  imgG(cy(imgF(z)))=cx(z)

            Substitute, 447, 418

 

      449  z e px => imgF(z) e py

            U Spec, 50

 

    

     Define: imgF(z) 

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

 

      450  imgF(z) e py

            Detach, 449, 414

 

      451  imgF(z) e py <=> Set(imgF(z)) & ALL(d):[d e imgF(z) => d e y]

            U Spec, 28

 

      452  [imgF(z) e py => Set(imgF(z)) & ALL(d):[d e imgF(z) => d e y]]

          & [Set(imgF(z)) & ALL(d):[d e imgF(z) => d e y] => imgF(z) e py]

            Iff-And, 451

 

      453  imgF(z) e py => Set(imgF(z)) & ALL(d):[d e imgF(z) => d e y]

            Split, 452

 

      454  Set(imgF(z)) & ALL(d):[d e imgF(z) => d e y] => imgF(z) e py

            Split, 452

 

      455  Set(imgF(z)) & ALL(d):[d e imgF(z) => d e y]

            Detach, 453, 450

 

      456  Set(imgF(z))

            Split, 455

 

      457  ALL(d):[d e imgF(z) => d e y]

            Split, 455

 

      458  z e px

          => ALL(c):[c e imgF(z) <=> EXIST(d):[d e z & f(d)=c]]

            U Spec, 51

 

      459  ALL(c):[c e imgF(z) <=> EXIST(d):[d e z & f(d)=c]]

            Detach, 458, 414

 

      460  imgF(z) e py => cy(imgF(z)) e py

            U Spec, 81

 

    

     Define: cy(imgF(z))

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

 

      461  cy(imgF(z)) e py

            Detach, 460, 450

 

      462  imgF(z) e py => ALL(c):[c e y => [c e cy(imgF(z)) <=> ~c e imgF(z)]]

            U Spec, 82

 

      463  ALL(c):[c e y => [c e cy(imgF(z)) <=> ~c e imgF(z)]]

            Detach, 462, 450

 

      464  z e px => cx(z) e px

            U Spec, 73

 

    

     Define: cx(z)

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

 

      465  cx(z) e px

            Detach, 464, 414

 

      466  z e px => ALL(c):[c e x => [c e cx(z) <=> ~c e z]]

            U Spec, 74

 

      467  ALL(c):[c e x => [c e cx(z) <=> ~c e z]]

            Detach, 466, 414

 

      468  cy(imgF(z)) e py => imgG(cy(imgF(z))) e px

            U Spec, 65

 

    

     Define: imgG(cy(imgF(z))) 

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

 

      469  imgG(cy(imgF(z))) e px

            Detach, 468, 461

 

      470  cy(imgF(z)) e py

          => ALL(c):[c e imgG(cy(imgF(z))) <=> EXIST(d):[d e cy(imgF(z)) & g(d)=c]]

            U Spec, 66

 

      471  ALL(c):[c e imgG(cy(imgF(z))) <=> EXIST(d):[d e cy(imgF(z)) & g(d)=c]]

            Detach, 470, 461

 

         

          Prove: ALL(a):[a e z => f(a) e imgF(z)]

         

          Suppose...

 

            472  p e z

                  Premise

 

            473  f(p) e imgF(z) <=> EXIST(d):[d e z & f(d)=f(p)]

                  U Spec, 459

 

            474  [f(p) e imgF(z) => EXIST(d):[d e z & f(d)=f(p)]]

              & [EXIST(d):[d e z & f(d)=f(p)] => f(p) e imgF(z)]

                  Iff-And, 473

 

            475  f(p) e imgF(z) => EXIST(d):[d e z & f(d)=f(p)]

                  Split, 474

 

            476  EXIST(d):[d e z & f(d)=f(p)] => f(p) e imgF(z)

                  Split, 474

 

            477  f(p)=f(p)

                  Reflex

 

            478  p e z & f(p)=f(p)

                  Join, 472, 477

 

            479  EXIST(d):[d e z & f(d)=f(p)]

                  E Gen, 478

 

            480  f(p) e imgF(z)

                  Detach, 476, 479

 

    

     Define: f   f: z -> imgF(z)   (a restriction on f)

     *********

 

      481  ALL(a):[a e z => f(a) e imgF(z)]

            4 Conclusion, 472

 

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

            U Spec, 2

 

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

            U Spec, 482

 

      484  Injection(f,x,y) <=> ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]

            U Spec, 483

 

      485  [Injection(f,x,y) => ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]]

          & [ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]] => Injection(f,x,y)]

            Iff-And, 484

 

      486  Injection(f,x,y) => ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]

            Split, 485

 

      487  ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]] => Injection(f,x,y)

            Split, 485

 

      488  ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]

            Detach, 486, 16

 

            489  p e z & q e z

                  Premise

 

            490  p e z

                  Split, 489

 

            491  q e z

                  Split, 489

 

            492  ALL(b):[Subset(z,b) <=> ALL(c):[c e z => c e b]]

                  U Spec, 1

 

            493  Subset(z,x) <=> ALL(c):[c e z => c e x]

                  U Spec, 492

 

            494  [Subset(z,x) => ALL(c):[c e z => c e x]]

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

                  Iff-And, 493

 

            495  Subset(z,x) => ALL(c):[c e z => c e x]

                  Split, 494

 

            496  ALL(c):[c e z => c e x] => Subset(z,x)

                  Split, 494

 

            497  ALL(c):[c e z => c e x]

                  Detach, 495, 400

 

            498  p e z => p e x

                  U Spec, 497

 

            499  p e x

                  Detach, 498, 490

 

            500  q e z => q e x

                  U Spec, 497

 

            501  q e x

                  Detach, 500, 491

 

            502  ALL(d):[p e x & d e x => [f(p)=f(d) => p=d]]

                  U Spec, 488

 

            503  p e x & q e x => [f(p)=f(q) => p=q]

                  U Spec, 502

 

            504  p e x & q e x

                  Join, 499, 501

 

            505  f(p)=f(q) => p=q

                  Detach, 503, 504

 

     f: z -> imgF(z) is injective

 

      506  ALL(a):ALL(b):[a e z & b e z => [f(a)=f(b) => a=b]]

            4 Conclusion, 489

 

     Apply Existence of Inverse Lemma

 

      507  ALL(y):ALL(f):[Set(z) & Set(y)

          & ALL(a):[a e z => f(a) e y]

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

          & ALL(a):ALL(b):[a e z & b e z => [f(a)=f(b) => a=b]]

          => EXIST(f'):[ALL(a):[a e y => f'(a) e z]

          & ALL(a):ALL(b):[a e z & b e y => [f'(b)=a <=> f(a)=b]]]]

            U Spec, 9

 

      508  ALL(f):[Set(z) & Set(imgF(z))

          & ALL(a):[a e z => f(a) e imgF(z)]

          & ALL(a):[a e imgF(z) => EXIST(b):[b e z & f(b)=a]]

          & ALL(a):ALL(b):[a e z & b e z => [f(a)=f(b) => a=b]]

          => EXIST(f'):[ALL(a):[a e imgF(z) => f'(a) e z]

          & ALL(a):ALL(b):[a e z & b e imgF(z) => [f'(b)=a <=> f(a)=b]]]]

            U Spec, 507

 

      509  Set(z) & Set(imgF(z))

          & ALL(a):[a e z => f(a) e imgF(z)]

          & ALL(a):[a e imgF(z) => EXIST(b):[b e z & f(b)=a]]

          & ALL(a):ALL(b):[a e z & b e z => [f(a)=f(b) => a=b]]

          => EXIST(f'):[ALL(a):[a e imgF(z) => f'(a) e z]

          & ALL(a):ALL(b):[a e z & b e imgF(z) => [f'(b)=a <=> f(a)=b]]]

            U Spec, 508

 

      510  Set(z) & Set(imgF(z))

            Join, 399, 456

 

      511  Set(z) & Set(imgF(z))

          & ALL(a):[a e z => f(a) e imgF(z)]

            Join, 510, 481

 

         

          Prove: ALL(a):[a e cy(imgF(z)) => g(a) e imgG(cy(imgF(z))]

 

            512  p e cy(imgF(z))

                  Premise

 

            513  g(p) e imgG(cy(imgF(z))) <=> EXIST(d):[d e cy(imgF(z)) & g(d)=g(p)]

                  U Spec, 471

 

            514  [g(p) e imgG(cy(imgF(z))) => EXIST(d):[d e cy(imgF(z)) & g(d)=g(p)]]

              & [EXIST(d):[d e cy(imgF(z)) & g(d)=g(p)] => g(p) e imgG(cy(imgF(z)))]

                  Iff-And, 513

 

            515  g(p) e imgG(cy(imgF(z))) => EXIST(d):[d e cy(imgF(z)) & g(d)=g(p)]

                  Split, 514

 

            516  EXIST(d):[d e cy(imgF(z)) & g(d)=g(p)] => g(p) e imgG(cy(imgF(z)))

                  Split, 514

 

            517  g(p)=g(p)

                  Reflex

 

            518  p e cy(imgF(z)) & g(p)=g(p)

                  Join, 512, 517

 

            519  EXIST(d):[d e cy(imgF(z)) & g(d)=g(p)]

                  E Gen, 518

 

            520  g(p) e imgG(cy(imgF(z)))

                  Detach, 516, 519

 

    

     Define: g   g: cy(imgF(z)) -> imgG(cy(imgF(z))

     *********

 

      521  ALL(a):[a e cy(imgF(z)) => g(a) e imgG(cy(imgF(z)))]

            4 Conclusion, 512

 

         

          Prove: ALL(a):ALL(b):[a e cy(imgF(z)) & b e cy(imgF(z)) => [g(a)=g(b) => a=b]]

         

          Suppose...

 

            522  p e cy(imgF(z)) & q e cy(imgF(z))

                  Premise

 

            523  p e cy(imgF(z))

                  Split, 522

 

            524  q e cy(imgF(z))

                  Split, 522

 

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

                  U Spec, 2

 

            526  ALL(b):[Injection(g,y,b) <=> ALL(c):ALL(d):[c e y & d e y => [g(c)=g(d) => c=d]]]

                  U Spec, 525

 

            527  Injection(g,y,x) <=> ALL(c):ALL(d):[c e y & d e y => [g(c)=g(d) => c=d]]

                  U Spec, 526

 

            528  [Injection(g,y,x) => ALL(c):ALL(d):[c e y & d e y => [g(c)=g(d) => c=d]]]

              & [ALL(c):ALL(d):[c e y & d e y => [g(c)=g(d) => c=d]] => Injection(g,y,x)]

                  Iff-And, 527

 

            529  Injection(g,y,x) => ALL(c):ALL(d):[c e y & d e y => [g(c)=g(d) => c=d]]

                  Split, 528

 

            530  ALL(c):ALL(d):[c e y & d e y => [g(c)=g(d) => c=d]] => Injection(g,y,x)

                  Split, 528

 

            531  ALL(c):ALL(d):[c e y & d e y => [g(c)=g(d) => c=d]]

                  Detach, 529, 17

 

            532  cy(imgF(z)) e py <=> Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]

                  U Spec, 28

 

            533  [cy(imgF(z)) e py => Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]]

              & [Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y] => cy(imgF(z)) e py]

                  Iff-And, 532

 

            534  cy(imgF(z)) e py => Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]

                  Split, 533

 

            535  Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y] => cy(imgF(z)) e py

                  Split, 533

 

            536  Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]

                  Detach, 534, 461

 

            537  Set(cy(imgF(z)))

                  Split, 536

 

            538  ALL(d):[d e cy(imgF(z)) => d e y]

                  Split, 536

 

            539  p e cy(imgF(z)) => p e y

                  U Spec, 538

 

            540  p e y

                  Detach, 539, 523

 

            541  q e cy(imgF(z)) => q e y

                  U Spec, 538

 

            542  q e y

                  Detach, 541, 524

 

            543  ALL(d):[p e y & d e y => [g(p)=g(d) => p=d]]

                  U Spec, 531

 

            544  p e y & q e y => [g(p)=g(q) => p=q]

                  U Spec, 543

 

            545  p e y & q e y

                  Join, 540, 542

 

            546  g(p)=g(q) => p=q

                  Detach, 544, 545

 

     Function g: cy(imgF(z)) -> imgG(cy(imgF(z)) is injective

 

      547  ALL(a):ALL(b):[a e cy(imgF(z)) & b e cy(imgF(z)) => [g(a)=g(b) => a=b]]

            4 Conclusion, 522

 

         

          Prove: ALL(a):[a e imgG(cy(imgF(z)))

                 => EXIST(d):[d e cy(imgF(z)) & g(d)=a]]

         

          Suppose...

 

            548  p e imgG(cy(imgF(z)))

                  Premise

 

            549  p e imgG(cy(imgF(z))) <=> EXIST(d):[d e cy(imgF(z)) & g(d)=p]

                  U Spec, 471

 

            550  [p e imgG(cy(imgF(z))) => EXIST(d):[d e cy(imgF(z)) & g(d)=p]]

              & [EXIST(d):[d e cy(imgF(z)) & g(d)=p] => p e imgG(cy(imgF(z)))]

                  Iff-And, 549

 

            551  p e imgG(cy(imgF(z))) => EXIST(d):[d e cy(imgF(z)) & g(d)=p]

                  Split, 550

 

            552  EXIST(d):[d e cy(imgF(z)) & g(d)=p] => p e imgG(cy(imgF(z)))

                  Split, 550

 

            553  EXIST(d):[d e cy(imgF(z)) & g(d)=p]

                  Detach, 551, 548

 

     Function g: cy(imgF(z)) -> imgG(cy(imgF(z)) is surjective

 

      554  ALL(a):[a e imgG(cy(imgF(z)))

          => EXIST(d):[d e cy(imgF(z)) & g(d)=a]]

            4 Conclusion, 548

 

      555  ALL(a):[a e cy(imgF(z)) => g(a) e cx(z)]

            Substitute, 448, 521

 

      556  ALL(a):[a e cx(z)

          => EXIST(d):[d e cy(imgF(z)) & g(d)=a]]

            Substitute, 448, 554

 

      557  ALL(y):ALL(f):[Set(cy(imgF(z))) & Set(y)

          & ALL(a):[a e cy(imgF(z)) => f(a) e y]

          & ALL(a):[a e y => EXIST(b):[b e cy(imgF(z)) & f(b)=a]]

          & ALL(a):ALL(b):[a e cy(imgF(z)) & b e cy(imgF(z)) => [f(a)=f(b) => a=b]]

          => EXIST(f'):[ALL(a):[a e y => f'(a) e cy(imgF(z))]

          & ALL(a):ALL(b):[a e cy(imgF(z)) & b e y => [f'(b)=a <=> f(a)=b]]]]

            U Spec, 9

 

      558  ALL(f):[Set(cy(imgF(z))) & Set(cx(z))

          & ALL(a):[a e cy(imgF(z)) => f(a) e cx(z)]

          & ALL(a):[a e cx(z) => EXIST(b):[b e cy(imgF(z)) & f(b)=a]]

          & ALL(a):ALL(b):[a e cy(imgF(z)) & b e cy(imgF(z)) => [f(a)=f(b) => a=b]]

          => EXIST(f'):[ALL(a):[a e cx(z) => f'(a) e cy(imgF(z))]

          & ALL(a):ALL(b):[a e cy(imgF(z)) & b e cx(z) => [f'(b)=a <=> f(a)=b]]]]

            U Spec, 557

 

      559  Set(cy(imgF(z))) & Set(cx(z))

          & ALL(a):[a e cy(imgF(z)) => g(a) e cx(z)]

          & ALL(a):[a e cx(z) => EXIST(b):[b e cy(imgF(z)) & g(b)=a]]

          & ALL(a):ALL(b):[a e cy(imgF(z)) & b e cy(imgF(z)) => [g(a)=g(b) => a=b]]

          => EXIST(f'):[ALL(a):[a e cx(z) => f'(a) e cy(imgF(z))]

          & ALL(a):ALL(b):[a e cy(imgF(z)) & b e cx(z) => [f'(b)=a <=> g(a)=b]]]

            U Spec, 558

 

      560  cy(imgF(z)) e py <=> Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]

            U Spec, 28

 

      561  [cy(imgF(z)) e py => Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]]

          & [Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y] => cy(imgF(z)) e py]

            Iff-And, 560

 

      562  cy(imgF(z)) e py => Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]

            Split, 561

 

      563  Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y] => cy(imgF(z)) e py

            Split, 561

 

      564  Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]

            Detach, 562, 461

 

      565  Set(cy(imgF(z)))

            Split, 564

 

      566  ALL(d):[d e cy(imgF(z)) => d e y]

            Split, 564

 

      567  cx(z) e px <=> Set(cx(z)) & ALL(d):[d e cx(z) => d e x]

            U Spec, 23

 

      568  [cx(z) e px => Set(cx(z)) & ALL(d):[d e cx(z) => d e x]]

          & [Set(cx(z)) & ALL(d):[d e cx(z) => d e x] => cx(z) e px]

            Iff-And, 567

 

      569  cx(z) e px => Set(cx(z)) & ALL(d):[d e cx(z) => d e x]

            Split, 568

 

      570  Set(cx(z)) & ALL(d):[d e cx(z) => d e x] => cx(z) e px

            Split, 568

 

      571  Set(cx(z)) & ALL(d):[d e cx(z) => d e x]

            Detach, 569, 465

 

      572  Set(cx(z))

            Split, 571

 

      573  ALL(d):[d e cx(z) => d e x]

            Split, 571

 

      574  Set(cy(imgF(z))) & Set(cx(z))

            Join, 565, 572

 

      575  Set(cy(imgF(z))) & Set(cx(z))

          & ALL(a):[a e cy(imgF(z)) => g(a) e cx(z)]

            Join, 574, 555

 

      576  Set(cy(imgF(z))) & Set(cx(z))

          & ALL(a):[a e cy(imgF(z)) => g(a) e cx(z)]

          & ALL(a):[a e cx(z)

          => EXIST(d):[d e cy(imgF(z)) & g(d)=a]]

            Join, 575, 556

 

      577  Set(cy(imgF(z))) & Set(cx(z))

          & ALL(a):[a e cy(imgF(z)) => g(a) e cx(z)]

          & ALL(a):[a e cx(z)

          => EXIST(d):[d e cy(imgF(z)) & g(d)=a]]

          & ALL(a):ALL(b):[a e cy(imgF(z)) & b e cy(imgF(z)) => [g(a)=g(b) => a=b]]

            Join, 576, 547

 

      578  EXIST(f'):[ALL(a):[a e cx(z) => f'(a) e cy(imgF(z))]

          & ALL(a):ALL(b):[a e cy(imgF(z)) & b e cx(z) => [f'(b)=a <=> g(a)=b]]]

            Detach, 559, 577

 

      579  ALL(a):[a e cx(z) => g'(a) e cy(imgF(z))]

          & ALL(a):ALL(b):[a e cy(imgF(z)) & b e cx(z) => [g'(b)=a <=> g(a)=b]]

            E Spec, 578

 

    

     Define: g'  (inverse of g: cy(imgF(z)) -> cx(z)

     **********

 

      580  ALL(a):[a e cx(z) => g'(a) e cy(imgF(z))]

            Split, 579

 

      581  ALL(a):ALL(b):[a e cy(imgF(z)) & b e cx(z) => [g'(b)=a <=> g(a)=b]]

            Split, 579

 

    

     Apply Inverses are Bijections Lemma

 

      582  ALL(set2):ALL(func):ALL(inv):[Set(cy(imgF(z))) & Set(set2)

          & ALL(a):[a e cy(imgF(z)) => func(a) e set2]

          & ALL(a):[a e set2 => inv(a) e cy(imgF(z))]

          & ALL(a):ALL(b):[a e cy(imgF(z)) & b e set2 => [inv(b)=a <=> func(a)=b]]

          => ALL(a):ALL(b):[a e set2 & b e set2 => [inv(a)=inv(b) => a=b]]

          & ALL(a):[a e cy(imgF(z)) => EXIST(b):[b e set2 & inv(b)=a]]]

            U Spec, 10

 

      583  ALL(func):ALL(inv):[Set(cy(imgF(z))) & Set(imgG(cy(imgF(z))))

          & ALL(a):[a e cy(imgF(z)) => func(a) e imgG(cy(imgF(z)))]

          & ALL(a):[a e imgG(cy(imgF(z))) => inv(a) e cy(imgF(z))]

          & ALL(a):ALL(b):[a e cy(imgF(z)) & b e imgG(cy(imgF(z))) => [inv(b)=a <=> func(a)=b]]

          => ALL(a):ALL(b):[a e imgG(cy(imgF(z))) & b e imgG(cy(imgF(z))) => [inv(a)=inv(b) => a=b]]

          & ALL(a):[a e cy(imgF(z)) => EXIST(b):[b e imgG(cy(imgF(z))) & inv(b)=a]]]

            U Spec, 582

 

      584  ALL(inv):[Set(cy(imgF(z))) & Set(imgG(cy(imgF(z))))

          & ALL(a):[a e cy(imgF(z)) => g(a) e imgG(cy(imgF(z)))]

          & ALL(a):[a e imgG(cy(imgF(z))) => inv(a) e cy(imgF(z))]

          & ALL(a):ALL(b):[a e cy(imgF(z)) & b e imgG(cy(imgF(z))) => [inv(b)=a <=> g(a)=b]]

          => ALL(a):ALL(b):[a e imgG(cy(imgF(z))) & b e imgG(cy(imgF(z))) => [inv(a)=inv(b) => a=b]]

          & ALL(a):[a e cy(imgF(z)) => EXIST(b):[b e imgG(cy(imgF(z))) & inv(b)=a]]]

            U Spec, 583

 

      585  Set(cy(imgF(z))) & Set(imgG(cy(imgF(z))))

          & ALL(a):[a e cy(imgF(z)) => g(a) e imgG(cy(imgF(z)))]

          & ALL(a):[a e imgG(cy(imgF(z))) => g'(a) e cy(imgF(z))]

          & ALL(a):ALL(b):[a e cy(imgF(z)) & b e imgG(cy(imgF(z))) => [g'(b)=a <=> g(a)=b]]

          => ALL(a):ALL(b):[a e imgG(cy(imgF(z))) & b e imgG(cy(imgF(z))) => [g'(a)=g'(b) => a=b]]

          & ALL(a):[a e cy(imgF(z)) => EXIST(b):[b e imgG(cy(imgF(z))) & g'(b)=a]]

            U Spec, 584

 

      586  Set(cy(imgF(z))) & Set(imgG(cy(imgF(z))))

            Join, 565, 435

 

      587  Set(cy(imgF(z))) & Set(imgG(cy(imgF(z))))

          & ALL(a):[a e cy(imgF(z)) => g(a) e imgG(cy(imgF(z)))]

            Join, 586, 521

 

      588  Set(cy(imgF(z))) & Set(imgG(cy(imgF(z))))

          & ALL(a):[a e cy(imgF(z)) => g(a) e imgG(cy(imgF(z)))]

          & ALL(a):[a e cx(z) => g'(a) e cy(imgF(z))]

            Join, 587, 580

 

      589  Set(cy(imgF(z))) & Set(imgG(cy(imgF(z))))

          & ALL(a):[a e cy(imgF(z)) => g(a) e imgG(cy(imgF(z)))]

          & ALL(a):[a e imgG(cy(imgF(z))) => g'(a) e cy(imgF(z))]

            Substitute, 448, 588

 

      590  Set(cy(imgF(z))) & Set(imgG(cy(imgF(z))))

          & ALL(a):[a e cy(imgF(z)) => g(a) e imgG(cy(imgF(z)))]

          & ALL(a):[a e imgG(cy(imgF(z))) => g'(a) e cy(imgF(z))]

          & ALL(a):ALL(b):[a e cy(imgF(z)) & b e cx(z) => [g'(b)=a <=> g(a)=b]]

            Join, 589, 581

 

      591  Set(cy(imgF(z))) & Set(imgG(cy(imgF(z))))

          & ALL(a):[a e cy(imgF(z)) => g(a) e imgG(cy(imgF(z)))]

          & ALL(a):[a e imgG(cy(imgF(z))) => g'(a) e cy(imgF(z))]

          & ALL(a):ALL(b):[a e cy(imgF(z)) & b e imgG(cy(imgF(z))) => [g'(b)=a <=> g(a)=b]]

            Substitute, 448, 590

 

      592  ALL(a):ALL(b):[a e imgG(cy(imgF(z))) & b e imgG(cy(imgF(z))) => [g'(a)=g'(b) => a=b]]

          & ALL(a):[a e cy(imgF(z)) => EXIST(b):[b e imgG(cy(imgF(z))) & g'(b)=a]]

            Detach, 585, 591

 

     g' is injective

 

      593  ALL(a):ALL(b):[a e imgG(cy(imgF(z))) & b e imgG(cy(imgF(z))) => [g'(a)=g'(b) => a=b]]

            Split, 592

 

     g' is surjective

 

      594  ALL(a):[a e cy(imgF(z)) => EXIST(b):[b e imgG(cy(imgF(z))) & g'(b)=a]]

            Split, 592

 

      595  ALL(a):ALL(b):[a e cx(z) & b e cx(z) => [g'(a)=g'(b) => a=b]]

            Substitute, 448, 593

 

      596  ALL(a):[a e cy(imgF(z)) => EXIST(b):[b e cx(z) & g'(b)=a]]

            Substitute, 448, 594

 

    

     Apply Cartesian Product Axiom

 

      597  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

 

      598  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, 597

 

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

            U Spec, 598

 

      600  Set(x) & Set(y)

            Join, 12, 13

 

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

            Detach, 599, 600

 

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

            E Spec, 601

 

    

     Define: xy  (Cartesian product of x and y)

     **********

 

      603  Set'(xy)

            Split, 602

 

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

            Split, 602

 

    

     Apply Subset axiom

 

      605  EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e xy & [a e z & b=f(a) | ~a e z & b=g'(a)]]]

            Subset, 603

 

      606  Set'(k) & ALL(a):ALL(b):[(a,b) e k <=> (a,b) e xy & [a e z & b=f(a) | ~a e z & b=g'(a)]]

            E Spec, 605

 

    

     Define: k

     *********

 

      607  Set'(k)

            Split, 606

 

      608  ALL(a):ALL(b):[(a,b) e k <=> (a,b) e xy & [a e z & b=f(a) | ~a e z & b=g'(a)]]

            Split, 606

 

    

     Apply Function axiom

 

      609  ALL(f):ALL(a):ALL(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):[d=f(c) <=> (c,d) e f]]

            Function

 

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

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

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

          => ALL(c):ALL(d):[d=k(c) <=> (c,d) e k]]

            U Spec, 609

 

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

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

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

          => ALL(c):ALL(d):[d=k(c) <=> (c,d) e k]]

            U Spec, 610

 

    

     Sufficient: For functionality of k

 

      612  ALL(c):ALL(d):[(c,d) e k => c e x & d e y]

          & ALL(c):[c e x => EXIST(d):[d e y & (c,d) e k]]

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

          => ALL(c):ALL(d):[d=k(c) <=> (c,d) e k]

            U Spec, 611

 

         

          Prove: ALL(c):ALL(d):[(c,d) e k => c e x & d e y]

         

          Suppose...

 

            613  (p,q) e k

                  Premise

 

            614  ALL(b):[(p,b) e k <=> (p,b) e xy & [p e z & b=f(p) | ~p e z & b=g'(p)]]

                  U Spec, 608

 

            615  (p,q) e k <=> (p,q) e xy & [p e z & q=f(p) | ~p e z & q=g'(p)]

                  U Spec, 614

 

            616  [(p,q) e k => (p,q) e xy & [p e z & q=f(p) | ~p e z & q=g'(p)]]

              & [(p,q) e xy & [p e z & q=f(p) | ~p e z & q=g'(p)] => (p,q) e k]

                  Iff-And, 615

 

            617  (p,q) e k => (p,q) e xy & [p e z & q=f(p) | ~p e z & q=g'(p)]

                  Split, 616

 

            618  (p,q) e xy & [p e z & q=f(p) | ~p e z & q=g'(p)] => (p,q) e k

                  Split, 616

 

            619  (p,q) e xy & [p e z & q=f(p) | ~p e z & q=g'(p)]

                  Detach, 617, 613

 

            620  (p,q) e xy

                  Split, 619

 

            621  p e z & q=f(p) | ~p e z & q=g'(p)

                  Split, 619

 

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

                  U Spec, 604

 

            623  (p,q) e xy <=> p e x & q e y

                  U Spec, 622

 

            624  [(p,q) e xy => p e x & q e y]

              & [p e x & q e y => (p,q) e xy]

                  Iff-And, 623

 

            625  (p,q) e xy => p e x & q e y

                  Split, 624

 

            626  p e x & q e y => (p,q) e xy

                  Split, 624

 

            627  p e x & q e y

                  Detach, 625, 620

 

     As Required:

 

      628  ALL(c):ALL(d):[(c,d) e k => c e x & d e y]

            4 Conclusion, 613

 

         

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

         

          Suppose...

 

            629  p e x

                  Premise

 

          2 cases:

 

            630  p e z | ~p e z

                  Or Not

 

              Case 1

             

              Prove: p e z => EXIST(d):[d e y & (p,d) e k]

             

              Suppose...

 

                  631  p e z

                        Premise

 

                  632  ALL(b):[(p,b) e k <=> (p,b) e xy & [p e z & b=f(p) | ~p e z & b=g'(p)]]

                        U Spec, 608

 

                  633  (p,f(p)) e k <=> (p,f(p)) e xy & [p e z & f(p)=f(p) | ~p e z & f(p)=g'(p)]

                        U Spec, 632

 

                  634  [(p,f(p)) e k => (p,f(p)) e xy & [p e z & f(p)=f(p) | ~p e z & f(p)=g'(p)]]

                   & [(p,f(p)) e xy & [p e z & f(p)=f(p) | ~p e z & f(p)=g'(p)] => (p,f(p)) e k]

                        Iff-And, 633

 

                  635  (p,f(p)) e k => (p,f(p)) e xy & [p e z & f(p)=f(p) | ~p e z & f(p)=g'(p)]

                        Split, 634

 

                  636  (p,f(p)) e xy & [p e z & f(p)=f(p) | ~p e z & f(p)=g'(p)] => (p,f(p)) e k

                        Split, 634

 

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

                        U Spec, 604

 

                  638  (p,f(p)) e xy <=> p e x & f(p) e y

                        U Spec, 637

 

                  639  [(p,f(p)) e xy => p e x & f(p) e y]

                   & [p e x & f(p) e y => (p,f(p)) e xy]

                        Iff-And, 638

 

                  640  (p,f(p)) e xy => p e x & f(p) e y

                        Split, 639

 

                  641  p e x & f(p) e y => (p,f(p)) e xy

                        Split, 639

 

                  642  z e px <=> Set(z) & ALL(d):[d e z => d e x]

                        U Spec, 23

 

                  643  [z e px => Set(z) & ALL(d):[d e z => d e x]]

                   & [Set(z) & ALL(d):[d e z => d e x] => z e px]

                        Iff-And, 642

 

                  644  z e px => Set(z) & ALL(d):[d e z => d e x]

                        Split, 643

 

                  645  Set(z) & ALL(d):[d e z => d e x] => z e px

                        Split, 643

 

                  646  Set(z) & ALL(d):[d e z => d e x]

                        Detach, 644, 414

 

                  647  Set(z)

                        Split, 646

 

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

                        Split, 646

 

                  649  p e z => p e x

                        U Spec, 648

 

                  650  p e x

                        Detach, 649, 631

 

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

                        U Spec, 14

 

                  652  f(p) e y

                        Detach, 651, 650

 

                  653  p e x & f(p) e y

                        Join, 650, 652

 

                  654  (p,f(p)) e xy

                        Detach, 641, 653

 

                  655  f(p)=f(p)

                        Reflex

 

                  656  p e z & f(p)=f(p)

                        Join, 631, 655

 

                  657  p e z & f(p)=f(p) | ~p e z & f(p)=g'(p)

                        Arb Or, 656

 

                  658  (p,f(p)) e xy

                   & [p e z & f(p)=f(p) | ~p e z & f(p)=g'(p)]

                        Join, 654, 657

 

                  659  (p,f(p)) e k

                        Detach, 636, 658

 

                  660  f(p) e y & (p,f(p)) e k

                        Join, 652, 659

 

                  661  EXIST(d):[d e y & (p,d) e k]

                        E Gen, 660

 

          Case 1

         

          As Required:

 

            662  p e z => EXIST(d):[d e y & (p,d) e k]

                  4 Conclusion, 631

 

              Case 2

             

              Prove: ~p e z => EXIST(d):[d e y & (p,d) e k]

             

              Suppose...

 

                  663  ~p e z

                        Premise

 

                  664  ALL(b):[(p,b) e k <=> (p,b) e xy & [p e z & b=f(p) | ~p e z & b=g'(p)]]

                        U Spec, 608

 

                  665  (p,g'(p)) e k <=> (p,g'(p)) e xy & [p e z & g'(p)=f(p) | ~p e z & g'(p)=g'(p)]

                        U Spec, 664

 

                  666  [(p,g'(p)) e k => (p,g'(p)) e xy & [p e z & g'(p)=f(p) | ~p e z & g'(p)=g'(p)]]

                   & [(p,g'(p)) e xy & [p e z & g'(p)=f(p) | ~p e z & g'(p)=g'(p)] => (p,g'(p)) e k]

                        Iff-And, 665

 

                  667  (p,g'(p)) e k => (p,g'(p)) e xy & [p e z & g'(p)=f(p) | ~p e z & g'(p)=g'(p)]

                        Split, 666

 

                  668  (p,g'(p)) e xy & [p e z & g'(p)=f(p) | ~p e z & g'(p)=g'(p)] => (p,g'(p)) e k

                        Split, 666

 

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

                        U Spec, 604

 

                  670  (p,g'(p)) e xy <=> p e x & g'(p) e y

                        U Spec, 669

 

                  671  [(p,g'(p)) e xy => p e x & g'(p) e y]

                   & [p e x & g'(p) e y => (p,g'(p)) e xy]

                        Iff-And, 670

 

                  672  (p,g'(p)) e xy => p e x & g'(p) e y

                        Split, 671

 

                  673  p e x & g'(p) e y => (p,g'(p)) e xy

                        Split, 671

 

                  674  p e cx(z) => g'(p) e cy(imgF(z))

                        U Spec, 580

 

                  675  p e x => [p e cx(z) <=> ~p e z]

                        U Spec, 467

 

                  676  p e cx(z) <=> ~p e z

                        Detach, 675, 629

 

                  677  [p e cx(z) => ~p e z] & [~p e z => p e cx(z)]

                        Iff-And, 676

 

                  678  p e cx(z) => ~p e z

                        Split, 677

 

                  679  ~p e z => p e cx(z)

                        Split, 677

 

                  680  p e cx(z)

                        Detach, 679, 663

 

                  681  g'(p) e cy(imgF(z))

                        Detach, 674, 680

 

                  682  cy(imgF(z)) e py <=> Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]

                        U Spec, 28

 

                  683  [cy(imgF(z)) e py => Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]]

                   & [Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y] => cy(imgF(z)) e py]

                        Iff-And, 682

 

                  684  cy(imgF(z)) e py => Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]

                        Split, 683

 

                  685  Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y] => cy(imgF(z)) e py

                        Split, 683

 

                  686  Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]

                        Detach, 684, 461

 

                  687  Set(cy(imgF(z)))

                        Split, 686

 

                  688  ALL(d):[d e cy(imgF(z)) => d e y]

                        Split, 686

 

                  689  g'(p) e cy(imgF(z)) => g'(p) e y

                        U Spec, 688

 

                  690  g'(p) e y

                        Detach, 689, 681

 

                  691  p e x & g'(p) e y

                        Join, 629, 690

 

                  692  (p,g'(p)) e xy

                        Detach, 673, 691

 

                  693  g'(p)=g'(p)

                        Reflex

 

                  694  ~p e z & g'(p)=g'(p)

                        Join, 663, 693

 

                  695  p e z & g'(p)=f(p) | ~p e z & g'(p)=g'(p)

                        Arb Or, 694

 

                  696  (p,g'(p)) e xy

                   & [p e z & g'(p)=f(p) | ~p e z & g'(p)=g'(p)]

                        Join, 692, 695

 

                  697  (p,g'(p)) e k

                        Detach, 668, 696

 

                  698  g'(p) e y & (p,g'(p)) e k

                        Join, 690, 697

 

                  699  EXIST(d):[d e y & (p,d) e k]

                        E Gen, 698

 

          Case 2

         

          As Required:

 

            700  ~p e z => EXIST(d):[d e y & (p,d) e k]

                  4 Conclusion, 663

 

            701  [p e z => EXIST(d):[d e y & (p,d) e k]]

              & [~p e z => EXIST(d):[d e y & (p,d) e k]]

                  Join, 662, 700

 

            702  EXIST(d):[d e y & (p,d) e k]

                  Cases, 630, 701

 

     As Required:

 

      703  ALL(c):[c e x => EXIST(d):[d e y & (c,d) e k]]

            4 Conclusion, 629

 

         

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

         

          Suppose...

 

            704  (p,q1) e k & (p,q2) e k

                  Premise

 

            705  (p,q1) e k

                  Split, 704

 

            706  (p,q2) e k

                  Split, 704

 

         

          2 cases:

 

            707  p e z | ~p e z

                  Or Not

 

              Case 1

             

              Suppose...

 

                  708  p e z

                        Premise

 

                  709  ALL(b):[(p,b) e k <=> (p,b) e xy & [p e z & b=f(p) | ~p e z & b=g'(p)]]

                        U Spec, 608

 

                  710  (p,q1) e k <=> (p,q1) e xy & [p e z & q1=f(p) | ~p e z & q1=g'(p)]

                        U Spec, 709

 

                  711  [(p,q1) e k => (p,q1) e xy & [p e z & q1=f(p) | ~p e z & q1=g'(p)]]

                   & [(p,q1) e xy & [p e z & q1=f(p) | ~p e z & q1=g'(p)] => (p,q1) e k]

                        Iff-And, 710

 

                  712  (p,q1) e k => (p,q1) e xy & [p e z & q1=f(p) | ~p e z & q1=g'(p)]

                        Split, 711

 

                  713  (p,q1) e xy & [p e z & q1=f(p) | ~p e z & q1=g'(p)] => (p,q1) e k

                        Split, 711

 

                  714  (p,q1) e xy & [p e z & q1=f(p) | ~p e z & q1=g'(p)]

                        Detach, 712, 705

 

                  715  (p,q1) e xy

                        Split, 714

 

                  716  p e z & q1=f(p) | ~p e z & q1=g'(p)

                        Split, 714

 

                  717  ~[p e z & q1=f(p)] => ~p e z & q1=g'(p)

                        Imply-Or, 716

 

                  718  ~[~p e z & q1=g'(p)] => ~~[p e z & q1=f(p)]

                        Contra, 717

 

                  719  ~[~p e z & q1=g'(p)] => p e z & q1=f(p)

                        Rem DNeg, 718

 

                        720  ~p e z & q1=g'(p)

                              Premise

 

                        721  ~p e z

                              Split, 720

 

                        722  q1=g'(p)

                              Split, 720

 

                        723  p e z & ~p e z

                              Join, 708, 721

 

                  724  ~[~p e z & q1=g'(p)]

                        4 Conclusion, 720

 

                  725  p e z & q1=f(p)

                        Detach, 719, 724

 

                  726  p e z

                        Split, 725

 

                  727  q1=f(p)

                        Split, 725

 

                  728  (p,q2) e k <=> (p,q2) e xy & [p e z & q2=f(p) | ~p e z & q2=g'(p)]

                        U Spec, 709

 

                  729  [(p,q2) e k => (p,q2) e xy & [p e z & q2=f(p) | ~p e z & q2=g'(p)]]

                   & [(p,q2) e xy & [p e z & q2=f(p) | ~p e z & q2=g'(p)] => (p,q2) e k]

                        Iff-And, 728

 

                  730  (p,q2) e k => (p,q2) e xy & [p e z & q2=f(p) | ~p e z & q2=g'(p)]

                        Split, 729

 

                  731  (p,q2) e xy & [p e z & q2=f(p) | ~p e z & q2=g'(p)] => (p,q2) e k

                        Split, 729

 

                  732  (p,q2) e xy & [p e z & q2=f(p) | ~p e z & q2=g'(p)]

                        Detach, 730, 706

 

                  733  (p,q2) e xy

                        Split, 732

 

                  734  p e z & q2=f(p) | ~p e z & q2=g'(p)

                        Split, 732

 

                  735  ~[p e z & q2=f(p)] => ~p e z & q2=g'(p)

                        Imply-Or, 734

 

                  736  ~[~p e z & q2=g'(p)] => ~~[p e z & q2=f(p)]

                        Contra, 735

 

                  737  ~[~p e z & q2=g'(p)] => p e z & q2=f(p)

                        Rem DNeg, 736

 

                        738  ~p e z & q2=g'(p)

                              Premise

 

                        739  ~p e z

                              Split, 738

 

                        740  q2=g'(p)

                              Split, 738

 

                        741  p e z & ~p e z

                              Join, 708, 739

 

                  742  ~[~p e z & q2=g'(p)]

                        4 Conclusion, 738

 

                  743  p e z & q2=f(p)

                        Detach, 737, 742

 

                  744  p e z

                        Split, 743

 

                  745  q2=f(p)

                        Split, 743

 

                  746  q1=q2

                        Substitute, 745, 727

 

          Case 1

         

          As Required:

 

            747  p e z => q1=q2

                  4 Conclusion, 708

 

                  748  ~p e z

                        Premise

 

                  749  ALL(b):[(p,b) e k <=> (p,b) e xy & [p e z & b=f(p) | ~p e z & b=g'(p)]]

                        U Spec, 608

 

                  750  (p,q1) e k <=> (p,q1) e xy & [p e z & q1=f(p) | ~p e z & q1=g'(p)]

                        U Spec, 749

 

                  751  [(p,q1) e k => (p,q1) e xy & [p e z & q1=f(p) | ~p e z & q1=g'(p)]]

                   & [(p,q1) e xy & [p e z & q1=f(p) | ~p e z & q1=g'(p)] => (p,q1) e k]

                        Iff-And, 750

 

                  752  (p,q1) e k => (p,q1) e xy & [p e z & q1=f(p) | ~p e z & q1=g'(p)]

                        Split, 751

 

                  753  (p,q1) e xy & [p e z & q1=f(p) | ~p e z & q1=g'(p)] => (p,q1) e k

                        Split, 751

 

                  754  (p,q1) e xy & [p e z & q1=f(p) | ~p e z & q1=g'(p)]

                        Detach, 752, 705

 

                  755  (p,q1) e xy

                        Split, 754

 

                  756  p e z & q1=f(p) | ~p e z & q1=g'(p)

                        Split, 754

 

                  757  ~[p e z & q1=f(p)] => ~p e z & q1=g'(p)

                        Imply-Or, 756

 

                        758  p e z & q1=f(p)

                              Premise

 

                        759  p e z

                              Split, 758

 

                        760  q1=f(p)

                              Split, 758

 

                        761  p e z & ~p e z

                              Join, 759, 748

 

                  762  ~[p e z & q1=f(p)]

                        4 Conclusion, 758

 

                  763  ~p e z & q1=g'(p)

                        Detach, 757, 762

 

                  764  ~p e z

                        Split, 763

 

                  765  q1=g'(p)

                        Split, 763

 

                  766  (p,q2) e k <=> (p,q2) e xy & [p e z & q2=f(p) | ~p e z & q2=g'(p)]

                        U Spec, 749

 

                  767  [(p,q2) e k => (p,q2) e xy & [p e z & q2=f(p) | ~p e z & q2=g'(p)]]

                   & [(p,q2) e xy & [p e z & q2=f(p) | ~p e z & q2=g'(p)] => (p,q2) e k]

                        Iff-And, 766

 

                  768  (p,q2) e k => (p,q2) e xy & [p e z & q2=f(p) | ~p e z & q2=g'(p)]

                        Split, 767

 

                  769  (p,q2) e xy & [p e z & q2=f(p) | ~p e z & q2=g'(p)] => (p,q2) e k

                        Split, 767

 

                  770  (p,q2) e xy & [p e z & q2=f(p) | ~p e z & q2=g'(p)]

                        Detach, 768, 706

 

                  771  (p,q2) e xy

                        Split, 770

 

                  772  p e z & q2=f(p) | ~p e z & q2=g'(p)

                        Split, 770

 

                  773  ~[p e z & q2=f(p)] => ~p e z & q2=g'(p)

                        Imply-Or, 772

 

                        774  p e z & q2=f(p)

                              Premise

 

                        775  p e z

                              Split, 774

 

                        776  q2=f(p)

                              Split, 774

 

                        777  p e z & ~p e z

                              Join, 775, 748

 

                  778  ~[p e z & q2=f(p)]

                        4 Conclusion, 774

 

                  779  ~p e z & q2=g'(p)

                        Detach, 773, 778

 

                  780  ~p e z

                        Split, 779

 

                  781  q2=g'(p)

                        Split, 779

 

                  782  q1=q2

                        Substitute, 781, 765

 

          As Required:

 

            783  ~p e z => q1=q2

                  4 Conclusion, 748

 

            784  [p e z => q1=q2] & [~p e z => q1=q2]

                  Join, 747, 783

 

            785  q1=q2

                  Cases, 707, 784

 

     As Required:

 

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

            4 Conclusion, 704

 

      787  ALL(c):ALL(d):[(c,d) e k => c e x & d e y]

          & ALL(c):[c e x => EXIST(d):[d e y & (c,d) e k]]

            Join, 628, 703

 

      788  ALL(c):ALL(d):[(c,d) e k => c e x & d e y]

          & ALL(c):[c e x => EXIST(d):[d e y & (c,d) e k]]

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

            Join, 787, 786

 

    

     As Required: k is a function

 

      789  ALL(c):ALL(d):[d=k(c) <=> (c,d) e k]

            Detach, 612, 788

 

         

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

         

          Suppose...

 

            790  p e x

                  Premise

 

            791  p e x => EXIST(d):[d e y & (p,d) e k]

                  U Spec, 703

 

            792  EXIST(d):[d e y & (p,d) e k]

                  Detach, 791, 790

 

            793  q e y & (p,q) e k

                  E Spec, 792

 

            794  q e y

                  Split, 793

 

            795  (p,q) e k

                  Split, 793

 

            796  ALL(d):[d=k(p) <=> (p,d) e k]

                  U Spec, 789

 

            797  q=k(p) <=> (p,q) e k

                  U Spec, 796

 

            798  [q=k(p) => (p,q) e k] & [(p,q) e k => q=k(p)]

                  Iff-And, 797

 

            799  q=k(p) => (p,q) e k

                  Split, 798

 

            800  (p,q) e k => q=k(p)

                  Split, 798

 

            801  q=k(p)

                  Detach, 800, 795

 

            802  k(p) e y

                  Substitute, 801, 794

 

     As Required:

 

      803  ALL(a):[a e x => k(a) e y]

            4 Conclusion, 790

 

         

          Prove: ALL(a):[a e x

                 => [a e z => k(a)=f(a)] & [~a e z => k(a)=g'(a)]]

         

          Suppose...

 

            804  p e x

                  Premise

 

             

              Prove: p e z => k(p)=f(p)

             

              Suppose...

 

                  805  p e z

                        Premise

 

                  806  ALL(b):[(p,b) e k <=> (p,b) e xy & [p e z & b=f(p) | ~p e z & b=g'(p)]]

                        U Spec, 608

 

                  807  (p,f(p)) e k <=> (p,f(p)) e xy & [p e z & f(p)=f(p) | ~p e z & f(p)=g'(p)]

                        U Spec, 806

 

                  808  [(p,f(p)) e k => (p,f(p)) e xy & [p e z & f(p)=f(p) | ~p e z & f(p)=g'(p)]]

                   & [(p,f(p)) e xy & [p e z & f(p)=f(p) | ~p e z & f(p)=g'(p)] => (p,f(p)) e k]

                        Iff-And, 807

 

                  809  (p,f(p)) e k => (p,f(p)) e xy & [p e z & f(p)=f(p) | ~p e z & f(p)=g'(p)]

                        Split, 808

 

                  810  (p,f(p)) e xy & [p e z & f(p)=f(p) | ~p e z & f(p)=g'(p)] => (p,f(p)) e k

                        Split, 808

 

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

                        U Spec, 604

 

                  812  (p,f(p)) e xy <=> p e x & f(p) e y

                        U Spec, 811

 

                  813  [(p,f(p)) e xy => p e x & f(p) e y]

                   & [p e x & f(p) e y => (p,f(p)) e xy]

                        Iff-And, 812

 

                  814  (p,f(p)) e xy => p e x & f(p) e y

                        Split, 813

 

                  815  p e x & f(p) e y => (p,f(p)) e xy

                        Split, 813

 

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

                        U Spec, 14

 

                  817  f(p) e y

                        Detach, 816, 804

 

                  818  p e x & f(p) e y

                        Join, 804, 817

 

                  819  (p,f(p)) e xy

                        Detach, 815, 818

 

                  820  (p,f(p)) e xy

                        Detach, 815, 818

 

                  821  f(p)=f(p)

                        Reflex

 

                  822  p e z & f(p)=f(p)

                        Join, 805, 821

 

                  823  p e z & f(p)=f(p) | ~p e z & f(p)=g'(p)

                        Arb Or, 822

 

                  824  (p,f(p)) e xy

                   & [p e z & f(p)=f(p) | ~p e z & f(p)=g'(p)]

                        Join, 820, 823

 

                  825  (p,f(p)) e k

                        Detach, 810, 824

 

                  826  ALL(d):[d=k(p) <=> (p,d) e k]

                        U Spec, 789

 

                  827  f(p)=k(p) <=> (p,f(p)) e k

                        U Spec, 826

 

                  828  [f(p)=k(p) => (p,f(p)) e k]

                   & [(p,f(p)) e k => f(p)=k(p)]

                        Iff-And, 827

 

                  829  f(p)=k(p) => (p,f(p)) e k

                        Split, 828

 

                  830  (p,f(p)) e k => f(p)=k(p)

                        Split, 828

 

                  831  f(p)=k(p)

                        Detach, 830, 825

 

                  832  k(p)=f(p)

                        Sym, 831

 

          As Required:

 

            833  p e z => k(p)=f(p)

                  4 Conclusion, 805

 

             

              Prove: ~p e z => k(p)=g'(p)

             

              Suppose...

 

                  834  ~p e z

                        Premise

 

                  835  ALL(b):[(p,b) e k <=> (p,b) e xy & [p e z & b=f(p) | ~p e z & b=g'(p)]]

                        U Spec, 608

 

                  836  (p,g'(p)) e k <=> (p,g'(p)) e xy & [p e z & g'(p)=f(p) | ~p e z & g'(p)=g'(p)]

                        U Spec, 835

 

                  837  [(p,g'(p)) e k => (p,g'(p)) e xy & [p e z & g'(p)=f(p) | ~p e z & g'(p)=g'(p)]]

                   & [(p,g'(p)) e xy & [p e z & g'(p)=f(p) | ~p e z & g'(p)=g'(p)] => (p,g'(p)) e k]

                        Iff-And, 836

 

                  838  (p,g'(p)) e k => (p,g'(p)) e xy & [p e z & g'(p)=f(p) | ~p e z & g'(p)=g'(p)]

                        Split, 837

 

                  839  (p,g'(p)) e xy & [p e z & g'(p)=f(p) | ~p e z & g'(p)=g'(p)] => (p,g'(p)) e k

                        Split, 837

 

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

                        U Spec, 604

 

                  841  (p,g'(p)) e xy <=> p e x & g'(p) e y

                        U Spec, 840

 

                  842  [(p,g'(p)) e xy => p e x & g'(p) e y]

                   & [p e x & g'(p) e y => (p,g'(p)) e xy]

                        Iff-And, 841

 

                  843  (p,g'(p)) e xy => p e x & g'(p) e y

                        Split, 842

 

                  844  p e x & g'(p) e y => (p,g'(p)) e xy

                        Split, 842

 

                  845  p e cx(z) => g'(p) e cy(imgF(z))

                        U Spec, 580

 

                  846  p e x => [p e cx(z) <=> ~p e z]

                        U Spec, 467

 

                  847  p e cx(z) <=> ~p e z

                        Detach, 846, 804

 

                  848  [p e cx(z) => ~p e z] & [~p e z => p e cx(z)]

                        Iff-And, 847

 

                  849  p e cx(z) => ~p e z

                        Split, 848

 

                  850  ~p e z => p e cx(z)

                        Split, 848

 

                  851  p e cx(z)

                        Detach, 850, 834

 

                  852  g'(p) e cy(imgF(z))

                        Detach, 845, 851

 

                  853  cy(imgF(z)) e py <=> Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]

                        U Spec, 28

 

                  854  [cy(imgF(z)) e py => Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]]

                   & [Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y] => cy(imgF(z)) e py]

                        Iff-And, 853

 

                  855  cy(imgF(z)) e py => Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]

                        Split, 854

 

                  856  Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y] => cy(imgF(z)) e py

                        Split, 854

 

                  857  Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]

                        Detach, 855, 461

 

                  858  Set(cy(imgF(z)))

                        Split, 857

 

                  859  ALL(d):[d e cy(imgF(z)) => d e y]

                        Split, 857

 

                  860  g'(p) e cy(imgF(z)) => g'(p) e y

                        U Spec, 859

 

                  861  g'(p) e y

                        Detach, 860, 852

 

                  862  p e x & g'(p) e y

                        Join, 804, 861

 

                  863  (p,g'(p)) e xy

                        Detach, 844, 862

 

                  864  g'(p)=g'(p)

                        Reflex

 

                  865  ~p e z & g'(p)=g'(p)

                        Join, 834, 864

 

                  866  p e z & g'(p)=f(p) | ~p e z & g'(p)=g'(p)

                        Arb Or, 865

 

                  867  (p,g'(p)) e xy

                   & [p e z & g'(p)=f(p) | ~p e z & g'(p)=g'(p)]

                        Join, 863, 866

 

                  868  (p,g'(p)) e k

                        Detach, 839, 867

 

                  869  ALL(d):[d=k(p) <=> (p,d) e k]

                        U Spec, 789

 

                  870  g'(p)=k(p) <=> (p,g'(p)) e k

                        U Spec, 869

 

                  871  [g'(p)=k(p) => (p,g'(p)) e k]

                   & [(p,g'(p)) e k => g'(p)=k(p)]

                        Iff-And, 870

 

                  872  g'(p)=k(p) => (p,g'(p)) e k

                        Split, 871

 

                  873  (p,g'(p)) e k => g'(p)=k(p)

                        Split, 871

 

                  874  g'(p)=k(p)

                        Detach, 873, 868

 

                  875  k(p)=g'(p)

                        Sym, 874

 

          As Required:

 

            876  ~p e z => k(p)=g'(p)

                  4 Conclusion, 834

 

            877  [p e z => k(p)=f(p)] & [~p e z => k(p)=g'(p)]

                  Join, 833, 876

 

     As Required:

 

      878  ALL(a):[a e x

          => [a e z => k(a)=f(a)] & [~a e z => k(a)=g'(a)]]

            4 Conclusion, 804

 

    

     Apply definition of Injection

 

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

            U Spec, 2

 

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

            U Spec, 879

 

      881  Injection(f,x,y) <=> ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]

            U Spec, 880

 

      882  [Injection(f,x,y) => ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]]

          & [ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]] => Injection(f,x,y)]

            Iff-And, 881

 

      883  Injection(f,x,y) => ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]

            Split, 882

 

      884  ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]] => Injection(f,x,y)

            Split, 882

 

     f is an injection on x

 

      885  ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]

            Detach, 883, 16

 

     Apply definition of Subset

 

      886  ALL(b):[Subset(z,b) <=> ALL(c):[c e z => c e b]]

            U Spec, 1

 

      887  Subset(z,x) <=> ALL(c):[c e z => c e x]

            U Spec, 886

 

      888  [Subset(z,x) => ALL(c):[c e z => c e x]]

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

            Iff-And, 887

 

      889  Subset(z,x) => ALL(c):[c e z => c e x]

            Split, 888

 

      890  ALL(c):[c e z => c e x] => Subset(z,x)

            Split, 888

 

     z is a subset of x

 

      891  ALL(c):[c e z => c e x]

            Detach, 889, 400

 

         

          Prove: ALL(a):ALL(b):[a e x & b e x => [k(a)=k(b) => a=b]]  (i.e. k is injective)

         

          Suppose...

 

            892  p e x & q e x

                  Premise

 

            893  p e x

                  Split, 892

 

            894  q e x

                  Split, 892

 

            895  p e x

              => [p e z => k(p)=f(p)] & [~p e z => k(p)=g'(p)]

                  U Spec, 878

 

            896  [p e z => k(p)=f(p)] & [~p e z => k(p)=g'(p)]

                  Detach, 895, 893

 

            897  p e z => k(p)=f(p)

                  Split, 896

 

            898  ~p e z => k(p)=g'(p)

                  Split, 896

 

            899  q e x

              => [q e z => k(q)=f(q)] & [~q e z => k(q)=g'(q)]

                  U Spec, 878

 

            900  [q e z => k(q)=f(q)] & [~q e z => k(q)=g'(q)]

                  Detach, 899, 894

 

            901  q e z => k(q)=f(q)

                  Split, 900

 

            902  ~q e z => k(q)=g'(q)

                  Split, 900

 

          2 cases:

 

            903  p e z | ~p e z

                  Or Not

 

          2 sub-cases:

 

            904  q e z | ~q e z

                  Or Not

 

             

              Prove: k(p)=k(q) => p=q

             

              Suppose...

 

                  905  k(p)=k(q)

                        Premise

 

                   Case 1

                  

                   Suppose...

 

                        906  p e z

                              Premise

 

                        907  k(p)=f(p)

                              Detach, 897, 906

 

                        908  f(p)=k(q)

                              Substitute, 907, 905

 

                        Sub-case 1

                       

                        Suppose...

 

                              909  q e z

                                    Premise

 

                              910  k(q)=f(q)

                                    Detach, 901, 909

 

                              911  f(p)=f(q)

                                    Substitute, 910, 908

 

                              912  ALL(d):[p e x & d e x => [f(p)=f(d) => p=d]]

                                    U Spec, 885

 

                              913  q e x

                             => [q e z => k(q)=f(q)] & [~q e z => k(q)=g'(q)]

                                    U Spec, 878

 

                              914  [q e z => k(q)=f(q)] & [~q e z => k(q)=g'(q)]

                                    Detach, 913, 894

 

                              915  q e z => k(q)=f(q)

                                    Split, 914

 

                              916  ~q e z => k(q)=g'(q)

                                    Split, 914

 

                              917  k(q)=f(q)

                                    Detach, 915, 909

 

                              918  f(p)=f(q)

                                    Substitute, 917, 908

 

                              919  p e x & q e x => [f(p)=f(q) => p=q]

                                    U Spec, 912

 

                              920  p e z => p e x

                                    U Spec, 891

 

                              921  p e x

                                    Detach, 920, 906

 

                              922  q e z => q e x

                                    U Spec, 891

 

                              923  q e x

                                    Detach, 922, 909

 

                              924  p e x & q e x

                                    Join, 921, 923

 

                              925  f(p)=f(q) => p=q

                                    Detach, 919, 924

 

                              926  p=q

                                    Detach, 925, 918

 

                   Sub-case 1

                  

                   As Required:

 

                        927  q e z => p=q

                              4 Conclusion, 909

 

                        Sub-case 2

                       

                        Suppose...

 

                              928  ~q e z

                                    Premise

 

                              929  k(q)=g'(q)

                                    Detach, 902, 928

 

                              930  q e cx(z) => g'(q) e cy(imgF(z))

                                    U Spec, 580

 

                              931  q e x => [q e cx(z) <=> ~q e z]

                                    U Spec, 467

 

                              932  q e cx(z) <=> ~q e z

                                    Detach, 931, 894

 

                              933  [q e cx(z) => ~q e z] & [~q e z => q e cx(z)]

                                    Iff-And, 932

 

                              934  q e cx(z) => ~q e z

                                    Split, 933

 

                              935  ~q e z => q e cx(z)

                                    Split, 933

 

                              936  q e cx(z)

                                    Detach, 935, 928

 

                              937  g'(q) e cy(imgF(z))

                                    Detach, 930, 936

 

                              938  k(q) e cy(imgF(z))

                                    Substitute, 929, 937

 

                              939  z e px

                             => ALL(c):[c e imgF(z) <=> EXIST(d):[d e z & f(d)=c]]

                                    U Spec, 51

 

                              940  ALL(c):[c e imgF(z) <=> EXIST(d):[d e z & f(d)=c]]

                                    Detach, 939, 414

 

                              941  k(p) e imgF(z) <=> EXIST(d):[d e z & f(d)=k(p)]

                                    U Spec, 940

 

                              942  [k(p) e imgF(z) => EXIST(d):[d e z & f(d)=k(p)]]

                             & [EXIST(d):[d e z & f(d)=k(p)] => k(p) e imgF(z)]

                                    Iff-And, 941

 

                              943  k(p) e imgF(z) => EXIST(d):[d e z & f(d)=k(p)]

                                    Split, 942

 

                              944  EXIST(d):[d e z & f(d)=k(p)] => k(p) e imgF(z)

                                    Split, 942

 

                              945  f(p)=k(p)

                                    Sym, 907

 

                              946  p e z & f(p)=k(p)

                                    Join, 906, 945

 

                              947  EXIST(d):[d e z & f(d)=k(p)]

                                    E Gen, 946

 

                              948  k(p) e imgF(z)

                                    Detach, 944, 947

 

                              949  k(p) e cy(imgF(z))

                                    Substitute, 905, 938

 

                              950  k(p) e y => [k(p) e cy(imgF(z)) <=> ~k(p) e imgF(z)]

                                    U Spec, 463

 

                              951  p e x => k(p) e y

                                    U Spec, 803

 

                              952  k(p) e y

                                    Detach, 951, 893

 

                              953  k(p) e cy(imgF(z)) <=> ~k(p) e imgF(z)

                                    Detach, 950, 952

 

                              954  [k(p) e cy(imgF(z)) => ~k(p) e imgF(z)]

                             & [~k(p) e imgF(z) => k(p) e cy(imgF(z))]

                                    Iff-And, 953

 

                              955  k(p) e cy(imgF(z)) => ~k(p) e imgF(z)

                                    Split, 954

 

                              956  ~k(p) e imgF(z) => k(p) e cy(imgF(z))

                                    Split, 954

 

                              957  ~k(p) e imgF(z)

                                    Detach, 955, 949

 

                              958  ~~k(p) e imgF(z) => p=q

                                    Arb Cons, 957

 

                              959  k(p) e imgF(z) => p=q

                                    Rem DNeg, 958

 

                              960  p=q

                                    Detach, 959, 948

 

                   Sub-case 2

                  

                   As Required:

 

                        961  ~q e z => p=q

                              4 Conclusion, 928

 

                        962  [q e z => p=q] & [~q e z => p=q]

                              Join, 927, 961

 

                        963  p=q

                              Cases, 904, 962

 

              Case 1

             

              As Required:

 

                  964  p e z => p=q

                        4 Conclusion, 906

 

                   Case 2

                  

                   Prove: ~p e z => p=q

                  

                   Suppose...

 

                        965  ~p e z

                              Premise

 

                        966  k(p)=g'(p)

                              Detach, 898, 965

 

                        Sub-case 1

                       

                        Prove: q e z => p=q

                       

                        Suppose...

 

                              967  q e z

                                    Premise

 

                              968  k(q)=f(q)

                                    Detach, 901, 967

 

                              969  p e cx(z) => g'(p) e cy(imgF(z))

                                    U Spec, 580

 

                              970  p e x => [p e cx(z) <=> ~p e z]

                                    U Spec, 467

 

                              971  p e cx(z) <=> ~p e z

                                    Detach, 970, 893

 

                              972  [p e cx(z) => ~p e z] & [~p e z => p e cx(z)]

                                    Iff-And, 971

 

                              973  p e cx(z) => ~p e z

                                    Split, 972

 

                              974  ~p e z => p e cx(z)

                                    Split, 972

 

                              975  p e cx(z)

                                    Detach, 974, 965

 

                              976  g'(p) e cy(imgF(z))

                                    Detach, 969, 975

 

                              977  k(p) e cy(imgF(z))

                                    Substitute, 966, 976

 

                              978  q e imgF(z) <=> EXIST(d):[d e z & f(d)=q]

                                    U Spec, 459

 

                              979  f(q) e imgF(z) <=> EXIST(d):[d e z & f(d)=f(q)]

                                    U Spec, 459

 

                              980  [f(q) e imgF(z) => EXIST(d):[d e z & f(d)=f(q)]]

                             & [EXIST(d):[d e z & f(d)=f(q)] => f(q) e imgF(z)]

                                    Iff-And, 979

 

                              981  f(q) e imgF(z) => EXIST(d):[d e z & f(d)=f(q)]

                                    Split, 980

 

                              982  EXIST(d):[d e z & f(d)=f(q)] => f(q) e imgF(z)

                                    Split, 980

 

                              983  f(q)=f(q)

                                    Reflex

 

                              984  q e z & f(q)=f(q)

                                    Join, 967, 983

 

                              985  EXIST(d):[d e z & f(d)=f(q)]

                                    E Gen, 984

 

                              986  f(q) e imgF(z)

                                    Detach, 982, 985

 

                              987  k(q) e imgF(z)

                                    Substitute, 968, 986

 

                              988  k(q) e y => [k(q) e cy(imgF(z)) <=> ~k(q) e imgF(z)]

                                    U Spec, 463

 

                              989  q e x => k(q) e y

                                    U Spec, 803

 

                              990  k(q) e y

                                    Detach, 989, 894

 

                              991  k(q) e cy(imgF(z)) <=> ~k(q) e imgF(z)

                                    Detach, 988, 990

 

                              992  [k(q) e cy(imgF(z)) => ~k(q) e imgF(z)]

                             & [~k(q) e imgF(z) => k(q) e cy(imgF(z))]

                                    Iff-And, 991

 

                              993  k(q) e cy(imgF(z)) => ~k(q) e imgF(z)

                                    Split, 992

 

                              994  ~k(q) e imgF(z) => k(q) e cy(imgF(z))

                                    Split, 992

 

                              995  k(q) e cy(imgF(z))

                                    Substitute, 905, 977

 

                              996  ~k(q) e imgF(z)

                                    Detach, 993, 995

 

                              997  ~~k(q) e imgF(z) => p=q

                                    Arb Cons, 996

 

                              998  k(q) e imgF(z) => p=q

                                    Rem DNeg, 997

 

                              999  p=q

                                    Detach, 998, 987

 

                   Sub-case 1

                  

                   As Required:

 

                        1000 q e z => p=q

                              4 Conclusion, 967

 

                        Sub-case 2

                       

                        Prove: ~q e z => p=q

                       

                        Suppose...

 

                              1001 ~q e z

                                    Premise

 

                              1002 k(q)=g'(q)

                                    Detach, 902, 1001

 

                              1003 g'(p)=k(q)

                                    Substitute, 966, 905

 

                              1004 g'(p)=g'(q)

                                    Substitute, 1002, 1003

 

                              1005 ALL(b):[p e cx(z) & b e cx(z) => [g'(p)=g'(b) => p=b]]

                                    U Spec, 595

 

                              1006 p e cx(z) & q e cx(z) => [g'(p)=g'(q) => p=q]

                                    U Spec, 1005

 

                              1007 p e x => [p e cx(z) <=> ~p e z]

                                    U Spec, 467

 

                              1008 p e cx(z) <=> ~p e z

                                    Detach, 1007, 893

 

                              1009 [p e cx(z) => ~p e z] & [~p e z => p e cx(z)]

                                    Iff-And, 1008

 

                              1010 p e cx(z) => ~p e z

                                    Split, 1009

 

                              1011 ~p e z => p e cx(z)

                                    Split, 1009

 

                              1012 p e cx(z)

                                    Detach, 1011, 965

 

                              1013 q e x => [q e cx(z) <=> ~q e z]

                                    U Spec, 467

 

                              1014 q e cx(z) <=> ~q e z

                                    Detach, 1013, 894

 

                              1015 [q e cx(z) => ~q e z] & [~q e z => q e cx(z)]

                                    Iff-And, 1014

 

                              1016 q e cx(z) => ~q e z

                                    Split, 1015

 

                              1017 ~q e z => q e cx(z)

                                    Split, 1015

 

                              1018 q e cx(z)

                                    Detach, 1017, 1001

 

                              1019 p e cx(z) & q e cx(z)

                                    Join, 1012, 1018

 

                              1020 g'(p)=g'(q) => p=q

                                    Detach, 1006, 1019

 

                              1021 p=q

                                    Detach, 1020, 1004

 

                   Sub-case 2

                  

                   As Required:

 

                        1022 ~q e z => p=q

                              4 Conclusion, 1001

 

                        1023 [q e z => p=q] & [~q e z => p=q]

                              Join, 1000, 1022

 

                        1024 p=q

                              Cases, 904, 1023

 

              Case 2

             

              As Required:

 

                  1025 ~p e z => p=q

                        4 Conclusion, 965

 

                  1026 [p e z => p=q] & [~p e z => p=q]

                        Join, 964, 1025

 

                  1027 p=q

                        Cases, 903, 1026

 

          As Required:

 

            1028 k(p)=k(q) => p=q

                  4 Conclusion, 905

 

    

     k is injective

 

      1029 ALL(a):ALL(b):[a e x & b e x => [k(a)=k(b) => a=b]]

            4 Conclusion, 892

 

            1030 p e imgF(z)

                  Premise

 

            1031 z e px

              => ALL(c):[c e imgF(z) <=> EXIST(d):[d e z & f(d)=c]]

                  U Spec, 51

 

            1032 ALL(c):[c e imgF(z) <=> EXIST(d):[d e z & f(d)=c]]

                  Detach, 1031, 414

 

            1033 p e imgF(z) <=> EXIST(d):[d e z & f(d)=p]

                  U Spec, 1032

 

            1034 [p e imgF(z) => EXIST(d):[d e z & f(d)=p]]

              & [EXIST(d):[d e z & f(d)=p] => p e imgF(z)]

                  Iff-And, 1033

 

            1035 p e imgF(z) => EXIST(d):[d e z & f(d)=p]

                  Split, 1034

 

            1036 EXIST(d):[d e z & f(d)=p] => p e imgF(z)

                  Split, 1034

 

            1037 EXIST(d):[d e z & f(d)=p]

                  Detach, 1035, 1030

 

    

     f: z -> imgF(z) is surjective

 

      1038 ALL(a):[a e imgF(z) => EXIST(d):[d e z & f(d)=a]]

            4 Conclusion, 1030

 

      1039 Set(z) & Set(imgF(z))

          & ALL(a):[a e z => f(a) e imgF(z)]

          & ALL(a):[a e imgF(z) => EXIST(d):[d e z & f(d)=a]]

            Join, 511, 1038

 

      1040 Set(z) & Set(imgF(z))

          & ALL(a):[a e z => f(a) e imgF(z)]

          & ALL(a):[a e imgF(z) => EXIST(d):[d e z & f(d)=a]]

          & ALL(a):ALL(b):[a e z & b e z => [f(a)=f(b) => a=b]]

            Join, 1039, 506

 

      1041 EXIST(f'):[ALL(a):[a e imgF(z) => f'(a) e z]

          & ALL(a):ALL(b):[a e z & b e imgF(z) => [f'(b)=a <=> f(a)=b]]]

            Detach, 509, 1040

 

      1042 ALL(a):[a e imgF(z) => f'(a) e z]

          & ALL(a):ALL(b):[a e z & b e imgF(z) => [f'(b)=a <=> f(a)=b]]

            E Spec, 1041

 

    

     Define: f'   (inverse of f: z -> imgF(z))

     **********

 

      1043 ALL(a):[a e imgF(z) => f'(a) e z]

            Split, 1042

 

      1044 ALL(a):ALL(b):[a e z & b e imgF(z) => [f'(b)=a <=> f(a)=b]]

            Split, 1042

 

         

          Prove: ALL(a):[aecx(z) => f(a)ecy(imgF(z))]  i.e. f: cx(z) -> cy(imgF(z) is well-defined

           

          Suppose...

 

            1045 p e cx(z)

                  Premise

 

            1046 f(p) e y => [f(p) e cy(imgF(z)) <=> ~f(p) e imgF(z)]

                  U Spec, 463

 

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

                  U Spec, 14

 

            1048 cx(z) e px <=> Set(cx(z)) & ALL(d):[d e cx(z) => d e x]

                  U Spec, 23

 

            1049 [cx(z) e px => Set(cx(z)) & ALL(d):[d e cx(z) => d e x]]

              & [Set(cx(z)) & ALL(d):[d e cx(z) => d e x] => cx(z) e px]

                  Iff-And, 1048

 

            1050 cx(z) e px => Set(cx(z)) & ALL(d):[d e cx(z) => d e x]

                  Split, 1049

 

            1051 Set(cx(z)) & ALL(d):[d e cx(z) => d e x] => cx(z) e px

                  Split, 1049

 

            1052 Set(cx(z)) & ALL(d):[d e cx(z) => d e x]

                  Detach, 1050, 465

 

            1053 Set(cx(z))

                  Split, 1052

 

            1054 ALL(d):[d e cx(z) => d e x]

                  Split, 1052

 

            1055 p e cx(z) => p e x

                  U Spec, 1054

 

            1056 p e x

                  Detach, 1055, 1045

 

            1057 f(p) e y

                  Detach, 1047, 1056

 

            1058 f(p) e cy(imgF(z)) <=> ~f(p) e imgF(z)

                  Detach, 1046, 1057

 

            1059 [f(p) e cy(imgF(z)) => ~f(p) e imgF(z)]

              & [~f(p) e imgF(z) => f(p) e cy(imgF(z))]

                  Iff-And, 1058

 

            1060 f(p) e cy(imgF(z)) => ~f(p) e imgF(z)

                  Split, 1059

 

          Sufficient:

 

            1061 ~f(p) e imgF(z) => f(p) e cy(imgF(z))

                  Split, 1059

 

             

              Prove: ~f(p) e imgF(z)

             

              Suppose to the contrary...

 

                  1062 f(p) e imgF(z)

                        Premise

 

                  1063 f(p) e imgF(z) <=> EXIST(d):[d e z & f(d)=f(p)]

                        U Spec, 459

 

                  1064 [f(p) e imgF(z) => EXIST(d):[d e z & f(d)=f(p)]]

                   & [EXIST(d):[d e z & f(d)=f(p)] => f(p) e imgF(z)]

                        Iff-And, 1063

 

                  1065 f(p) e imgF(z) => EXIST(d):[d e z & f(d)=f(p)]

                        Split, 1064

 

                  1066 EXIST(d):[d e z & f(d)=f(p)] => f(p) e imgF(z)

                        Split, 1064

 

                  1067 EXIST(d):[d e z & f(d)=f(p)]

                        Detach, 1065, 1062

 

                  1068 q e z & f(q)=f(p)

                        E Spec, 1067

 

                  1069 q e z

                        Split, 1068

 

                  1070 f(q)=f(p)

                        Split, 1068

 

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

                        U Spec, 2

 

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

                        U Spec, 1071

 

                  1073 Injection(f,x,y) <=> ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]

                        U Spec, 1072

 

                  1074 [Injection(f,x,y) => ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]]

                   & [ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]] => Injection(f,x,y)]

                        Iff-And, 1073

 

                  1075 Injection(f,x,y) => ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]

                        Split, 1074

 

                  1076 ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]] => Injection(f,x,y)

                        Split, 1074

 

                  1077 ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]

                        Detach, 1075, 16

 

                  1078 ALL(d):[p e x & d e x => [f(p)=f(d) => p=d]]

                        U Spec, 1077

 

                  1079 p e x & q e x => [f(p)=f(q) => p=q]

                        U Spec, 1078

 

                  1080 z e px <=> Set(z) & ALL(d):[d e z => d e x]

                        U Spec, 23

 

                  1081 [z e px => Set(z) & ALL(d):[d e z => d e x]]

                   & [Set(z) & ALL(d):[d e z => d e x] => z e px]

                        Iff-And, 1080

 

                  1082 z e px => Set(z) & ALL(d):[d e z => d e x]

                        Split, 1081

 

                  1083 Set(z) & ALL(d):[d e z => d e x] => z e px

                        Split, 1081

 

                  1084 Set(z) & ALL(d):[d e z => d e x]

                        Detach, 1082, 414

 

                  1085 Set(z)

                        Split, 1084

 

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

                        Split, 1084

 

                  1087 q e z => q e x

                        U Spec, 1086

 

                  1088 q e x

                        Detach, 1087, 1069

 

                  1089 p e x & q e x

                        Join, 1056, 1088

 

                  1090 f(p)=f(q) => p=q

                        Detach, 1079, 1089

 

                  1091 f(p)=f(q)

                        Sym, 1070

 

                  1092 p=q

                        Detach, 1090, 1091

 

                  1093 p e x => [p e cx(z) <=> ~p e z]

                        U Spec, 467

 

                  1094 p e cx(z) <=> ~p e z

                        Detach, 1093, 1056

 

                  1095 [p e cx(z) => ~p e z] & [~p e z => p e cx(z)]

                        Iff-And, 1094

 

                  1096 p e cx(z) => ~p e z

                        Split, 1095

 

                  1097 ~p e z => p e cx(z)

                        Split, 1095

 

                  1098 ~p e z

                        Detach, 1096, 1045

 

                  1099 ~q e z

                        Substitute, 1092, 1098

 

                  1100 q e z & ~q e z

                        Join, 1069, 1099

 

          As Required:

 

            1101 ~f(p) e imgF(z)

                  4 Conclusion, 1062

 

            1102 f(p) e cy(imgF(z))

                  Detach, 1061, 1101

 

    

     Define: f: cx(z) -> cy(imgF(z))  (a restriction on f: x -> y)

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

 

      1103 ALL(a):[a e cx(z) => f(a) e cy(imgF(z))]

            4 Conclusion, 1045

 

         

          Suppose...

 

            1104 p e cx(z)

                  Premise

 

            1105 p e cx(z) => f(p) e cy(imgF(z))

                  U Spec, 1103

 

            1106 f(p) e cy(imgF(z))

                  Detach, 1105, 1104

 

            1107 f(p) e y => [f(p) e cy(imgF(z)) <=> ~f(p) e imgF(z)]

                  U Spec, 463

 

            1108 cy(imgF(z)) e py <=> Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]

                  U Spec, 28

 

            1109 [cy(imgF(z)) e py => Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]]

              & [Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y] => cy(imgF(z)) e py]

                  Iff-And, 1108

 

            1110 cy(imgF(z)) e py => Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]

                  Split, 1109

 

            1111 Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y] => cy(imgF(z)) e py

                  Split, 1109

 

            1112 Set(cy(imgF(z))) & ALL(d):[d e cy(imgF(z)) => d e y]

                  Detach, 1110, 461

 

            1113 Set(cy(imgF(z)))

                  Split, 1112

 

            1114 ALL(d):[d e cy(imgF(z)) => d e y]

                  Split, 1112

 

            1115 f(p) e cy(imgF(z)) => f(p) e y

                  U Spec, 1114

 

            1116 f(p) e y

                  Detach, 1115, 1106

 

            1117 f(p) e cy(imgF(z)) <=> ~f(p) e imgF(z)

                  Detach, 1107, 1116

 

            1118 [f(p) e cy(imgF(z)) => ~f(p) e imgF(z)]

              & [~f(p) e imgF(z) => f(p) e cy(imgF(z))]

                  Iff-And, 1117

 

            1119 f(p) e cy(imgF(z)) => ~f(p) e imgF(z)

                  Split, 1118

 

            1120 ~f(p) e imgF(z) => f(p) e cy(imgF(z))

                  Split, 1118

 

            1121 ~f(p) e imgF(z)

                  Detach, 1119, 1106

 

     As Required:

 

      1122 ALL(a):[a e cx(z) => ~f(a) e imgF(z)]

            4 Conclusion, 1104

 

      1123 ALL(a):[~~f(a) e imgF(z) => ~a e cx(z)]

            Contra, 1122

 

     As Required:

 

      1124 ALL(a):[f(a) e imgF(z) => ~a e cx(z)]

            Rem DNeg, 1123

 

         

          Prove: ALL(a):[a e y => EXIST(b):[b e x & k(b)=a]]  i.e. k is surjective

         

          Suppose...

 

            1125 p e y

                  Premise

 

          2 cases:

 

            1126 p e imgF(z) | ~p e imgF(z)

                  Or Not

 

              Case 1

             

              Prove: p e imgF(z) => EXIST(b):[b e x & p=k(b)]

             

              Suppose...

 

                  1127 p e imgF(z)

                        Premise

 

                  1128 ALL(b):[(f'(p),b) e k <=> (f'(p),b) e xy & [f'(p) e z & b=f(f'(p)) | ~f'(p) e z & b=g'(f'(p))]]

                        U Spec, 608

 

                  1129 (f'(p),p) e k <=> (f'(p),p) e xy & [f'(p) e z & p=f(f'(p)) | ~f'(p) e z & p=g'(f'(p))]

                        U Spec, 1128

 

                  1130 [(f'(p),p) e k => (f'(p),p) e xy & [f'(p) e z & p=f(f'(p)) | ~f'(p) e z & p=g'(f'(p))]]

                   & [(f'(p),p) e xy & [f'(p) e z & p=f(f'(p)) | ~f'(p) e z & p=g'(f'(p))] => (f'(p),p) e k]

                        Iff-And, 1129

 

                  1131 (f'(p),p) e k => (f'(p),p) e xy & [f'(p) e z & p=f(f'(p)) | ~f'(p) e z & p=g'(f'(p))]

                        Split, 1130

 

                  1132 (f'(p),p) e xy & [f'(p) e z & p=f(f'(p)) | ~f'(p) e z & p=g'(f'(p))] => (f'(p),p) e k

                        Split, 1130

 

                  1133 ALL(c2):[(f'(p),c2) e xy <=> f'(p) e x & c2 e y]

                        U Spec, 604

 

                  1134 (f'(p),p) e xy <=> f'(p) e x & p e y

                        U Spec, 1133

 

                  1135 [(f'(p),p) e xy => f'(p) e x & p e y]

                   & [f'(p) e x & p e y => (f'(p),p) e xy]

                        Iff-And, 1134

 

                  1136 (f'(p),p) e xy => f'(p) e x & p e y

                        Split, 1135

 

                  1137 f'(p) e x & p e y => (f'(p),p) e xy

                        Split, 1135

 

                  1138 p e imgF(z) => f'(p) e z

                        U Spec, 1043

 

                  1139 f'(p) e z

                        Detach, 1138, 1127

 

                  1140 ALL(b):[Subset(z,b) <=> ALL(c):[c e z => c e b]]

                        U Spec, 1

 

                  1141 Subset(z,x) <=> ALL(c):[c e z => c e x]

                        U Spec, 1140

 

                  1142 [Subset(z,x) => ALL(c):[c e z => c e x]]

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

                        Iff-And, 1141

 

                  1143 Subset(z,x) => ALL(c):[c e z => c e x]

                        Split, 1142

 

                  1144 ALL(c):[c e z => c e x] => Subset(z,x)

                        Split, 1142

 

                  1145 ALL(c):[c e z => c e x]

                        Detach, 1143, 400

 

                  1146 f'(p) e z => f'(p) e x

                        U Spec, 1145

 

                  1147 f'(p) e x

                        Detach, 1146, 1139

 

                  1148 f'(p) e x & p e y

                        Join, 1147, 1125

 

                  1149 (f'(p),p) e xy

                        Detach, 1137, 1148

 

                  1150 ALL(b):[f'(p) e z & b e imgF(z) => [f'(b)=f'(p) <=> f(f'(p))=b]]

                        U Spec, 1044

 

                  1151 f'(p) e z & p e imgF(z) => [f'(p)=f'(p) <=> f(f'(p))=p]

                        U Spec, 1150

 

                  1152 f'(p) e z & p e imgF(z)

                        Join, 1139, 1127

 

                  1153 f'(p)=f'(p) <=> f(f'(p))=p

                        Detach, 1151, 1152

 

                  1154 [f'(p)=f'(p) => f(f'(p))=p]

                   & [f(f'(p))=p => f'(p)=f'(p)]

                        Iff-And, 1153

 

                  1155 f'(p)=f'(p) => f(f'(p))=p

                        Split, 1154

 

                  1156 f(f'(p))=p => f'(p)=f'(p)

                        Split, 1154

 

                  1157 f'(p)=f'(p)

                        Reflex

 

                  1158 f(f'(p))=p

                        Detach, 1155, 1157

 

                  1159 p=f(f'(p))

                        Sym, 1158

 

                  1160 f'(p) e z & p=f(f'(p))

                        Join, 1139, 1159

 

                  1161 f'(p) e z & p=f(f'(p)) | ~f'(p) e z & p=g'(f'(p))

                        Arb Or, 1160

 

                  1162 (f'(p),p) e xy

                   & [f'(p) e z & p=f(f'(p)) | ~f'(p) e z & p=g'(f'(p))]

                        Join, 1149, 1161

 

                  1163 (f'(p),p) e k

                        Detach, 1132, 1162

 

                  1164 ALL(d):[d=k(f'(p)) <=> (f'(p),d) e k]

                        U Spec, 789

 

                  1165 p=k(f'(p)) <=> (f'(p),p) e k

                        U Spec, 1164

 

                  1166 [p=k(f'(p)) => (f'(p),p) e k]

                   & [(f'(p),p) e k => p=k(f'(p))]

                        Iff-And, 1165

 

                  1167 p=k(f'(p)) => (f'(p),p) e k

                        Split, 1166

 

                  1168 (f'(p),p) e k => p=k(f'(p))

                        Split, 1166

 

                  1169 p=k(f'(p))

                        Detach, 1168, 1163

 

                  1170 f'(p) e x & p=k(f'(p))

                        Join, 1147, 1169

 

                  1171 EXIST(b):[b e x & p=k(b)]

                        E Gen, 1170

 

          Case 1

         

          As Required:

 

            1172 p e imgF(z) => EXIST(b):[b e x & p=k(b)]

                  4 Conclusion, 1127

 

              Case 2

             

              Prove: ~p e imgF(z) => EXIST(b):[b e x & p=k(b)]

             

              Suppose...

 

                  1173 ~p e imgF(z)

                        Premise

 

                  1174 ALL(b):[(g(p),b) e k <=> (g(p),b) e xy & [g(p) e z & b=f(g(p)) | ~g(p) e z & b=g'(g(p))]]

                        U Spec, 608

 

                  1175 (g(p),p) e k <=> (g(p),p) e xy & [g(p) e z & p=f(g(p)) | ~g(p) e z & p=g'(g(p))]

                        U Spec, 1174

 

                  1176 [(g(p),p) e k => (g(p),p) e xy & [g(p) e z & p=f(g(p)) | ~g(p) e z & p=g'(g(p))]]

                   & [(g(p),p) e xy & [g(p) e z & p=f(g(p)) | ~g(p) e z & p=g'(g(p))] => (g(p),p) e k]

                        Iff-And, 1175

 

                  1177 (g(p),p) e k => (g(p),p) e xy & [g(p) e z & p=f(g(p)) | ~g(p) e z & p=g'(g(p))]

                        Split, 1176

 

                  1178 (g(p),p) e xy & [g(p) e z & p=f(g(p)) | ~g(p) e z & p=g'(g(p))] => (g(p),p) e k

                        Split, 1176

 

                  1179 ALL(c2):[(g(p),c2) e xy <=> g(p) e x & c2 e y]

                        U Spec, 604

 

                  1180 (g(p),p) e xy <=> g(p) e x & p e y

                        U Spec, 1179

 

                  1181 [(g(p),p) e xy => g(p) e x & p e y]

                   & [g(p) e x & p e y => (g(p),p) e xy]

                        Iff-And, 1180

 

                  1182 (g(p),p) e xy => g(p) e x & p e y

                        Split, 1181

 

                  1183 g(p) e x & p e y => (g(p),p) e xy

                        Split, 1181

 

                  1184 p e y => g(p) e x

                        U Spec, 15

 

                  1185 g(p) e x

                        Detach, 1184, 1125

 

                  1186 g(p) e x & p e y

                        Join, 1185, 1125

 

                  1187 (g(p),p) e xy

                        Detach, 1183, 1186

 

                  1188 p e cy(imgF(z)) => g(p) e imgG(cy(imgF(z)))

                        U Spec, 521

 

                  1189 p e y => [p e cy(imgF(z)) <=> ~p e imgF(z)]

                        U Spec, 463

 

                  1190 p e cy(imgF(z)) <=> ~p e imgF(z)

                        Detach, 1189, 1125

 

                  1191 [p e cy(imgF(z)) => ~p e imgF(z)]

                   & [~p e imgF(z) => p e cy(imgF(z))]

                        Iff-And, 1190

 

                  1192 p e cy(imgF(z)) => ~p e imgF(z)

                        Split, 1191

 

                  1193 ~p e imgF(z) => p e cy(imgF(z))

                        Split, 1191

 

                  1194 p e cy(imgF(z))

                        Detach, 1193, 1173

 

                  1195 p e cy(imgF(z)) => g(p) e imgG(cy(imgF(z)))

                        U Spec, 521

 

                  1196 g(p) e imgG(cy(imgF(z)))

                        Detach, 1195, 1194

 

                  1197 g(p) e x => [g(p) e cx(z) <=> ~g(p) e z]

                        U Spec, 467

 

                  1198 p e y => g(p) e x

                        U Spec, 15

 

                  1199 g(p) e x

                        Detach, 1198, 1125

 

                  1200 g(p) e cx(z) <=> ~g(p) e z

                        Detach, 1197, 1199

 

                  1201 [g(p) e cx(z) => ~g(p) e z]

                   & [~g(p) e z => g(p) e cx(z)]

                        Iff-And, 1200

 

              Sufficient:

 

                  1202 g(p) e cx(z) => ~g(p) e z

                        Split, 1201

 

                  1203 ~g(p) e z => g(p) e cx(z)

                        Split, 1201

 

                  1204 g(p) e imgG(cy(imgF(z))) => ~g(p) e z

                        Substitute, 448, 1202

 

                  1205 ~g(p) e z

                        Detach, 1204, 1196

 

                  1206 ALL(b):[p e cy(imgF(z)) & b e cx(z) => [g'(b)=p <=> g(p)=b]]

                        U Spec, 581

 

                  1207 p e cy(imgF(z)) & g(p) e cx(z) => [g'(g(p))=p <=> g(p)=g(p)]

                        U Spec, 1206

 

                  1208 g(p) e x => [g(p) e cx(z) <=> ~g(p) e z]

                        U Spec, 467

 

                  1209 g(p) e cx(z) <=> ~g(p) e z

                        Detach, 1208, 1199

 

                  1210 [g(p) e cx(z) => ~g(p) e z]

                   & [~g(p) e z => g(p) e cx(z)]

                        Iff-And, 1209

 

                  1211 g(p) e cx(z) => ~g(p) e z

                        Split, 1210

 

                  1212 ~g(p) e z => g(p) e cx(z)

                        Split, 1210

 

                  1213 g(p) e cx(z)

                        Detach, 1212, 1205

 

                  1214 p e cy(imgF(z)) & g(p) e cx(z)

                        Join, 1194, 1213

 

                  1215 g'(g(p))=p <=> g(p)=g(p)

                        Detach, 1207, 1214

 

                  1216 [g'(g(p))=p => g(p)=g(p)] & [g(p)=g(p) => g'(g(p))=p]

                        Iff-And, 1215

 

                  1217 g'(g(p))=p => g(p)=g(p)

                        Split, 1216

 

                  1218 g(p)=g(p) => g'(g(p))=p

                        Split, 1216

 

                  1219 g(p)=g(p)

                        Reflex

 

                  1220 g'(g(p))=p

                        Detach, 1218, 1219

 

                  1221 p=g'(g(p))

                        Sym, 1220

 

                  1222 ~g(p) e z & p=g'(g(p))

                        Join, 1205, 1221

 

                  1223 g(p) e z & p=f(g(p)) | ~g(p) e z & p=g'(g(p))

                        Arb Or, 1222

 

                  1224 (g(p),p) e xy

                   & [g(p) e z & p=f(g(p)) | ~g(p) e z & p=g'(g(p))]

                        Join, 1187, 1223

 

                  1225 (g(p),p) e k

                        Detach, 1178, 1224

 

                  1226 ALL(d):[d=k(g(p)) <=> (g(p),d) e k]

                        U Spec, 789

 

                  1227 p=k(g(p)) <=> (g(p),p) e k

                        U Spec, 1226

 

                  1228 [p=k(g(p)) => (g(p),p) e k]

                   & [(g(p),p) e k => p=k(g(p))]

                        Iff-And, 1227

 

                  1229 p=k(g(p)) => (g(p),p) e k

                        Split, 1228

 

                  1230 (g(p),p) e k => p=k(g(p))

                        Split, 1228

 

                  1231 p=k(g(p))

                        Detach, 1230, 1225

 

                  1232 g(p) e x & p=k(g(p))

                        Join, 1199, 1231

 

                  1233 EXIST(b):[b e x & p=k(b)]

                        E Gen, 1232

 

          Case 2

         

          As Required:

 

            1234 ~p e imgF(z) => EXIST(b):[b e x & p=k(b)]

                  4 Conclusion, 1173

 

            1235 [p e imgF(z) => EXIST(b):[b e x & p=k(b)]]

              & [~p e imgF(z) => EXIST(b):[b e x & p=k(b)]]

                  Join, 1172, 1234

 

            1236 EXIST(b):[b e x & p=k(b)]

                  Cases, 1126, 1235

 

            1237 EXIST(b):[b e x & k(b)=p]

                  Sym, 1236

 

     k is surjective

    

     As Required:

 

      1238 ALL(a):[a e y => EXIST(b):[b e x & k(b)=a]]

            4 Conclusion, 1125

 

    

     Use Injection, Surjection and Bijection predicates

 

      1239 ALL(a):ALL(b):[Bijection(k,a,b) <=> Injection(k,a,b) & Surjection(k,a,b)]

            U Spec, 4

 

      1240 ALL(b):[Bijection(k,x,b) <=> Injection(k,x,b) & Surjection(k,x,b)]

            U Spec, 1239

 

      1241 Bijection(k,x,y) <=> Injection(k,x,y) & Surjection(k,x,y)

            U Spec, 1240

 

      1242 [Bijection(k,x,y) => Injection(k,x,y) & Surjection(k,x,y)]

          & [Injection(k,x,y) & Surjection(k,x,y) => Bijection(k,x,y)]

            Iff-And, 1241

 

      1243 Bijection(k,x,y) => Injection(k,x,y) & Surjection(k,x,y)

            Split, 1242

 

      1244 Injection(k,x,y) & Surjection(k,x,y) => Bijection(k,x,y)

            Split, 1242

 

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

            U Spec, 2

 

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

            U Spec, 1245

 

      1247 Injection(k,x,y) <=> ALL(c):ALL(d):[c e x & d e x => [k(c)=k(d) => c=d]]

            U Spec, 1246

 

      1248 [Injection(k,x,y) => ALL(c):ALL(d):[c e x & d e x => [k(c)=k(d) => c=d]]]

          & [ALL(c):ALL(d):[c e x & d e x => [k(c)=k(d) => c=d]] => Injection(k,x,y)]

            Iff-And, 1247

 

      1249 Injection(k,x,y) => ALL(c):ALL(d):[c e x & d e x => [k(c)=k(d) => c=d]]

            Split, 1248

 

      1250 ALL(c):ALL(d):[c e x & d e x => [k(c)=k(d) => c=d]] => Injection(k,x,y)

            Split, 1248

 

      1251 Injection(k,x,y)

            Detach, 1250, 1029

 

      1252 ALL(a):ALL(b):[Surjection(k,a,b) <=> ALL(c):[c e b => EXIST(d):[d e a & k(d)=c]]]

            U Spec, 3

 

      1253 ALL(b):[Surjection(k,x,b) <=> ALL(c):[c e b => EXIST(d):[d e x & k(d)=c]]]

            U Spec, 1252

 

      1254 Surjection(k,x,y) <=> ALL(c):[c e y => EXIST(d):[d e x & k(d)=c]]

            U Spec, 1253

 

      1255 [Surjection(k,x,y) => ALL(c):[c e y => EXIST(d):[d e x & k(d)=c]]]

          & [ALL(c):[c e y => EXIST(d):[d e x & k(d)=c]] => Surjection(k,x,y)]

            Iff-And, 1254

 

      1256 Surjection(k,x,y) => ALL(c):[c e y => EXIST(d):[d e x & k(d)=c]]

            Split, 1255

 

      1257 ALL(c):[c e y => EXIST(d):[d e x & k(d)=c]] => Surjection(k,x,y)

            Split, 1255

 

      1258 Surjection(k,x,y)

            Detach, 1257, 1238

 

      1259 Injection(k,x,y) & Surjection(k,x,y)

            Join, 1251, 1258

 

      1260 Bijection(k,x,y)

            Detach, 1244, 1259

 

     As Required:

 

      1261 ALL(a):[a e x => k(a) e y] & Bijection(k,x,y)

            Join, 803, 1260

 

As Required:

 

1262 ALL(s1):ALL(s2):ALL(f1):ALL(f2):[Set(s1)

     & Set(s2)

     & ALL(a):[a e s1 => f1(a) e s2]

     & ALL(a):[a e s2 => f2(a) e s1]

     & Injection(f1,s1,s2)

     & Injection(f2,s2,s1)

     => EXIST(f3):[ALL(a):[a e s1 => f3(a) e s2] & Bijection(f3,s1,s2)]]

      4 Conclusion, 11