THEOREM

-------

 

ALL(a):[Subset(a,sA) => a=pre(img(a))] <=> FOnto

 

where

 

f is a function mapping set sA to set sB

 

img(x) = the image set of set x under f

pre(x) = the pre-image set of x under f

 

Subset(x,y) means x is a subset of y

FOnto       means f is injective (onto)

 

&   means AND

|   means OR

=>  means IMPLIES

<=> means IF AND ONLY IF

 

 

By Dan Christensen

 

This proof written using proof assistant software developed by the author and available free at:

http://www.dcproof.com

 

 

OUTLINE

-------

 

Let f be a function mapping set sA to set sB.

 

Suppose f is onto.

 

  Suppose s is a subset of sA. Prove s = pre(img(s))

 

    '=>'

    Suppose x e s

 

      Show x e pre(img(s)

 

    '<='

    Suppose ~ x e s  (proof by contrapositive)

 

      Case 1: Suppose x e sA

 

        Suppose x e pre(img(s))

 

        Obtain contradiction.       

 

      Case 2: Suppose ~ x e sA

 

        Show ~ x e pre(img(s))

 

    Therefore, s = pre(img(s))

 

Suppose f is not onto.  (proof by contrapositive)

 

  Let x and y be distinct elements of sA such that f(x)=f(y).

 

  Construct the singleton {x} (a subset of sA).

 

  Show {x} not equal to pre(img({x})).

 

  Therefore, not all subsets s of sA are such that s = pre(img(s)).

 

 

AXIOMS/DEFINITIONS

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

 

Define: set equality

 

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

      Axiom

 

Define: Subset

 

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

      Axiom

 

Define: Sets sA and sB

 

3     Set(sA)

      Axiom

 

4     Set(sB)

      Axiom

 

Define: f

 

f is a function mapping set sA to set sB

 

5     ALL(a):[a e sA => f(a) e sB]

      Axiom

 

Define: FOnto  (f is injective (onto))

 

6     FOnto <=> ALL(a):ALL(b):[a e sA & b e sA => [f(a)=f(b) => a=b]]

      Axiom

 

Define: img

 

img(x) = the image set of set x under f

 

7     ALL(a):[Subset(a,sA) => Subset(img(a),sB)

     & ALL(b):[b e img(a) <=> EXIST(c):[c e a & f(c)=b]]]

      Axiom

 

Define: pre

 

pre(x) = the pre-image set of set x under f

 

8     ALL(a):[Subset(a,sB) => Subset(pre(a),sA)

     & ALL(b):[b e pre(a) <=> EXIST(c):[c e a & f(b)=c]]]

      Axiom

 

    

     Prove: FOnto => ALL(a):[Subset(a,sA) => a=pre(img(a))]

    

     Suppose...

 

      9     FOnto

            Premise

 

     Apply definition of FOnto

 

      10    [FOnto => ALL(a):ALL(b):[a e sA & b e sA => [f(a)=f(b) => a=b]]]

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

            Iff-And, 6

 

      11    FOnto => ALL(a):ALL(b):[a e sA & b e sA => [f(a)=f(b) => a=b]]

            Split, 10

 

      12    ALL(a):ALL(b):[a e sA & b e sA => [f(a)=f(b) => a=b]] => FOnto

            Split, 10

 

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

            Detach, 11, 9

 

         

          Prove: ALL(a):[Subset(a,sA) => a=pre(img(a))]

         

          Suppose...

 

            14    Subset(s,sA)

                  Premise

 

          Apply definiton of Subset

 

            15    ALL(b):[Subset(s,b) <=> ALL(c):[c e s => c e b]]

                  U Spec, 2

 

            16    Subset(s,sA) <=> ALL(c):[c e s => c e sA]

                  U Spec, 15

 

            17    [Subset(s,sA) => ALL(c):[c e s => c e sA]]

              & [ALL(c):[c e s => c e sA] => Subset(s,sA)]

                  Iff-And, 16

 

            18    Subset(s,sA) => ALL(c):[c e s => c e sA]

                  Split, 17

 

            19    ALL(c):[c e s => c e sA] => Subset(s,sA)

                  Split, 17

 

            20    ALL(c):[c e s => c e sA]

                  Detach, 18, 14

 

          Apply definition of img

 

            21    Subset(s,sA) => Subset(img(s),sB)

              & ALL(b):[b e img(s) <=> EXIST(c):[c e s & f(c)=b]]

                  U Spec, 7

 

            22    Subset(img(s),sB)

              & ALL(b):[b e img(s) <=> EXIST(c):[c e s & f(c)=b]]

                  Detach, 21, 14

 

            23    Subset(img(s),sB)

                  Split, 22

 

            24    ALL(b):[b e img(s) <=> EXIST(c):[c e s & f(c)=b]]

                  Split, 22

 

          Apply definiton of pre

 

            25    Subset(img(s),sB) => Subset(pre(img(s)),sA)

              & ALL(b):[b e pre(img(s)) <=> EXIST(c):[c e img(s) & f(b)=c]]

                  U Spec, 8

 

            26    Subset(pre(img(s)),sA)

              & ALL(b):[b e pre(img(s)) <=> EXIST(c):[c e img(s) & f(b)=c]]

                  Detach, 25, 23

 

            27    Subset(pre(img(s)),sA)

                  Split, 26

 

            28    ALL(b):[b e pre(img(s)) <=> EXIST(c):[c e img(s) & f(b)=c]]

                  Split, 26

 

            29    ALL(b):[s=b <=> ALL(c):[c e s <=> c e b]]

                  U Spec, 1

 

            30    s=pre(img(s)) <=> ALL(c):[c e s <=> c e pre(img(s))]

                  U Spec, 29

 

            31    [s=pre(img(s)) => ALL(c):[c e s <=> c e pre(img(s))]]

              & [ALL(c):[c e s <=> c e pre(img(s))] => s=pre(img(s))]

                  Iff-And, 30

 

            32    s=pre(img(s)) => ALL(c):[c e s <=> c e pre(img(s))]

                  Split, 31

 

          Sufficient: For s=pre(img(s))

 

            33    ALL(c):[c e s <=> c e pre(img(s))] => s=pre(img(s))

                  Split, 31

 

              

              Prove: ALL(c):[c e s => c e pre(img(s))]

             

              Suppose...

 

                  34    x e s

                        Premise

 

              Apply definition of pre

 

                  35    x e pre(img(s)) <=> EXIST(c):[c e img(s) & f(x)=c]

                        U Spec, 28

 

                  36    [x e pre(img(s)) => EXIST(c):[c e img(s) & f(x)=c]]

                   & [EXIST(c):[c e img(s) & f(x)=c] => x e pre(img(s))]

                        Iff-And, 35

 

                  37    x e pre(img(s)) => EXIST(c):[c e img(s) & f(x)=c]

                        Split, 36

 

              Sufficient: For x e pre(img(s))

 

                  38    EXIST(c):[c e img(s) & f(x)=c] => x e pre(img(s))

                        Split, 36

 

              Apply definition of img

 

                  39    f(x) e img(s) <=> EXIST(c):[c e s & f(c)=f(x)]

                        U Spec, 24

 

                  40    [f(x) e img(s) => EXIST(c):[c e s & f(c)=f(x)]]

                   & [EXIST(c):[c e s & f(c)=f(x)] => f(x) e img(s)]

                        Iff-And, 39

 

                  41    f(x) e img(s) => EXIST(c):[c e s & f(c)=f(x)]

                        Split, 40

 

              Sufficient: For f(x) e img(s)

 

                  42    EXIST(c):[c e s & f(c)=f(x)] => f(x) e img(s)

                        Split, 40

 

                  43    f(x)=f(x)

                        Reflex

 

                  44    x e s & f(x)=f(x)

                        Join, 34, 43

 

                  45    EXIST(c):[c e s & f(c)=f(x)]

                        E Gen, 44

 

                  46    f(x) e img(s)

                        Detach, 42, 45

 

                  47    f(x) e img(s) & f(x)=f(x)

                        Join, 46, 43

 

                  48    EXIST(c):[c e img(s) & f(x)=c]

                        E Gen, 47

 

                  49    x e pre(img(s))

                        Detach, 38, 48

 

          As Required:

 

            50    ALL(c):[c e s => c e pre(img(s))]

                  4 Conclusion, 34

 

              

              Prove: ALL(c):[~c e s => ~c e pre(img(s))]

             

              Suppose...

 

                  51    ~x e s

                        Premise

 

              Two cases to consider:

 

                  52    x e sA | ~x e sA

                        Or Not

 

                   Case 1:

                  

                   Prove: x e sA => ~x e pre(img(s))

                  

                   Suppose...

 

                        53    x e sA

                              Premise

 

                       

                        Suppose to the contrary...

 

                              54    x e pre(img(s))

                                    Premise

 

                        Apply definition of pre

 

                              55    x e pre(img(s)) <=> EXIST(c):[c e img(s) & f(x)=c]

                                    U Spec, 28

 

                              56    [x e pre(img(s)) => EXIST(c):[c e img(s) & f(x)=c]]

                             & [EXIST(c):[c e img(s) & f(x)=c] => x e pre(img(s))]

                                    Iff-And, 55

 

                              57    x e pre(img(s)) => EXIST(c):[c e img(s) & f(x)=c]

                                                      Split, 56

 

                              58    EXIST(c):[c e img(s) & f(x)=c] => x e pre(img(s))

                                                       Split, 56

 

                              59    EXIST(c):[c e img(s) & f(x)=c]

                                    Detach, 57, 54

 

                              60    y e img(s) & f(x)=y

                                    E Spec, 59

 

                        Define: y

 

                              61    y e img(s)

                                                      Split, 60

 

                              62    f(x)=y

                                                       Split, 60

 

                              63    f(x) e img(s)

                                    Substitute, 62, 61

 

                        Apply definition of img

 

                              64    f(x) e img(s) <=> EXIST(c):[c e s & f(c)=f(x)]

                                    U Spec, 24

 

                              65    [f(x) e img(s) => EXIST(c):[c e s & f(c)=f(x)]]

                             & [EXIST(c):[c e s & f(c)=f(x)] => f(x) e img(s)]

                                    Iff-And, 64

 

                              66    f(x) e img(s) => EXIST(c):[c e s & f(c)=f(x)]

                                                       Split, 65

 

                              67    EXIST(c):[c e s & f(c)=f(x)] => f(x) e img(s)

                                                      Split, 65

 

                              68    EXIST(c):[c e s & f(c)=f(x)]

                                    Detach, 66, 63

 

                              69    z e s & f(z)=f(x)

                                    E Spec, 68

 

                              70    z e s

                                                                         Split, 69

 

                              71    f(z)=f(x)

                                                                        Split, 69

 

                        Apply definition of FOnto

 

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

                                    U Spec, 13

 

                              73    z e sA & x e sA => [f(z)=f(x) => z=x]

                                    U Spec, 72

 

                              74    z e s => z e sA

                                    U Spec, 20

 

                              75    z e sA

                                    Detach, 74, 70

 

                              76    z e sA & x e sA

                                    Join, 75, 53

 

                              77    f(z)=f(x) => z=x

                                    Detach, 73, 76

 

                              78    z=x

                                    Detach, 77, 71

 

                              79    x e s

                                    Substitute, 78, 70

 

                              80    x e s & ~x e s

                                    Join, 79, 51

 

                   As Required:

 

                        81    ~x e pre(img(s))

                              4 Conclusion, 54

 

              As Required:

 

                  82    x e sA => ~x e pre(img(s))

                        4 Conclusion, 53

 

                   Case 2:

                  

                   Prove: ~x e sA => ~x e pre(img(s))

                  

                   Suppose...

 

                        83    ~x e sA

                              Premise

 

                   Apply definition of Subset

 

                        84    ALL(b):[Subset(pre(img(s)),b) <=> ALL(c):[c e pre(img(s)) => c e b]]

                              U Spec, 2

 

                        85    Subset(pre(img(s)),sA) <=> ALL(c):[c e pre(img(s)) => c e sA]

                              U Spec, 84

 

                        86    [Subset(pre(img(s)),sA) => ALL(c):[c e pre(img(s)) => c e sA]]

                        & [ALL(c):[c e pre(img(s)) => c e sA] => Subset(pre(img(s)),sA)]

                              Iff-And, 85

 

                        87    Subset(pre(img(s)),sA) => ALL(c):[c e pre(img(s)) => c e sA]

                              Split, 86

 

                        88    ALL(c):[c e pre(img(s)) => c e sA] => Subset(pre(img(s)),sA)

                              Split, 86

 

                        89    ALL(c):[c e pre(img(s)) => c e sA]

                              Detach, 87, 27

 

                        90    x e pre(img(s)) => x e sA

                              U Spec, 89

 

                        91    ~x e sA => ~x e pre(img(s))

                              Contra, 90

 

                        92    ~x e pre(img(s))

                              Detach, 91, 83

 

              As Required:

 

                  93    ~x e sA => ~x e pre(img(s))

                        4 Conclusion, 83

 

                  94    [x e sA => ~x e pre(img(s))]

                   & [~x e sA => ~x e pre(img(s))]

                        Join, 82, 93

 

                  95    ~x e pre(img(s))

                        Cases, 52, 94

 

          As Required:

 

            96    ALL(c):[~c e s => ~c e pre(img(s))]

                  4 Conclusion, 51

 

            97    ALL(c):[~~c e pre(img(s)) => ~~c e s]

                  Contra, 96

 

            98    ALL(c):[c e pre(img(s)) => ~~c e s]

                  Rem DNeg, 97

 

            99    ALL(c):[c e pre(img(s)) => c e s]

                  Rem DNeg, 98

 

            100  ALL(c):[[c e s => c e pre(img(s))] & [c e pre(img(s)) => c e s]]

                  Join, 50, 99

 

            101  ALL(c):[c e s <=> c e pre(img(s))]

                  Iff-And, 100

 

            102  s=pre(img(s))

                  Detach, 33, 101

 

     As Required:

 

      103  ALL(a):[Subset(a,sA) => a=pre(img(a))]

            4 Conclusion, 14

 

As Required:

 

104  FOnto => ALL(a):[Subset(a,sA) => a=pre(img(a))]

      4 Conclusion, 9

 

    

     Prove: ~FOnto => ~ALL(a):[Subset(a,sA) => a=pre(img(a))]

    

     Suppose...

 

      105  ~FOnto

            Premise

 

     Apply definition of FOnto

 

      106  [FOnto => ALL(a):ALL(b):[a e sA & b e sA => [f(a)=f(b) => a=b]]]

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

            Iff-And, 6

 

      107  FOnto => ALL(a):ALL(b):[a e sA & b e sA => [f(a)=f(b) => a=b]]

            Split, 106

 

      108  ALL(a):ALL(b):[a e sA & b e sA => [f(a)=f(b) => a=b]] => FOnto

            Split, 106

 

      109  ~FOnto => ~ALL(a):ALL(b):[a e sA & b e sA => [f(a)=f(b) => a=b]]

            Contra, 108

 

      110  ~ALL(a):ALL(b):[a e sA & b e sA => [f(a)=f(b) => a=b]]

            Detach, 109, 105

 

      111  ~~EXIST(a):~ALL(b):[a e sA & b e sA => [f(a)=f(b) => a=b]]

            Quant, 110

 

      112  EXIST(a):~ALL(b):[a e sA & b e sA => [f(a)=f(b) => a=b]]

            Rem DNeg, 111

 

      113  EXIST(a):~~EXIST(b):~[a e sA & b e sA => [f(a)=f(b) => a=b]]

            Quant, 112

 

      114  EXIST(a):EXIST(b):~[a e sA & b e sA => [f(a)=f(b) => a=b]]

            Rem DNeg, 113

 

      115  EXIST(a):EXIST(b):~~[a e sA & b e sA & ~[f(a)=f(b) => a=b]]

            Imply-And, 114

 

      116  EXIST(a):EXIST(b):[a e sA & b e sA & ~[f(a)=f(b) => a=b]]

            Rem DNeg, 115

 

      117  EXIST(a):EXIST(b):[a e sA & b e sA & ~~[f(a)=f(b) & ~a=b]]

            Imply-And, 116

 

      118  EXIST(a):EXIST(b):[a e sA & b e sA & [f(a)=f(b) & ~a=b]]

            Rem DNeg, 117

 

      119  EXIST(b):[x e sA & b e sA & [f(x)=f(b) & ~x=b]]

            E Spec, 118

 

      120  x e sA & y e sA & [f(x)=f(y) & ~x=y]

            E Spec, 119

 

     Define: x and y  (distinct elements of sA with identical images under f)

 

      121  x e sA

            Split, 120

 

      122  y e sA

            Split, 120

 

      123  f(x)=f(y) & ~x=y

            Split, 120

 

      124  f(x)=f(y)

            Split, 123

 

      125  ~x=y

            Split, 123

 

     Construct the singleton {x}

    

     Apply the Subset Axiom

 

      126  EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e sA & a=x]]

            Subset, 3

 

      127  Set(onlyX) & ALL(a):[a e onlyX <=> a e sA & a=x]

            E Spec, 126

 

     Define: onlyX  (subset of sA, a singleton)

 

      128  Set(onlyX)

            Split, 127

 

      129  ALL(a):[a e onlyX <=> a e sA & a=x]

            Split, 127

 

     Apply definition of Subset

 

      130  ALL(b):[Subset(onlyX,b) <=> ALL(c):[c e onlyX => c e b]]

            U Spec, 2

 

      131  Subset(onlyX,sA) <=> ALL(c):[c e onlyX => c e sA]

            U Spec, 130

 

      132  [Subset(onlyX,sA) => ALL(c):[c e onlyX => c e sA]]

          & [ALL(c):[c e onlyX => c e sA] => Subset(onlyX,sA)]

            Iff-And, 131

 

      133  Subset(onlyX,sA) => ALL(c):[c e onlyX => c e sA]

            Split, 132

 

      134  ALL(c):[c e onlyX => c e sA] => Subset(onlyX,sA)

            Split, 132

 

         

          Prove: ALL(c):[c e onlyX => c e sA]

         

          Suppose...

 

            135  z e onlyX

                  Premise

 

          Apply definition of onlyX

 

            136  z e onlyX <=> z e sA & z=x

                  U Spec, 129

 

            137  [z e onlyX => z e sA & z=x]

              & [z e sA & z=x => z e onlyX]

                  Iff-And, 136

 

            138  z e onlyX => z e sA & z=x

                  Split, 137

 

            139  z e sA & z=x => z e onlyX

                  Split, 137

 

            140  z e sA & z=x

                  Detach, 138, 135

 

            141  z e sA

                  Split, 140

 

     As Required:

 

      142  ALL(c):[c e onlyX => c e sA]

            4 Conclusion, 135

 

      143  Subset(onlyX,sA)

            Detach, 134, 142

 

     Apply definition of img

 

      144  Subset(onlyX,sA) => Subset(img(onlyX),sB)

          & ALL(b):[b e img(onlyX) <=> EXIST(c):[c e onlyX & f(c)=b]]

            U Spec, 7

 

      145  Subset(img(onlyX),sB)

          & ALL(b):[b e img(onlyX) <=> EXIST(c):[c e onlyX & f(c)=b]]

            Detach, 144, 143

 

      146  Subset(img(onlyX),sB)

            Split, 145

 

      147  ALL(b):[b e img(onlyX) <=> EXIST(c):[c e onlyX & f(c)=b]]

            Split, 145

 

     Apply defintion of pre

 

      148  Subset(img(onlyX),sB) => Subset(pre(img(onlyX)),sA)

          & ALL(b):[b e pre(img(onlyX)) <=> EXIST(c):[c e img(onlyX) & f(b)=c]]

            U Spec, 8

 

      149  Subset(pre(img(onlyX)),sA)

          & ALL(b):[b e pre(img(onlyX)) <=> EXIST(c):[c e img(onlyX) & f(b)=c]]

            Detach, 148, 146

 

      150  Subset(pre(img(onlyX)),sA)

            Split, 149

 

      151  ALL(b):[b e pre(img(onlyX)) <=> EXIST(c):[c e img(onlyX) & f(b)=c]]

            Split, 149

 

      152  y e pre(img(onlyX)) <=> EXIST(c):[c e img(onlyX) & f(y)=c]

            U Spec, 151

 

      153  [y e pre(img(onlyX)) => EXIST(c):[c e img(onlyX) & f(y)=c]]

          & [EXIST(c):[c e img(onlyX) & f(y)=c] => y e pre(img(onlyX))]

            Iff-And, 152

 

      154  y e pre(img(onlyX)) => EXIST(c):[c e img(onlyX) & f(y)=c]

            Split, 153

 

     Sufficient: For y e pre(img(onlyX))

 

      155  EXIST(c):[c e img(onlyX) & f(y)=c] => y e pre(img(onlyX))

            Split, 153

 

     Apply definition of onlyX

 

      156  f(y) e img(onlyX) <=> EXIST(c):[c e onlyX & f(c)=f(y)]

            U Spec, 147

 

      157  [f(y) e img(onlyX) => EXIST(c):[c e onlyX & f(c)=f(y)]]

          & [EXIST(c):[c e onlyX & f(c)=f(y)] => f(y) e img(onlyX)]

            Iff-And, 156

 

      158  f(y) e img(onlyX) => EXIST(c):[c e onlyX & f(c)=f(y)]

            Split, 157

 

     Sufficient: For f(y) e img(onlyX)

 

      159  EXIST(c):[c e onlyX & f(c)=f(y)] => f(y) e img(onlyX)

            Split, 157

 

      160  x e onlyX <=> x e sA & x=x

            U Spec, 129

 

      161  [x e onlyX => x e sA & x=x]

          & [x e sA & x=x => x e onlyX]

            Iff-And, 160

 

      162  x e onlyX => x e sA & x=x

            Split, 161

 

      163  x e sA & x=x => x e onlyX

            Split, 161

 

      164  x=x

            Reflex

 

      165  x e sA & x=x

            Join, 121, 164

 

      166  x e onlyX

            Detach, 163, 165

 

      167  x e onlyX & f(x)=f(y)

            Join, 166, 124

 

      168  EXIST(c):[c e onlyX & f(c)=f(y)]

            E Gen, 167

 

      169  f(y) e img(onlyX)

            Detach, 159, 168

 

      170  f(y)=f(y)

            Reflex

 

      171  f(y) e img(onlyX) & f(y)=f(y)

            Join, 169, 170

 

      172  EXIST(c):[c e img(onlyX) & f(y)=c]

            E Gen, 171

 

      173  y e pre(img(onlyX))

            Detach, 155, 172

 

     Apply definition of set equality

 

      174  ALL(b):[onlyX=b <=> ALL(c):[c e onlyX <=> c e b]]

            U Spec, 1

 

      175  onlyX=pre(img(onlyX)) <=> ALL(c):[c e onlyX <=> c e pre(img(onlyX))]

            U Spec, 174

 

      176  [onlyX=pre(img(onlyX)) => ALL(c):[c e onlyX <=> c e pre(img(onlyX))]]

          & [ALL(c):[c e onlyX <=> c e pre(img(onlyX))] => onlyX=pre(img(onlyX))]

            Iff-And, 175

 

      177  onlyX=pre(img(onlyX)) => ALL(c):[c e onlyX <=> c e pre(img(onlyX))]

            Split, 176

 

      178  ALL(c):[c e onlyX <=> c e pre(img(onlyX))] => onlyX=pre(img(onlyX))

            Split, 176

 

      179  ~ALL(c):[c e onlyX <=> c e pre(img(onlyX))] => ~onlyX=pre(img(onlyX))

            Contra, 177

 

      180  ~~EXIST(c):~[c e onlyX <=> c e pre(img(onlyX))] => ~onlyX=pre(img(onlyX))

            Quant, 179

 

      181  EXIST(c):~[c e onlyX <=> c e pre(img(onlyX))] => ~onlyX=pre(img(onlyX))

            Rem DNeg, 180

 

      182  EXIST(c):~[[c e onlyX => c e pre(img(onlyX))]

          & [c e pre(img(onlyX)) => c e onlyX]] => ~onlyX=pre(img(onlyX))

            Iff-And, 181

 

      183  EXIST(c):~~[~[c e onlyX => c e pre(img(onlyX))] | ~[c e pre(img(onlyX)) => c e onlyX]] => ~onlyX=pre(img(onlyX))

            DeMorgan, 182

 

      184  EXIST(c):[~[c e onlyX => c e pre(img(onlyX))] | ~[c e pre(img(onlyX)) => c e onlyX]] => ~onlyX=pre(img(onlyX))

            Rem DNeg, 183

 

      185  EXIST(c):[~~[c e onlyX & ~c e pre(img(onlyX))] | ~[c e pre(img(onlyX)) => c e onlyX]] => ~onlyX=pre(img(onlyX))

            Imply-And, 184

 

      186  EXIST(c):[c e onlyX & ~c e pre(img(onlyX)) | ~[c e pre(img(onlyX)) => c e onlyX]] => ~onlyX=pre(img(onlyX))

            Rem DNeg, 185

 

      187  EXIST(c):[c e onlyX & ~c e pre(img(onlyX)) | ~~[c e pre(img(onlyX)) & ~c e onlyX]] => ~onlyX=pre(img(onlyX))

            Imply-And, 186

 

     Sufficient: For ~onlyX=pre(img(onlyX))

 

      188  EXIST(c):[c e onlyX & ~c e pre(img(onlyX)) | c e pre(img(onlyX)) & ~c e onlyX] => ~onlyX=pre(img(onlyX))

            Rem DNeg, 187

 

     Apply definition of onlyX

 

      189  y e onlyX <=> y e sA & y=x

            U Spec, 129

 

      190  [y e onlyX => y e sA & y=x]

          & [y e sA & y=x => y e onlyX]

            Iff-And, 189

 

      191  y e onlyX => y e sA & y=x

            Split, 190

 

      192  y e sA & y=x => y e onlyX

            Split, 190

 

      193  ~[y e sA & y=x] => ~y e onlyX

            Contra, 191

 

      194  ~~[~y e sA | ~y=x] => ~y e onlyX

            DeMorgan, 193

 

      195  ~y e sA | ~y=x => ~y e onlyX

            Rem DNeg, 194

 

      196  ~y=x

            Sym, 125

 

      197  ~y e sA | ~y=x

            Arb Or, 196

 

      198  ~y e onlyX

            Detach, 195, 197

 

      199  y e pre(img(onlyX)) & ~y e onlyX

            Join, 173, 198

 

      200  y e onlyX & ~y e pre(img(onlyX)) | y e pre(img(onlyX)) & ~y e onlyX

            Arb Or, 199

 

      201  EXIST(c):[c e onlyX & ~c e pre(img(onlyX)) | c e pre(img(onlyX)) & ~c e onlyX]

            E Gen, 200

 

      202  ~onlyX=pre(img(onlyX))

            Detach, 188, 201

 

      203  Subset(onlyX,sA) & ~onlyX=pre(img(onlyX))

            Join, 143, 202

 

      204  EXIST(a):[Subset(a,sA) & ~a=pre(img(a))]

            E Gen, 203

 

      205  ~ALL(a):~[Subset(a,sA) & ~a=pre(img(a))]

            Quant, 204

 

      206  ~ALL(a):~~[Subset(a,sA) => ~~a=pre(img(a))]

            Imply-And, 205

 

      207  ~ALL(a):[Subset(a,sA) => ~~a=pre(img(a))]

            Rem DNeg, 206

 

      208  ~ALL(a):[Subset(a,sA) => a=pre(img(a))]

            Rem DNeg, 207

 

As Required:

 

209  ~FOnto => ~ALL(a):[Subset(a,sA) => a=pre(img(a))]

      4 Conclusion, 105

 

210  ~~ALL(a):[Subset(a,sA) => a=pre(img(a))] => ~~FOnto

      Contra, 209

 

211  ALL(a):[Subset(a,sA) => a=pre(img(a))] => ~~FOnto

      Rem DNeg, 210

 

212  ALL(a):[Subset(a,sA) => a=pre(img(a))] => FOnto

      Rem DNeg, 211

 

213  [ALL(a):[Subset(a,sA) => a=pre(img(a))] => FOnto]

     & [FOnto => ALL(a):[Subset(a,sA) => a=pre(img(a))]]

      Join, 212, 104

 

As Required:

 

214  ALL(a):[Subset(a,sA) => a=pre(img(a))] <=> FOnto

      Iff-And, 213