THEOREM

*******

 

  ALL(s):[Set(s) => EXIST(a):EXIST(b):[Set(a) & Set(b) & a e b & ~ALL(c):[c e a => c e b]]]

 

 

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

 

    

     PROOF

     *****

    

     Suppose...

 

      1     Set(s)

            Premise

 

     Construct null

    

     Apply Subset Axiom

 

      2     EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e s & ~a e s]]

            Subset, 1

 

      3     Set(null) & ALL(a):[a e null <=> a e s & ~a e s]

            E Spec, 2

 

     Define: Null

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

 

      4     Set(null)

            Split, 3

 

      5     ALL(a):[a e null <=> a e s & ~a e s]

            Split, 3

 

         

          Prove: ~EXIST(a):a e null

         

          Suppose to the contrary...

 

            6     x e null

                  Premise

 

          Apply definition of null

 

            7     x e null <=> x e s & ~x e s

                  U Spec, 5

 

            8     [x e null => x e s & ~x e s]

              & [x e s & ~x e s => x e null]

                  Iff-And, 7

 

            9     x e null => x e s & ~x e s

                  Split, 8

 

            10    x e s & ~x e s => x e null

                  Split, 8

 

            11    x e s & ~x e s

                  Detach, 9, 6

 

     As Required:

 

      12    ~EXIST(a):a e null

            4 Conclusion, 6

 

      13    ~~ALL(a):~a e null

            Quant, 12

 

    

     As Required:

 

      14    ALL(a):~a e null

            Rem DNeg, 13

 

     Construct ps

    

     Apply Power Set Axiom

 

      15    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

 

      16    Set(s) => EXIST(b):[Set(b)

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

            U Spec, 15

 

      17    EXIST(b):[Set(b)

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

            Detach, 16, 1

 

      18    Set(ps)

          & ALL(c):[c e ps <=> Set(c) & ALL(d):[d e c => d e s]]

            E Spec, 17

 

    

     Define: ps   (power set of s)

     **********

 

      19    Set(ps)

            Split, 18

 

      20    ALL(c):[c e ps <=> Set(c) & ALL(d):[d e c => d e s]]

            Split, 18

 

     Construct t

    

     Apply Subset Axiom

 

      21    EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e ps & a=null]]

            Subset, 19

 

      22    Set(t) & ALL(a):[a e t <=> a e ps & a=null]

            E Spec, 21

 

    

     Define: t    

     *********

 

      23    Set(t)

            Split, 22

 

      24    ALL(a):[a e t <=> a e ps & a=null]

            Split, 22

 

         

          Prove: ALL(a):[a e t <=> a=null]

         

          '=>'

         

          Suppose...

 

            25    x e t

                  Premise

 

          Apply definition of t

 

            26    x e t <=> x e ps & x=null

                  U Spec, 24

 

            27    [x e t => x e ps & x=null] & [x e ps & x=null => x e t]

                  Iff-And, 26

 

            28    x e t => x e ps & x=null

                  Split, 27

 

            29    x e ps & x=null => x e t

                  Split, 27

 

            30    x e ps & x=null

                  Detach, 28, 25

 

            31    x e ps

                  Split, 30

 

            32    x=null

                  Split, 30

 

     As Required:

 

      33    ALL(a):[a e t => a=null]

            4 Conclusion, 25

 

         

          '<='

         

          Suppose...

 

            34    x=null

                  Premise

 

         

          Prove:  x e t

         

          Apply definition of t

 

            35    x e t <=> x e ps & x=null

                  U Spec, 24

 

            36    [x e t => x e ps & x=null] & [x e ps & x=null => x e t]

                  Iff-And, 35

 

            37    x e t => x e ps & x=null

                  Split, 36

 

          Sufficient: For x e t

 

            38    x e ps & x=null => x e t

                  Split, 36

 

         

          Prove: x e ps

         

          Apply definition of ps

 

            39    x e ps <=> Set(x) & ALL(d):[d e x => d e s]

                  U Spec, 20

 

            40    [x e ps => Set(x) & ALL(d):[d e x => d e s]]

              & [Set(x) & ALL(d):[d e x => d e s] => x e ps]

                  Iff-And, 39

 

            41    x e ps => Set(x) & ALL(d):[d e x => d e s]

                  Split, 40

 

          Sufficient: For x e ps

 

            42    Set(x) & ALL(d):[d e x => d e s] => x e ps

                  Split, 40

 

            43    Set(x)

                  Substitute, 34, 4

 

             

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

             

              Suppose...

 

                  44    y e x

                        Premise

 

                  45    y e null

                        Substitute, 34, 44

 

              Apply definition of null

 

                  46    ~y e null

                        U Spec, 14

 

                  47    ~~y e null => y e s

                        Arb Cons, 46

 

                  48    y e null => y e s

                        Rem DNeg, 47

 

                  49    y e s

                        Detach, 48, 45

 

          As Required:

 

            50    ALL(d):[d e x => d e s]

                  4 Conclusion, 44

 

          Joining results

 

            51    Set(x) & ALL(d):[d e x => d e s]

                  Join, 43, 50

 

          As Required:

 

            52    x e ps

                  Detach, 42, 51

 

          Join results

 

            53    x e ps & x=null

                  Join, 52, 34

 

            54    x e t

                  Detach, 38, 53

 

     As Required:

 

      55    ALL(a):[a=null => a e t]

            4 Conclusion, 34

 

     Join results

 

      56    ALL(a):[[a e t => a=null] & [a=null => a e t]]

            Join, 33, 55

 

     As Required:

 

      57    ALL(a):[a e t <=> a=null]

            Iff-And, 56

 

     Construct pps

    

     Apply Power Set Axiom

 

      58    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

 

      59    Set(ps) => EXIST(b):[Set(b)

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

            U Spec, 58

 

      60    EXIST(b):[Set(b)

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

            Detach, 59, 19

 

      61    Set(pps)

          & ALL(c):[c e pps <=> Set(c) & ALL(d):[d e c => d e ps]]

            E Spec, 60

 

    

     Define: pps   (the power set of ps)

     ***********

 

      62    Set(pps)

            Split, 61

 

      63    ALL(c):[c e pps <=> Set(c) & ALL(d):[d e c => d e ps]]

            Split, 61

 

     Construct u

    

     Apply Subset Axiom

 

      64    EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e pps & a=t]]

            Subset, 62

 

      65    Set(u) & ALL(a):[a e u <=> a e pps & a=t]

            E Spec, 64

 

    

     Define: u  

     *********

 

      66    Set(u)

            Split, 65

 

      67    ALL(a):[a e u <=> a e pps & a=t]

            Split, 65

 

         

          Prove: ALL(a):[a e u => a=t]

         

          Suppose...

 

            68    x e u

                  Premise

 

         

          Prove: x=t

         

          Apply definition of u

 

            69    x e u <=> x e pps & x=t

                  U Spec, 67

 

            70    [x e u => x e pps & x=t] & [x e pps & x=t => x e u]

                  Iff-And, 69

 

            71    x e u => x e pps & x=t

                  Split, 70

 

            72    x e pps & x=t => x e u

                  Split, 70

 

            73    x e pps & x=t

                  Detach, 71, 68

 

            74    x e pps

                  Split, 73

 

          As Required:

 

            75    x=t

                  Split, 73

 

     As Required:

 

      76    ALL(a):[a e u => a=t]

            4 Conclusion, 68

 

         

          Prove: ALL(a):[a=t => a e u]

         

          Suppose...

 

            77    x=t

                  Premise

 

         

          Prove: x e u

           

          Apply definition of u

 

            78    x e u <=> x e pps & x=t

                  U Spec, 67

 

            79    [x e u => x e pps & x=t] & [x e pps & x=t => x e u]

                  Iff-And, 78

 

            80    x e u => x e pps & x=t

                  Split, 79

 

          Sufficient: For x e u

 

            81    x e pps & x=t => x e u

                  Split, 79

 

         

          Prove: x e pps

         

          Apply definition of pps

 

            82    x e pps <=> Set(x) & ALL(d):[d e x => d e ps]

                  U Spec, 63

 

            83    [x e pps => Set(x) & ALL(d):[d e x => d e ps]]

              & [Set(x) & ALL(d):[d e x => d e ps] => x e pps]

                  Iff-And, 82

 

            84    x e pps => Set(x) & ALL(d):[d e x => d e ps]

                  Split, 83

 

          Sufficient: For x e pps

 

            85    Set(x) & ALL(d):[d e x => d e ps] => x e pps

                  Split, 83

 

            86    Set(x)

                  Substitute, 77, 23

 

             

              Prove: ALL(d):[d e x => d e ps]

             

              Suppose...

 

                  87    y e x

                        Premise

 

                  88    y e t

                        Substitute, 77, 87

 

             

              Prove: y e ps

             

              Apply definition of t

 

                  89    y e t <=> y e ps & y=null

                        U Spec, 24

 

                  90    [y e t => y e ps & y=null] & [y e ps & y=null => y e t]

                        Iff-And, 89

 

                  91    y e t => y e ps & y=null

                        Split, 90

 

                  92    y e ps & y=null => y e t

                        Split, 90

 

                  93    y e ps & y=null

                        Detach, 91, 88

 

              As Required:

 

                  94    y e ps

                        Split, 93

 

          As Required:

 

            95    ALL(d):[d e x => d e ps]

                  4 Conclusion, 87

 

            96    Set(x) & ALL(d):[d e x => d e ps]

                  Join, 86, 95

 

          As Required:

 

            97    x e pps

                  Detach, 85, 96

 

            98    x e pps & x=t

                  Join, 97, 77

 

          As Required:

 

            99    x e u

                  Detach, 81, 98

 

     As Required:

 

      100  ALL(a):[a=t => a e u]

            4 Conclusion, 77

 

      101  ALL(a):[[a e u => a=t] & [a=t => a e u]]

            Join, 76, 100

 

     As Required:

 

      102  ALL(a):[a e u <=> a=t]

            Iff-And, 101

 

    

     Prove: t e u

    

     Apply definition of u

 

      103  t e u <=> t e pps & t=t

            U Spec, 67

 

      104  [t e u => t e pps & t=t] & [t e pps & t=t => t e u]

            Iff-And, 103

 

      105  t e u => t e pps & t=t

            Split, 104

 

     Sufficient: For t e u

 

      106  t e pps & t=t => t e u

            Split, 104

 

    

     Prove: t e pps

    

     Apply definition of pps

 

      107  t e pps <=> Set(t) & ALL(d):[d e t => d e ps]

            U Spec, 63

 

      108  [t e pps => Set(t) & ALL(d):[d e t => d e ps]]

          & [Set(t) & ALL(d):[d e t => d e ps] => t e pps]

            Iff-And, 107

 

      109  t e pps => Set(t) & ALL(d):[d e t => d e ps]

            Split, 108

 

     Sufficient: For t e pps

 

      110  Set(t) & ALL(d):[d e t => d e ps] => t e pps

            Split, 108

 

         

          Prove: ALL(d):[d e t => d e ps]

         

          Suppose...

 

            111  x e t

                  Premise

 

         

          Prove: x e ps

         

          Apply definition of t

 

            112  x e t <=> x e ps & x=null

                  U Spec, 24

 

            113  [x e t => x e ps & x=null] & [x e ps & x=null => x e t]

                  Iff-And, 112

 

            114  x e t => x e ps & x=null

                  Split, 113

 

            115  x e ps & x=null => x e t

                  Split, 113

 

            116  x e ps & x=null

                  Detach, 114, 111

 

          As Required:

 

            117  x e ps

                  Split, 116

 

     As Required:

 

      118  ALL(d):[d e t => d e ps]

            4 Conclusion, 111

 

      119  Set(t) & ALL(d):[d e t => d e ps]

            Join, 23, 118

 

     As Required:

 

      120  t e pps

            Detach, 110, 119

 

      121  t=t

            Reflex

 

      122  t e pps & t=t

            Join, 120, 121

 

     As Required:

 

      123  t e u

            Detach, 106, 122

 

    

     Prove: null e t

    

     Apply definition of t

 

      124  null e t <=> null e ps & null=null

            U Spec, 24

 

      125  [null e t => null e ps & null=null]

          & [null e ps & null=null => null e t]

            Iff-And, 124

 

      126  null e t => null e ps & null=null

            Split, 125

 

     Sufficient: For null e t

 

      127  null e ps & null=null => null e t

            Split, 125

 

    

     Prove: null e ps

    

     Apply definition of ps

 

      128  null e ps <=> Set(null) & ALL(d):[d e null => d e s]

            U Spec, 20

 

      129  [null e ps => Set(null) & ALL(d):[d e null => d e s]]

          & [Set(null) & ALL(d):[d e null => d e s] => null e ps]

            Iff-And, 128

 

      130  null e ps => Set(null) & ALL(d):[d e null => d e s]

            Split, 129

 

     Sufficient: For null e ps

 

      131  Set(null) & ALL(d):[d e null => d e s] => null e ps

            Split, 129

 

         

          Prove: ALL(d):[d e null => d e s]

         

          Suppose...

 

            132  x e null

                  Premise

 

          Prove: x e s

         

          Apply definition of null

 

            133  ~x e null

                  U Spec, 14

 

            134  ~~x e null => x e s

                  Arb Cons, 133

 

            135  x e null => x e s

                  Rem DNeg, 134

 

          As Required:

 

            136  x e s

                  Detach, 135, 132

 

     As Required:

 

      137  ALL(d):[d e null => d e s]

            4 Conclusion, 132

 

     Join results

 

      138  Set(null) & ALL(d):[d e null => d e s]

            Join, 4, 137

 

     As Required:

 

      139  null e ps

            Detach, 131, 138

 

      140  null=null

            Reflex

 

      141  null e ps & null=null

            Join, 139, 140

 

     As Required:

 

      142  null e t

            Detach, 127, 141

 

    

     Prove: ~null e u

    

     Apply definition of u

 

      143  null e u <=> null e pps & null=t

            U Spec, 67

 

      144  [null e u => null e pps & null=t]

          & [null e pps & null=t => null e u]

            Iff-And, 143

 

      145  null e u => null e pps & null=t

            Split, 144

 

      146  null e pps & null=t => null e u

            Split, 144

 

      147  ~[null e pps & null=t] => ~null e u

            Contra, 145

 

      148  ~~[~null e pps | ~null=t] => ~null e u

            DeMorgan, 147

 

     Sufficient: For ~null e u

 

      149  ~null e pps | ~null=t => ~null e u

            Rem DNeg, 148

 

    

     Prove: ~null=t

    

     Apply Set Equality Axiom

 

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

            Set Equality

 

      151  ALL(b):[Set(null) & Set(b) => [null=b <=> ALL(c):[c e null <=> c e b]]]

            U Spec, 150

 

      152  Set(null) & Set(t) => [null=t <=> ALL(c):[c e null <=> c e t]]

            U Spec, 151

 

      153  Set(null) & Set(t)

            Join, 4, 23

 

      154  null=t <=> ALL(c):[c e null <=> c e t]

            Detach, 152, 153

 

      155  [null=t => ALL(c):[c e null <=> c e t]]

          & [ALL(c):[c e null <=> c e t] => null=t]

            Iff-And, 154

 

      156  null=t => ALL(c):[c e null <=> c e t]

            Split, 155

 

      157  ALL(c):[c e null <=> c e t] => null=t

            Split, 155

 

      158  ~ALL(c):[c e null <=> c e t] => ~null=t

            Contra, 156

 

      159  ~~EXIST(c):~[c e null <=> c e t] => ~null=t

            Quant, 158

 

      160  EXIST(c):~[c e null <=> c e t] => ~null=t

            Rem DNeg, 159

 

      161  EXIST(c):~[[c e null => c e t]

          & [c e t => c e null]] => ~null=t

            Iff-And, 160

 

      162  EXIST(c):~~[~[c e null => c e t] | ~[c e t => c e null]] => ~null=t

            DeMorgan, 161

 

      163  EXIST(c):[~[c e null => c e t] | ~[c e t => c e null]] => ~null=t

            Rem DNeg, 162

 

      164  EXIST(c):[~~[c e null & ~c e t] | ~[c e t => c e null]] => ~null=t

            Imply-And, 163

 

      165  EXIST(c):[c e null & ~c e t | ~[c e t => c e null]] => ~null=t

            Rem DNeg, 164

 

      166  EXIST(c):[c e null & ~c e t | ~~[c e t & ~c e null]] => ~null=t

            Imply-And, 165

 

     Sufficient: For ~null=t

 

      167  EXIST(c):[c e null & ~c e t | c e t & ~c e null] => ~null=t

            Rem DNeg, 166

 

      168  ~null e null

            U Spec, 14

 

      169  null e t & ~null e null

            Join, 142, 168

 

      170  null e null & ~null e t | null e t & ~null e null

            Arb Or, 169

 

     Generalizing...

 

      171  EXIST(c):[c e null & ~c e t | c e t & ~c e null]

            E Gen, 170

 

     As Required:

 

      172  ~null=t

            Detach, 167, 171

 

      173  ~null e pps | ~null=t

            Arb Or, 172

 

      174  ~null e u

            Detach, 149, 173

 

      175  null e t & ~null e u

            Join, 142, 174

 

     Generalizing...

 

      176  EXIST(c):[c e t & ~c e u]

            E Gen, 175

 

      177  ~ALL(c):~[c e t & ~c e u]

            Quant, 176

 

      178  ~ALL(c):~~[c e t => ~~c e u]

            Imply-And, 177

 

      179  ~ALL(c):[c e t => ~~c e u]

            Rem DNeg, 178

 

     As Required:

 

      180  ~ALL(c):[c e t => c e u]

            Rem DNeg, 179

 

      181  Set(t) & Set(u)

            Join, 23, 66

 

      182  Set(t) & Set(u) & t e u

            Join, 181, 123

 

      183  Set(t) & Set(u) & t e u

          & ~ALL(c):[c e t => c e u]

            Join, 182, 180

 

As Required:

 

184  ALL(s):[Set(s)

     => EXIST(a):EXIST(b):[Set(a) & Set(b) & a e b

     & ~ALL(c):[c e a => c e b]]]

      4 Conclusion, 1