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