THEOREM

*******

 

  ALL(s):[Set(s) & EXIST(a):a e s

  => [Countable(s) => EXIST(f2):[ALL(c):[c e n => f2(c) e s] & Surjection(f2,n,s)]]]

 

(This formal proof was write and verified with the aid of the author's DC Proof 2.0 software available free at http://www.dcproof.com )

 

 

PREVIOUS RESULTS

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

 

Injective function f1: A --> B for non-empty A, implies existence of surjective f1: B --> A  (See proof)

 

1     ALL(a):ALL(b):ALL(f1):[Set(a) & Set(b) & EXIST(c):c e a & ALL(c):[c e a => f1(c) e b]

     & Injection(f1,a,b)

     => EXIST(f2):[ALL(c):[c e b => f2(c) e a] & Surjection(f2,b,a)]]

      Axiom

 

 

 

DEFINITIONS

***********

 

Let n be the set of natural numbers

 

2     Set(n)

      Axiom

 

 

Define: Countable

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

 

3     ALL(s):[Set(s) => [Countable(s)

     <=> EXIST(f):[ALL(b):[b e s => f(b) e n]

     & Injection(f,s,n)]]]

      Axiom

 

 

Define: Surjection

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

 

4     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: Injection

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

 

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

     => c=d]]]

      Axiom

 

    

     PROOF

     *****

    

     Prove: ALL(s):[Set(s) & EXIST(a):a e s

            => [Countable(s) => EXIST(f):[ALL(a):[a e n => a e s] & Surjection(f,n,s)]]]

    

     Suppose...

 

      6     Set(s) & EXIST(a):a e s

            Premise

 

      7     Set(s)

            Split, 6

 

      8     EXIST(a):a e s

            Split, 6

 

     Define: x0

 

      9     x0 e s

            E Spec, 8

 

         

          Prove: Countable(s) => EXIST(f):[ALL(a):[a e n => a e s] & Surjection(f,n,s)]]

         

          Suppose...

 

            10    Countable(s)

                  Premise

 

            11    Set(s) => [Countable(s)

              <=> EXIST(f):[ALL(b):[b e s => f(b) e n]

              & Injection(f,s,n)]]

                  U Spec, 3

 

            12    Countable(s)

              <=> EXIST(f):[ALL(b):[b e s => f(b) e n]

              & Injection(f,s,n)]

                  Detach, 11, 7

 

            13    [Countable(s) => EXIST(f):[ALL(b):[b e s => f(b) e n]

              & Injection(f,s,n)]]

              & [EXIST(f):[ALL(b):[b e s => f(b) e n]

              & Injection(f,s,n)] => Countable(s)]

                  Iff-And, 12

 

            14    Countable(s) => EXIST(f):[ALL(b):[b e s => f(b) e n]

              & Injection(f,s,n)]

                  Split, 13

 

            15    EXIST(f):[ALL(b):[b e s => f(b) e n]

              & Injection(f,s,n)] => Countable(s)

                  Split, 13

 

            16    EXIST(f):[ALL(b):[b e s => f(b) e n]

              & Injection(f,s,n)]

                  Detach, 14, 10

 

            17    ALL(b):[b e s => f(b) e n]

              & Injection(f,s,n)

                  E Spec, 16

 

            18    ALL(b):[b e s => f(b) e n]

                  Split, 17

 

            19    Injection(f,s,n)

                  Split, 17

 

            20    ALL(b):ALL(f1):[Set(s) & Set(b) & EXIST(c):c e s & ALL(c):[c e s

              => f1(c) e b] & Injection(f1,s,b)

              => EXIST(f2):[ALL(c):[c e b => f2(c) e s] & Surjection(f2,b,s)]]

                  U Spec, 1

 

            21    ALL(f1):[Set(s) & Set(n) & EXIST(c):c e s & ALL(c):[c e s => f1(c) e n]

              & Injection(f1,s,n)

              => EXIST(f2):[ALL(c):[c e n => f2(c) e s] & Surjection(f2,n,s)]]

                  U Spec, 20

 

            22    Set(s) & Set(n) & EXIST(c):c e s & ALL(c):[c e s => f(c) e n] & Injection(f,s,n)

              => EXIST(f2):[ALL(c):[c e n => f2(c) e s] & Surjection(f2,n,s)]

                  U Spec, 21

 

            23    Set(s) & Set(n)

                  Join, 7, 2

 

            24    Set(s) & Set(n) & EXIST(a):a e s

                  Join, 23, 8

 

            25    Set(s) & Set(n) & EXIST(a):a e s

              & ALL(b):[b e s => f(b) e n]

                  Join, 24, 18

 

            26    Set(s) & Set(n) & EXIST(a):a e s

              & ALL(b):[b e s => f(b) e n]

              & Injection(f,s,n)

                  Join, 25, 19

 

            27    EXIST(f2):[ALL(c):[c e n => f2(c) e s] & Surjection(f2,n,s)]

                  Detach, 22, 26

 

      28    Countable(s)

          => EXIST(f2):[ALL(c):[c e n => f2(c) e s] & Surjection(f2,n,s)]

            4 Conclusion, 10

 

As Required:

 

29    ALL(s):[Set(s) & EXIST(a):a e s

     => [Countable(s)

     => EXIST(f2):[ALL(c):[c e n => f2(c) e s] & Surjection(f2,n,s)]]]

      4 Conclusion, 6