THEOREM

*******

 

    ALL(u):[Set(u) => [EXIST(x):[x e u & [P(x) => ALL(y):[y e u => P(y)]]]

    <=> EXIST(x):x e u]]

 

 

PROOF

*****

 

    By Dan Christensen

 

    This proof was prepared with the aid of, and mechanically verified by the author's

    DC Proof software available at http://www.dcproof.com

 

    

     Let u be an arbitrary set

 

      1     Set(u)

            Premise

 

         

          Suppose u is non-empty

 

            2     EXIST(x):x e u

                  Premise

 

            3     x e u

                  E Spec, 2

 

          2 cases to consider:  (where '|' is the OR-operator)

 

            4     ALL(y):[y e u => P(y)] | ~ALL(y):[y e u => P(y)]

                  Or Not

 

             

              Case 1

             

              Prove: ALL(y):[y e u => P(y)]

                     => EXIST(x):[x e u & [P(x) => ALL(y):[y e u => P(y)]]]

             

              Suppose...

 

                  5     ALL(y):[y e u => P(y)]

                        Premise

 

                  6     P(x) => ALL(y):[y e u => P(y)]

                        Arb Ante, 5

 

                  7     x e u & [P(x) => ALL(y):[y e u => P(y)]]

                        Join, 3, 6

 

                  8     EXIST(x):[x e u & [P(x) => ALL(y):[y e u => P(y)]]]

                        E Gen, 7

 

          Case 1

         

          As Required:

 

            9     ALL(y):[y e u => P(y)]

              => EXIST(x):[x e u & [P(x) => ALL(y):[y e u => P(y)]]]

                  4 Conclusion, 5

 

             

              Case 2

             

              Prove: ~ALL(y):[y e u => P(y)]

                     => EXIST(x):[x e u & [P(x) => ALL(a):[a e u => P(a)]]]

             

              Suppose...

 

                  10    ~ALL(y):[y e u => P(y)]

                        Premise

 

              Switch quantifier

 

                  11    ~~EXIST(y):~[y e u => P(y)]

                        Quant, 10

 

                  12    EXIST(y):~[y e u => P(y)]

                        Rem DNeg, 11

 

                  13    EXIST(y):~~[y e u & ~P(y)]

                        Imply-And, 12

 

                  14    EXIST(y):[y e u & ~P(y)]

                        Rem DNeg, 13

 

                  15    y e u & ~P(y)

                        E Spec, 14

 

                  16    y e u

                        Split, 15

 

                  17    ~P(y)

                        Split, 15

 

                  18    ~P(y) | ALL(a):[a e u => P(a)]

                        Arb Or, 17

 

                  19    y e u & [~P(y) | ALL(a):[a e u => P(a)]]

                        Join, 16, 18

 

                  20    EXIST(x):[x e u & [~P(x) | ALL(a):[a e u => P(a)]]]

                        E Gen, 19

 

                  21    EXIST(x):[x e u & [~~P(x) => ALL(a):[a e u => P(a)]]]

                        Imply-Or, 20

 

                  22    EXIST(x):[x e u & [P(x) => ALL(a):[a e u => P(a)]]]

                        Rem DNeg, 21

 

          Sub-case 2

         

          As Required:

 

            23    ~ALL(y):[y e u => P(y)]

              => EXIST(x):[x e u & [P(x) => ALL(a):[a e u => P(a)]]]

                  4 Conclusion, 10

 

          Joining previous results for Cases Rule

 

            24    [ALL(y):[y e u => P(y)]

              => EXIST(x):[x e u & [P(x) => ALL(y):[y e u => P(y)]]]]

              & [~ALL(y):[y e u => P(y)]

              => EXIST(x):[x e u & [P(x) => ALL(a):[a e u => P(a)]]]]

                  Join, 9, 23

 

          Apply Cases Rule

 

            25    EXIST(x):[x e u & [P(x) => ALL(a):[a e u => P(a)]]]

                  Cases, 4, 24

 

     As Required:

 

      26    EXIST(x):x e u

          => EXIST(x):[x e u & [P(x) => ALL(a):[a e u => P(a)]]]

            4 Conclusion, 2

 

         

          Suppose u is empty

 

            27    ~EXIST(x):x e u

                  Premise

 

          Switch quantifier

 

            28    ~~ALL(x):~x e u

                  Quant, 27

 

            29    ALL(x):~x e u

                  Rem DNeg, 28

 

              Prove: ~EXIST(x):[x e u & [P(x) => ALL(y):[y e u => P(y)]]]

             

              Suppose to the contrary...

 

                  30    EXIST(x):[x e u & [P(x) => ALL(y):[y e u => P(y)]]]

                        Premise

 

                  31    x e u & [P(x) => ALL(y):[y e u => P(y)]]

                        E Spec, 30

 

                  32    x e u

                        Split, 31

 

                  33    P(x) => ALL(y):[y e u => P(y)]

                        Split, 31

 

                  34    ~x e u

                        U Spec, 29

 

              Obtain the contradiction...

 

                  35    x e u & ~x e u

                        Join, 32, 34

 

          As Required:

 

            36    ~EXIST(x):[x e u & [P(x) => ALL(y):[y e u => P(y)]]]

                  4 Conclusion, 30

 

     As Required:

 

      37    ~EXIST(x):x e u

          => ~EXIST(x):[x e u & [P(x) => ALL(y):[y e u => P(y)]]]

            4 Conclusion, 27

 

     Apply Contrapositive Rule

 

      38    ~~EXIST(x):[x e u & [P(x) => ALL(y):[y e u => P(y)]]] => ~~EXIST(x):x e u

            Contra, 37

 

      39    EXIST(x):[x e u & [P(x) => ALL(y):[y e u => P(y)]]] => ~~EXIST(x):x e u

            Rem DNeg, 38

 

     As Required:

 

      40    EXIST(x):[x e u & [P(x) => ALL(y):[y e u => P(y)]]] => EXIST(x):x e u

            Rem DNeg, 39

 

     Joint previous results for Iff-And Rule

 

      41    [EXIST(x):[x e u & [P(x) => ALL(y):[y e u => P(y)]]] => EXIST(x):x e u]

          & [EXIST(x):x e u

          => EXIST(x):[x e u & [P(x) => ALL(a):[a e u => P(a)]]]]

            Join, 40, 26

 

     Apply Iff-And Rule

 

      42    EXIST(x):[x e u & [P(x) => ALL(y):[y e u => P(y)]]]

          <=> EXIST(x):x e u

            Iff-And, 41

 

As Required:

 

43    ALL(u):[Set(u)

     => [EXIST(x):[x e u & [P(x) => ALL(y):[y e u => P(y)]]]

     <=> EXIST(x):x e u]]

      4 Conclusion, 1