THEOREM
*******
ALL(a):ALL(b):[Set(a) & Set(b) => [a=b <=> Subset(a,b) & Subset(b,a)]]
DEFINTIONS
**********
Define: Subset
1 ALL(a):ALL(b):[Subset(a,b) <=> ALL(c):[c e a => c e b]]
Axiom
PROOF
*****
Suppose...
2 Set(x) & Set(y)
Premise
3 Set(x)
Split, 2
4 Set(y)
Split, 2
Apply Set Equality Axiom
5 ALL(a):ALL(b):[Set(a) & Set(b) => [a=b <=> ALL(c):[c e a <=> c e b]]]
Set Equality
6 ALL(b):[Set(x) & Set(b) => [x=b <=> ALL(c):[c e x <=> c e b]]]
U Spec, 5
7 Set(x) & Set(y) => [x=y <=> ALL(c):[c e x <=> c e y]]
U Spec, 6
8 x=y <=> ALL(c):[c e x <=> c e y]
Detach, 7, 2
9 [x=y => ALL(c):[c e x <=> c e y]]
& [ALL(c):[c e x <=> c e y] => x=y]
Iff-And, 8
10 x=y => ALL(c):[c e x <=> c e y]
Split, 9
11 ALL(c):[c e x <=> c e y] => x=y
Split, 9
'=>'
Prove: x=y => Subset(x,y) & Subset(y,x)
Suppose...
12 x=y
Premise
13 ALL(c):[c e x <=> c e y]
Detach, 10, 12
14 ALL(b):[Subset(x,b) <=> ALL(c):[c e x => c e b]]
U Spec, 1
15 Subset(x,y) <=> ALL(c):[c e x => c e y]
U Spec, 14
16 [Subset(x,y) => ALL(c):[c e x => c e y]]
& [ALL(c):[c e x => c e y] => Subset(x,y)]
Iff-And, 15
17 Subset(x,y) => ALL(c):[c e x => c e y]
Split, 16
18 ALL(c):[c e x => c e y] => Subset(x,y)
Split, 16
Prove: ALL(c):[c e x => c e y]
Suppose...
19 p e x
Premise
20 p e x <=> p e y
U Spec, 13
21 [p e x => p e y] & [p e y => p e x]
Iff-And, 20
22 p e x => p e y
Split, 21
23 p e y => p e x
Split, 21
24 p e y
Detach, 22, 19
As Required:
25 ALL(c):[c e x => c e y]
4 Conclusion, 19
26 Subset(x,y)
Detach, 18, 25
27 ALL(b):[Subset(y,b) <=> ALL(c):[c e y => c e b]]
U Spec, 1
28 Subset(y,x) <=> ALL(c):[c e y => c e x]
U Spec, 27
29 [Subset(y,x) => ALL(c):[c e y => c e x]]
& [ALL(c):[c e y => c e x] => Subset(y,x)]
Iff-And, 28
30 Subset(y,x) => ALL(c):[c e y => c e x]
Split, 29
31 ALL(c):[c e y => c e x] => Subset(y,x)
Split, 29
Prove: ALL(c):[c e y => c e x]
Suppose...
32 p e y
Premise
33 p e x <=> p e y
U Spec, 13
34 [p e x => p e y] & [p e y => p e x]
Iff-And, 33
35 p e x => p e y
Split, 34
36 p e y => p e x
Split, 34
37 p e x
Detach, 36, 32
As Required:
38 ALL(c):[c e y => c e x]
4 Conclusion, 32
39 Subset(y,x)
Detach, 31, 38
40 Subset(x,y) & Subset(y,x)
Join, 26, 39
As Required:
41 x=y => Subset(x,y) & Subset(y,x)
4 Conclusion, 12
'<='
Prove: Subset(x,y) & Subset(y,x) => x=y
Suppose...
42 Subset(x,y) & Subset(y,x)
Premise
43 Subset(x,y)
Split, 42
44 Subset(y,x)
Split, 42
Apply defintion of Subset
45 ALL(b):[Subset(x,b) <=> ALL(c):[c e x => c e b]]
U Spec, 1
46 Subset(x,y) <=> ALL(c):[c e x => c e y]
U Spec, 45
47 [Subset(x,y) => ALL(c):[c e x => c e y]]
& [ALL(c):[c e x => c e y] => Subset(x,y)]
Iff-And, 46
48 Subset(x,y) => ALL(c):[c e x => c e y]
Split, 47
49 ALL(c):[c e x => c e y] => Subset(x,y)
Split, 47
50 ALL(c):[c e x => c e y]
Detach, 48, 43
Apply definition of Subset
51 ALL(b):[Subset(y,b) <=> ALL(c):[c e y => c e b]]
U Spec, 1
52 Subset(y,x) <=> ALL(c):[c e y => c e x]
U Spec, 51
53 [Subset(y,x) => ALL(c):[c e y => c e x]]
& [ALL(c):[c e y => c e x] => Subset(y,x)]
Iff-And, 52
54 Subset(y,x) => ALL(c):[c e y => c e x]
Split, 53
55 ALL(c):[c e y => c e x] => Subset(y,x)
Split, 53
56 ALL(c):[c e y => c e x]
Detach, 54, 44
57 ALL(c):[[c e x => c e y] & [c e y => c e x]]
Join, 50, 56
58 ALL(c):[c e x <=> c e y]
Iff-And, 57
59 x=y
Detach, 11, 58
As Required:
60 Subset(x,y) & Subset(y,x) => x=y
4 Conclusion, 42
61 [x=y => Subset(x,y) & Subset(y,x)]
& [Subset(x,y) & Subset(y,x) => x=y]
Join, 41, 60
62 x=y <=> Subset(x,y) & Subset(y,x)
Iff-And, 61
As Required:
63 ALL(a):ALL(b):[Set(a) & Set(b) => [a=b <=> Subset(a,b) & Subset(b,a)]]
4 Conclusion, 2