THEOREM   The Knaster Fixed-Point Theorem

*******

 

  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]]

 

 

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

 

 

DEFINITIONS/PREVIOUS RESULTS

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

 

Define: Subset

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

 

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

      Axiom

 

 

Set equality theorem (previous result)

 

2     ALL(a):ALL(b):[Set(a) & Set(b) => [a=b <=> Subset(a,b) & Subset(b,a)]]

      Axiom

 

    

     PROOF

     *****

    

     Suppose...

 

      3     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))]]

            Premise

 

      4     Set(s)

            Split, 3

 

    

     Define: ps  (the power set of s)

     **********

 

      5     Set(ps)

            Split, 3

 

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

            Split, 3

 

    

     Define: f  (a function mapping ps to itself)

     *********

 

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

            Split, 3

 

     f preserves the subset relation

 

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

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

            Split, 3

 

      9     EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e ps & Subset(a,f(a))]]

            Subset, 5

 

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

            E Spec, 9

 

    

     Define: z

     *********

    

     z is the family of all subsets A of s that are such that A is a subset of f(A)

 

      11    Set(z)

            Split, 10

 

      12    ALL(a):[a e z <=> a e ps & Subset(a,f(a))]

            Split, 10

 

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

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

            Arb Union

 

      14    Set(z) & ALL(a):[a e z => Set(a)]

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

            U Spec, 13

 

         

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

         

          Suppose...

 

            15    p e z

                  Premise

 

          Apply definition of z

 

            16    p e z <=> p e ps & Subset(p,f(p))

                  U Spec, 12

 

            17    [p e z => p e ps & Subset(p,f(p))]

              & [p e ps & Subset(p,f(p)) => p e z]

                  Iff-And, 16

 

            18    p e z => p e ps & Subset(p,f(p))

                  Split, 17

 

            19    p e ps & Subset(p,f(p)) => p e z

                  Split, 17

 

            20    p e ps & Subset(p,f(p))

                  Detach, 18, 15

 

            21    p e ps

                  Split, 20

 

            22    Subset(p,f(p))

                  Split, 20

 

            23    p e ps <=> Set(p) & Subset(p,s)

                  U Spec, 6

 

            24    [p e ps => Set(p) & Subset(p,s)]

              & [Set(p) & Subset(p,s) => p e ps]

                  Iff-And, 23

 

            25    p e ps => Set(p) & Subset(p,s)

                  Split, 24

 

            26    Set(p) & Subset(p,s) => p e ps

                  Split, 24

 

            27    Set(p) & Subset(p,s)

                  Detach, 25, 21

 

            28    Set(p)

                  Split, 27

 

     As Required:

 

      29    ALL(a):[a e z => Set(a)]

            4 Conclusion, 15

 

      30    Set(z) & ALL(a):[a e z => Set(a)]

            Join, 11, 29

 

      31    EXIST(a):[Set(a) & ALL(b):[b e a <=> EXIST(c):[c e z & b e c]]]

            Detach, 14, 30

 

      32    Set(x) & ALL(b):[b e x <=> EXIST(c):[c e z & b e c]]

            E Spec, 31

 

    

     Define: x  (the union of z)

     *********

 

      33    Set(x)

            Split, 32

 

      34    ALL(b):[b e x <=> EXIST(c):[c e z & b e c]]

            Split, 32

 

         

          Prove: ALL(a):[a e z

                 => Subset(a,x) & Subset(a,f(a)) & Subset(f(a),f(x))]

         

          Suppose...

 

            35    p e z

                  Premise

 

          Apply definition of z

 

            36    p e z <=> p e ps & Subset(p,f(p))

                  U Spec, 12

 

            37    [p e z => p e ps & Subset(p,f(p))]

              & [p e ps & Subset(p,f(p)) => p e z]

                  Iff-And, 36

 

            38    p e z => p e ps & Subset(p,f(p))

                  Split, 37

 

            39    p e ps & Subset(p,f(p)) => p e z

                  Split, 37

 

            40    p e ps & Subset(p,f(p))

                  Detach, 38, 35

 

            41    p e ps

                  Split, 40

 

            42    Subset(p,f(p))

                  Split, 40

 

          Apply definition of Subset

 

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

                  U Spec, 1

 

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

                  U Spec, 43

 

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

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

                  Iff-And, 44

 

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

                  Split, 45

 

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

                  Split, 45

 

             

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

             

              Suppose...

 

                  48    q e p

                        Premise

 

              Apply definition of x

 

                  49    q e x <=> EXIST(c):[c e z & q e c]

                        U Spec, 34

 

                  50    [q e x => EXIST(c):[c e z & q e c]]

                   & [EXIST(c):[c e z & q e c] => q e x]

                        Iff-And, 49

 

                  51    q e x => EXIST(c):[c e z & q e c]

                        Split, 50

 

                  52    EXIST(c):[c e z & q e c] => q e x

                        Split, 50

 

                  53    p e z & q e p

                        Join, 35, 48

 

                  54    EXIST(c):[c e z & q e c]

                        E Gen, 53

 

                  55    q e x

                        Detach, 52, 54

 

          As Required:

 

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

                  4 Conclusion, 48

 

            57    Subset(p,x)

                  Detach, 47, 56

 

          Apply premise

 

            58    ALL(b):[p e ps & b e ps

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

                  U Spec, 8

 

            59    p e ps & x e ps

              => [Subset(p,x) => Subset(f(p),f(x))]

                  U Spec, 58

 

          Apply definition of ps

 

            60    x e ps <=> Set(x) & Subset(x,s)

                  U Spec, 6

 

            61    [x e ps => Set(x) & Subset(x,s)]

              & [Set(x) & Subset(x,s) => x e ps]

                  Iff-And, 60

 

            62    x e ps => Set(x) & Subset(x,s)

                  Split, 61

 

            63    Set(x) & Subset(x,s) => x e ps

                  Split, 61

 

          Apply definition of Subset

 

            64    ALL(b):[Subset(x,b) <=> ALL(c):[c e x => c e b]]

                  U Spec, 1

 

            65    Subset(x,s) <=> ALL(c):[c e x => c e s]

                  U Spec, 64

 

            66    [Subset(x,s) => ALL(c):[c e x => c e s]]

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

                  Iff-And, 65

 

            67    Subset(x,s) => ALL(c):[c e x => c e s]

                  Split, 66

 

            68    ALL(c):[c e x => c e s] => Subset(x,s)

                  Split, 66

 

             

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

             

              Suppose...

 

                  69    q e x

                        Premise

 

              Apply definition of x

 

                  70    q e x <=> EXIST(c):[c e z & q e c]

                        U Spec, 34

 

                  71    [q e x => EXIST(c):[c e z & q e c]]

                   & [EXIST(c):[c e z & q e c] => q e x]

                        Iff-And, 70

 

                  72    q e x => EXIST(c):[c e z & q e c]

                        Split, 71

 

                  73    EXIST(c):[c e z & q e c] => q e x

                        Split, 71

 

                  74    EXIST(c):[c e z & q e c]

                        Detach, 72, 69

 

                  75    r e z & q e r

                        E Spec, 74

 

                  76    r e z

                        Split, 75

 

                  77    q e r

                        Split, 75

 

              Apply definition of z

 

                  78    r e z <=> r e ps & Subset(r,f(r))

                        U Spec, 12

 

                  79    [r e z => r e ps & Subset(r,f(r))]

                   & [r e ps & Subset(r,f(r)) => r e z]

                        Iff-And, 78

 

                  80    r e z => r e ps & Subset(r,f(r))

                        Split, 79

 

                  81    r e ps & Subset(r,f(r)) => r e z

                        Split, 79

 

                  82    r e ps & Subset(r,f(r))

                        Detach, 80, 76

 

                  83    r e ps

                        Split, 82

 

                  84    Subset(r,f(r))

                        Split, 82

 

              Apply definition of ps

 

                  85    r e ps <=> Set(r) & Subset(r,s)

                        U Spec, 6

 

                  86    [r e ps => Set(r) & Subset(r,s)]

                   & [Set(r) & Subset(r,s) => r e ps]

                        Iff-And, 85

 

                  87    r e ps => Set(r) & Subset(r,s)

                        Split, 86

 

                  88    Set(r) & Subset(r,s) => r e ps

                        Split, 86

 

                  89    Set(r) & Subset(r,s)

                        Detach, 87, 83

 

                  90    Set(r)

                        Split, 89

 

                  91    Subset(r,s)

                        Split, 89

 

              Apply definition of Subset

 

                  92    ALL(b):[Subset(r,b) <=> ALL(c):[c e r => c e b]]

                        U Spec, 1

 

                  93    Subset(r,s) <=> ALL(c):[c e r => c e s]

                        U Spec, 92

 

                  94    [Subset(r,s) => ALL(c):[c e r => c e s]]

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

                        Iff-And, 93

 

                  95    Subset(r,s) => ALL(c):[c e r => c e s]

                        Split, 94

 

                  96    ALL(c):[c e r => c e s] => Subset(r,s)

                        Split, 94

 

                  97    ALL(c):[c e r => c e s]

                        Detach, 95, 91

 

                  98    q e r => q e s

                        U Spec, 97

 

                  99    q e s

                        Detach, 98, 77

 

          As Required:

 

            100  ALL(c):[c e x => c e s]

                  4 Conclusion, 69

 

            101  Subset(x,s)

                  Detach, 68, 100

 

            102  Set(x) & Subset(x,s)

                  Join, 33, 101

 

            103  x e ps

                  Detach, 63, 102

 

            104  p e ps & x e ps

                  Join, 41, 103

 

            105  Subset(p,x) => Subset(f(p),f(x))

                  Detach, 59, 104

 

            106  Subset(f(p),f(x))

                  Detach, 105, 57

 

            107  Subset(p,x) & Subset(p,f(p))

                  Join, 57, 42

 

            108  Subset(p,x) & Subset(p,f(p)) & Subset(f(p),f(x))

                  Join, 107, 106

 

     As Required:

 

      109  ALL(a):[a e z

          => Subset(a,x) & Subset(a,f(a)) & Subset(f(a),f(x))]

            4 Conclusion, 35

 

     Apply definition of Subset

 

      110  ALL(b):[Subset(x,b) <=> ALL(c):[c e x => c e b]]

            U Spec, 1

 

      111  Subset(x,f(x)) <=> ALL(c):[c e x => c e f(x)]

            U Spec, 110

 

      112  [Subset(x,f(x)) => ALL(c):[c e x => c e f(x)]]

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

            Iff-And, 111

 

      113  Subset(x,f(x)) => ALL(c):[c e x => c e f(x)]

            Split, 112

 

    

     Sufficient: For Subset(x,f(x))

 

      114  ALL(c):[c e x => c e f(x)] => Subset(x,f(x))

            Split, 112

 

         

          Prove: ALL(c):[c e x => c e f(x)]

         

          Suppose...

 

            115  p e x

                  Premise

 

          Apply definition of x

 

            116  p e x <=> EXIST(c):[c e z & p e c]

                  U Spec, 34

 

            117  [p e x => EXIST(c):[c e z & p e c]]

              & [EXIST(c):[c e z & p e c] => p e x]

                  Iff-And, 116

 

            118  p e x => EXIST(c):[c e z & p e c]

                  Split, 117

 

            119  EXIST(c):[c e z & p e c] => p e x

                  Split, 117

 

            120  EXIST(c):[c e z & p e c]

                  Detach, 118, 115

 

            121  q e z & p e q

                  E Spec, 120

 

          From definition of x, we have q such that...

 

            122  q e z

                  Split, 121

 

            123  p e q

                  Split, 121

 

            124  q e z

              => Subset(q,x) & Subset(q,f(q)) & Subset(f(q),f(x))

                  U Spec, 109

 

            125  Subset(q,x) & Subset(q,f(q)) & Subset(f(q),f(x))

                  Detach, 124, 122

 

          From previous result...

 

            126  Subset(q,x)

                  Split, 125

 

            127  Subset(q,f(q))

                  Split, 125

 

            128  Subset(f(q),f(x))

                  Split, 125

 

          Apply definition of Subset

 

            129  ALL(b):[Subset(q,b) <=> ALL(c):[c e q => c e b]]

                  U Spec, 1

 

            130  Subset(q,f(q)) <=> ALL(c):[c e q => c e f(q)]

                  U Spec, 129

 

            131  [Subset(q,f(q)) => ALL(c):[c e q => c e f(q)]]

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

                  Iff-And, 130

 

            132  Subset(q,f(q)) => ALL(c):[c e q => c e f(q)]

                  Split, 131

 

            133  ALL(c):[c e q => c e f(q)] => Subset(q,f(q))

                  Split, 131

 

            134  ALL(c):[c e q => c e f(q)]

                  Detach, 132, 127

 

            135  p e q => p e f(q)

                  U Spec, 134

 

            136  p e f(q)

                  Detach, 135, 123

 

          Apply definition of Subset

 

            137  ALL(b):[Subset(f(q),b) <=> ALL(c):[c e f(q) => c e b]]

                  U Spec, 1

 

            138  Subset(f(q),f(x)) <=> ALL(c):[c e f(q) => c e f(x)]

                  U Spec, 137

 

            139  [Subset(f(q),f(x)) => ALL(c):[c e f(q) => c e f(x)]]

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

                  Iff-And, 138

 

            140  Subset(f(q),f(x)) => ALL(c):[c e f(q) => c e f(x)]

                  Split, 139

 

            141  ALL(c):[c e f(q) => c e f(x)] => Subset(f(q),f(x))

                  Split, 139

 

            142  ALL(c):[c e f(q) => c e f(x)]

                  Detach, 140, 128

 

            143  p e f(q) => p e f(x)

                  U Spec, 142

 

            144  p e f(x)

                  Detach, 143, 136

 

     As Required:

 

      145  ALL(c):[c e x => c e f(x)]

            4 Conclusion, 115

 

      146  Subset(x,f(x))

            Detach, 114, 145

 

     Apply premise

 

      147  ALL(b):[x e ps & b e ps

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

            U Spec, 8

 

      148  x e ps & f(x) e ps

          => [Subset(x,f(x)) => Subset(f(x),f(f(x)))]

            U Spec, 147

 

      149  x e ps <=> Set(x) & Subset(x,s)

            U Spec, 6

 

      150  [x e ps => Set(x) & Subset(x,s)]

          & [Set(x) & Subset(x,s) => x e ps]

            Iff-And, 149

 

      151  x e ps => Set(x) & Subset(x,s)

            Split, 150

 

      152  Set(x) & Subset(x,s) => x e ps

            Split, 150

 

     Apply definition of Subset

 

      153  ALL(b):[Subset(x,b) <=> ALL(c):[c e x => c e b]]

            U Spec, 1

 

      154  Subset(x,s) <=> ALL(c):[c e x => c e s]

            U Spec, 153

 

      155  [Subset(x,s) => ALL(c):[c e x => c e s]]

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

            Iff-And, 154

 

      156  Subset(x,s) => ALL(c):[c e x => c e s]

            Split, 155

 

      157  ALL(c):[c e x => c e s] => Subset(x,s)

            Split, 155

 

         

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

         

          Suppose...

 

            158  p e x

                  Premise

 

          Apply definition of x

 

            159  p e x <=> EXIST(c):[c e z & p e c]

                  U Spec, 34

 

            160  [p e x => EXIST(c):[c e z & p e c]]

              & [EXIST(c):[c e z & p e c] => p e x]

                  Iff-And, 159

 

            161  p e x => EXIST(c):[c e z & p e c]

                  Split, 160

 

            162  EXIST(c):[c e z & p e c] => p e x

                  Split, 160

 

            163  EXIST(c):[c e z & p e c]

                  Detach, 161, 158

 

            164  q e z & p e q

                  E Spec, 163

 

            165  q e z

                  Split, 164

 

            166  p e q

                  Split, 164

 

          Apply definition of z

 

            167  q e z <=> q e ps & Subset(q,f(q))

                  U Spec, 12

 

            168  [q e z => q e ps & Subset(q,f(q))]

              & [q e ps & Subset(q,f(q)) => q e z]

                  Iff-And, 167

 

            169  q e z => q e ps & Subset(q,f(q))

                  Split, 168

 

            170  q e ps & Subset(q,f(q)) => q e z

                  Split, 168

 

            171  q e ps & Subset(q,f(q))

                  Detach, 169, 165

 

            172  q e ps

                  Split, 171

 

            173  Subset(q,f(q))

                  Split, 171

 

          Apply definition of ps

 

            174  q e ps <=> Set(q) & Subset(q,s)

                  U Spec, 6

 

            175  [q e ps => Set(q) & Subset(q,s)]

              & [Set(q) & Subset(q,s) => q e ps]

                  Iff-And, 174

 

            176  q e ps => Set(q) & Subset(q,s)

                  Split, 175

 

            177  Set(q) & Subset(q,s) => q e ps

                  Split, 175

 

            178  Set(q) & Subset(q,s)

                  Detach, 176, 172

 

            179  Set(q)

                  Split, 178

 

            180  Subset(q,s)

                  Split, 178

 

          Apply definition of Subset

 

            181  ALL(b):[Subset(q,b) <=> ALL(c):[c e q => c e b]]

                  U Spec, 1

 

            182  Subset(q,s) <=> ALL(c):[c e q => c e s]

                  U Spec, 181

 

            183  [Subset(q,s) => ALL(c):[c e q => c e s]]

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

                  Iff-And, 182

 

            184  Subset(q,s) => ALL(c):[c e q => c e s]

                  Split, 183

 

            185  ALL(c):[c e q => c e s] => Subset(q,s)

                  Split, 183

 

            186  ALL(c):[c e q => c e s]

                  Detach, 184, 180

 

            187  p e q => p e s

                  U Spec, 186

 

            188  p e s

                  Detach, 187, 166

 

     As Required:

 

      189  ALL(c):[c e x => c e s]

            4 Conclusion, 158

 

      190  Subset(x,s)

            Detach, 157, 189

 

      191  Set(x) & Subset(x,s)

            Join, 33, 190

 

      192  x e ps

            Detach, 152, 191

 

     Apply definition of ps

 

      193  f(x) e ps <=> Set(f(x)) & Subset(f(x),s)

            U Spec, 6

 

      194  [f(x) e ps => Set(f(x)) & Subset(f(x),s)]

          & [Set(f(x)) & Subset(f(x),s) => f(x) e ps]

            Iff-And, 193

 

      195  f(x) e ps => Set(f(x)) & Subset(f(x),s)

            Split, 194

 

      196  Set(f(x)) & Subset(f(x),s) => f(x) e ps

            Split, 194

 

      197  x e ps => f(x) e ps

            U Spec, 7

 

      198  f(x) e ps

            Detach, 197, 192

 

      199  f(x) e ps <=> Set(f(x)) & Subset(f(x),s)

            U Spec, 6

 

      200  [f(x) e ps => Set(f(x)) & Subset(f(x),s)]

          & [Set(f(x)) & Subset(f(x),s) => f(x) e ps]

            Iff-And, 199

 

      201  f(x) e ps => Set(f(x)) & Subset(f(x),s)

            Split, 200

 

      202  Set(f(x)) & Subset(f(x),s) => f(x) e ps

            Split, 200

 

      203  Set(f(x)) & Subset(f(x),s)

            Detach, 201, 198

 

      204  Set(f(x))

            Split, 203

 

      205  Subset(f(x),s)

            Split, 203

 

      206  f(x) e ps

            Detach, 196, 203

 

      207  x e ps & f(x) e ps

            Join, 192, 206

 

      208  Subset(x,f(x)) => Subset(f(x),f(f(x)))

            Detach, 148, 207

 

      209  Subset(f(x),f(f(x)))

            Detach, 208, 146

 

      210  f(x) e z <=> f(x) e ps & Subset(f(x),f(f(x)))

            U Spec, 12

 

      211  [f(x) e z => f(x) e ps & Subset(f(x),f(f(x)))]

          & [f(x) e ps & Subset(f(x),f(f(x))) => f(x) e z]

            Iff-And, 210

 

      212  f(x) e z => f(x) e ps & Subset(f(x),f(f(x)))

            Split, 211

 

      213  f(x) e ps & Subset(f(x),f(f(x))) => f(x) e z

            Split, 211

 

      214  f(x) e ps & Subset(f(x),f(f(x)))

            Join, 206, 209

 

      215  f(x) e z

            Detach, 213, 214

 

     Apply definition of Subset

 

      216  ALL(b):[Subset(f(x),b) <=> ALL(c):[c e f(x) => c e b]]

            U Spec, 1

 

      217  Subset(f(x),x) <=> ALL(c):[c e f(x) => c e x]

            U Spec, 216

 

      218  [Subset(f(x),x) => ALL(c):[c e f(x) => c e x]]

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

            Iff-And, 217

 

      219  Subset(f(x),x) => ALL(c):[c e f(x) => c e x]

            Split, 218

 

      220  ALL(c):[c e f(x) => c e x] => Subset(f(x),x)

            Split, 218

 

         

          Prove: ALL(c):[c e f(x) => c e x]

         

          Suppose...

 

            221  p e f(x)

                  Premise

 

          Apply definition of x

 

            222  p e x <=> EXIST(c):[c e z & p e c]

                  U Spec, 34

 

            223  [p e x => EXIST(c):[c e z & p e c]]

              & [EXIST(c):[c e z & p e c] => p e x]

                  Iff-And, 222

 

            224  p e x => EXIST(c):[c e z & p e c]

                  Split, 223

 

          Sufficient: For p e x

 

            225  EXIST(c):[c e z & p e c] => p e x

                  Split, 223

 

            226  f(x) e z & p e f(x)

                  Join, 215, 221

 

            227  EXIST(c):[c e z & p e c]

                  E Gen, 226

 

            228  p e x

                  Detach, 225, 227

 

     As Required:

 

      229  ALL(c):[c e f(x) => c e x]

            4 Conclusion, 221

 

      230  Subset(f(x),x)

            Detach, 220, 229

 

     Apply previous result

 

      231  ALL(b):[Set(f(x)) & Set(b) => [f(x)=b <=> Subset(f(x),b) & Subset(b,f(x))]]

            U Spec, 2

 

      232  Set(f(x)) & Set(x) => [f(x)=x <=> Subset(f(x),x) & Subset(x,f(x))]

            U Spec, 231

 

      233  Set(f(x)) & Set(x)

            Join, 204, 33

 

      234  f(x)=x <=> Subset(f(x),x) & Subset(x,f(x))

            Detach, 232, 233

 

      235  [f(x)=x => Subset(f(x),x) & Subset(x,f(x))]

          & [Subset(f(x),x) & Subset(x,f(x)) => f(x)=x]

            Iff-And, 234

 

      236  f(x)=x => Subset(f(x),x) & Subset(x,f(x))

            Split, 235

 

      237  Subset(f(x),x) & Subset(x,f(x)) => f(x)=x

            Split, 235

 

      238  Subset(f(x),x) & Subset(x,f(x))

            Join, 230, 146

 

      239  f(x)=x

            Detach, 237, 238

 

      240  Set(x) & Subset(x,s) & f(x)=x

            Join, 191, 239

 

As Required:

 

241  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]]

      4 Conclusion, 3