THEOREM 4

*********

Let null be an empty set. Let unull be its union. Then unull=null.

This machine-verified formal proof was written with the aid of the author's DC Proof 2.0 available at http://www.dcproof.com

LINKS TO PREVIOUS RESULTS

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

From Theorem 1, we know that every set has an empty subset.

From Theorem 3, we know that every empty set can be expressed

as a family of sets, and that there exists the union of that family.

PROOF

*****

Suppose...

1 Set(null) & ALL(a):~a e null

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

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

Premise

2 Set(null)

Split, 1

3 ALL(a):~a e null

Split, 1

4 ALL(a):[a e null => Set(a)]

Split, 1

5 Set(unull)

Split, 1

6 ALL(b):[b e unull <=> EXIST(c):[c e null & b e c]]

Split, 1

Apply Set Equality Axiom

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

Set Equality

8 ALL(b):[Set(unull) & Set(b) => [unull=b <=> ALL(c):[c e unull <=> c e b]]]

U Spec, 7

9 Set(unull) & Set(null) => [unull=null <=> ALL(c):[c e unull <=> c e null]]

U Spec, 8

10 Set(unull) & Set(null)

Join, 5, 2

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

Detach, 9, 10

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

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

Iff-And, 11

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

Split, 12

Sufficient: For unull=null

14 ALL(c):[c e unull <=> c e null] => unull=null

Split, 12

'=>'

Prove: ALL(c):[c e unull => c e null]

Suppose...

15 x e unull

Premise

Apply definition of unull

16 x e unull <=> EXIST(c):[c e null & x e c]

U Spec, 6

17 [x e unull => EXIST(c):[c e null & x e c]]

& [EXIST(c):[c e null & x e c] => x e unull]

Iff-And, 16

18 x e unull => EXIST(c):[c e null & x e c]

Split, 17

19 EXIST(c):[c e null & x e c] => x e unull

Split, 17

20 EXIST(c):[c e null & x e c]

Detach, 18, 15

21 y e null & x e y

E Spec, 20

22 y e null

Split, 21

23 x e y

Split, 21

Apply definiton of null

24 ~y e null

U Spec, 3

25 ~y e null => x e null

Arb Cons, 22

26 x e null

Detach, 25, 24

As Required:

27 ALL(c):[c e unull => c e null]

4 Conclusion, 15

'<='

Prove: ALL(c):[c e null => c e unull]

Suppose...

28 x e null

Premise

Apply definition of null

29 ~x e null

U Spec, 3

30 ~x e null => x e unull

Arb Cons, 28

31 x e unull

Detach, 30, 29

As Required:

32 ALL(c):[c e null => c e unull]

4 Conclusion, 28

Joining results...

33 ALL(c):[[c e unull => c e null] & [c e null => c e unull]]

Join, 27, 32

34 ALL(c):[c e unull <=> c e null]

Iff-And, 33

As Required:

35 unull=null

Detach, 14, 34

As Required:

36 ALL(null):ALL(unull):[Set(null) & ALL(a):~a e null

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

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

=> unull=null]

4 Conclusion, 1