Theorem:

 

ALL(null):ALL(s):[Set(null)

& ALL(a):~a e null

& Set(s)

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

=> null=s]

 

    

     Proof

     -----

    

     Initial premise

 

      1     Set(null)

          & ALL(a):~a e null

          & Set(s)

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

            Premise

 

     Define: null

 

      2     Set(null)

            Split, 1

 

      3     ALL(a):~a e null

            Split, 1

 

     Define: s

 

      4     Set(s)

            Split, 1

 

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

            Split, 1

 

     Prove: null = s

    

     Apply set equality axiom for null and s.

 

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

            Set Equality

 

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

            U Spec, 6

 

      8     Set(null) & Set(s) => [null=s <=> ALL(c):[c e null <=> c e s]]

            U Spec, 7

 

      9     Set(null) & Set(s)

            Join, 2, 4

 

      10    null=s <=> ALL(c):[c e null <=> c e s]

            Detach, 8, 9

 

      11    [null=s => ALL(c):[c e null <=> c e s]]

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

            Iff-And, 10

 

      12    null=s => ALL(c):[c e null <=> c e s]

            Split, 11

 

     Sufficient: For null=s

 

      13    ALL(c):[c e null <=> c e s] => null=s

            Split, 11

 

         

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

         

          Suppose...

 

            14    x e null

                  Premise

 

          Apply definition of null

 

            15    ~x e null

                  U Spec, 3

 

          Apply arbitrary consequent rule

 

            16    ~~x e null => x e s

                  Arb Cons, 15

 

            17    x e null => x e s

                  Rem DNeg, 16

 

            18    x e s

                  Detach, 17, 14

 

     As Required:

 

      19    ALL(a):[a e null => a e s]

            4 Conclusion, 14

 

         

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

         

          Suppose...

 

            20    x e s

                  Premise

 

          Apply definition of s

 

            21    x e s <=> ~x=x

                  U Spec, 5

 

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

                  Iff-And, 21

 

            23    x e s => ~x=x

                  Split, 22

 

            24    ~x=x => x e s

                  Split, 22

 

            25    ~x=x

                  Detach, 23, 20

 

          Apply arbitrary consequent rule

 

            26    ~~x=x => x e null

                  Arb Cons, 25

 

            27    x=x => x e null

                  Rem DNeg, 26

 

          Apply reflexivity axiom

 

            28    x=x

                  Reflex

 

            29    x e null

                  Detach, 27, 28

 

     As Required:

 

      30    ALL(a):[a e s => a e null]

            4 Conclusion, 20

 

     Joining results...

 

      31    ALL(a):[[a e null => a e s] & [a e s => a e null]]

            Join, 19, 30

 

      32    ALL(a):[a e null <=> a e s]

            Iff-And, 31

 

     As Required:

 

      33    null=s

            Detach, 13, 32

 

As Required:

 

34    ALL(null):ALL(s):[Set(null)

     & ALL(a):~a e null

     & Set(s)

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

     => null=s]

      4 Conclusion, 1