THEOREM
*******
For every set there exists 3 disjoint subsets on which a trichotomy rule holds. (Notation: '|' = OR-operator)
ALL(s):[Set(s)=> EXIST(t):EXIST(u):EXIST(v):[Set(t) & Set(u) & Set(v)
& ALL(a):[a e t => a e s] <---- Subsets t, u, v of s
& ALL(a):[a e u => a e s]
& ALL(a):[a e v => a e s]
& ALL(a):[a e s
=> [a e t | a e u | a e v] <---- Trichotomy Rule
& ~[a e t & a e u]
& ~[a e t & a e v]
& ~[a e u & a e v]]]]]
Proof uses: t = s and u = v = { }
Dan Christensen
2023-08-03
PROOF
*****
Let s be an arbitrary set
1 Set(s)
Premise
Apply Subset Axiom
2 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e s & a e s]]
Subset, 1
3 Set(t) & ALL(a):[a e t <=> a e s & a e s]
E Spec, 2
Define: t (t=s)
4 Set(t)
Split, 3
5 ALL(a):[a e t <=> a e s & a e s]
Split, 3
Prove: t is a subset of s
Suppose...
6 x e t
Premise
Apply definition of t
7 x e t <=> x e s & x e s
U Spec, 5
8 [x e t => x e s & x e s] & [x e s & x e s => x e t]
Iff-And, 7
9 x e t => x e s & x e s
Split, 8
10 x e s & x e s => x e t
Split, 8
11 x e s & x e s
Detach, 9, 6
12 x e s
Split, 11
As Required:
13 ALL(a):[a e t => a e s]
4 Conclusion, 6
Prove: s is a subset of t
Suppose...
14 x e s
Premise
Apply definition of t
15 x e t <=> x e s & x e s
U Spec, 5
16 [x e t => x e s & x e s] & [x e s & x e s => x e t]
Iff-And, 15
17 x e s & x e s => x e t
Split, 16
18 x e s & x e s
Join, 14, 14
19 x e t
Detach, 17, 18
As Required:
20 ALL(a):[a e s => a e t]
4 Conclusion, 14
Apply Subset Axiom
21 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e s & ~a e s]]
Subset, 1
22 Set(u) & ALL(a):[a e u <=> a e s & ~a e s]
E Spec, 21
Define: u (empty subset of s)
23 Set(u)
Split, 22
24 ALL(a):[a e u <=> a e s & ~a e s]
Split, 22
Prove: u is a subset of s
Suppose...
25 x e u
Premise
Apply defintion of u
26 x e u <=> x e s & ~x e s
U Spec, 24
27 [x e u => x e s & ~x e s] & [x e s & ~x e s => x e u]
Iff-And, 26
28 x e u => x e s & ~x e s
Split, 27
29 x e s & ~x e s
Detach, 28, 25
30 x e s
Split, 29
As Required:
31 ALL(a):[a e u => a e s]
4 Conclusion, 25
Prove: u is empty
Suppose...
32 x e u
Premise
Apply definition of u
33 x e u <=> x e s & ~x e s
U Spec, 24
34 [x e u => x e s & ~x e s] & [x e s & ~x e s => x e u]
Iff-And, 33
35 x e u => x e s & ~x e s
Split, 34
36 x e s & ~x e s
Detach, 35, 32
As Required:
37 ~EXIST(a):a e u
4 Conclusion, 32
38 Set(v) & ALL(a):[a e v <=> a e s & ~a e s]
E Spec, 21
Define: v (empty subset of s)
39 Set(v)
Split, 38
40 ALL(a):[a e v <=> a e s & ~a e s]
Split, 38
Prove: v is a subset of s
Suppose...
41 x e v
Premise
Apply definition of v
42 x e v <=> x e s & ~x e s
U Spec, 40
43 [x e v => x e s & ~x e s] & [x e s & ~x e s => x e v]
Iff-And, 42
44 x e v => x e s & ~x e s
Split, 43
45 x e s & ~x e s
Detach, 44, 41
46 x e s
Split, 45
As Required:
47 ALL(a):[a e v => a e s]
4 Conclusion, 41
Prove: ~EXIST(a):a e v
Suppose to contrary...
48 x e v
Premise
Apply definition of v
49 x e v <=> x e s & ~x e s
U Spec, 40
50 [x e v => x e s & ~x e s] & [x e s & ~x e s => x e v]
Iff-And, 49
51 x e v => x e s & ~x e s
Split, 50
52 x e s & ~x e s
Detach, 51, 48
v is empty
53 ~EXIST(a):a e v
4 Conclusion, 48
Prove: ALL(a):[a e s
=> [a e t | a e u | a e v]
& ~[a e t & a e u]
& ~[a e t & a e v]
& ~[a e u & a e v]]
Suppose...
54 x e s
Premise
55 x e s => x e t
U Spec, 20
56 x e t
Detach, 55, 54
57 x e t | x e u
Arb Or, 56
As Required:
58 x e t | x e u | x e v
Arb Or, 57
Prove: ~[x e t & x e u]
Suppose to the contrary...
59 x e t & x e u
Premise
60 x e u
Split, 59
61 EXIST(a):a e u
E Gen, 60
Obtain contradiction...
62 EXIST(a):a e u & ~EXIST(a):a e u
Join, 61, 37
As Required:
63 ~[x e t & x e u]
4 Conclusion, 59
Prove: ~[x e t & x e v]
Suppose to the contrary...
64 x e t & x e v
Premise
65 x e v
Split, 64
66 EXIST(a):a e v
E Gen, 65
Obtain contradiction...
67 EXIST(a):a e v & ~EXIST(a):a e v
Join, 66, 53
As Required:
68 ~[x e t & x e v]
4 Conclusion, 64
Prove: ~[x e u & x e v]
Suppose to the contrary...
69 x e u & x e v
Premise
70 x e u
Split, 69
71 EXIST(a):a e u
E Gen, 70
Obtain contradiction...
72 ~EXIST(a):a e u & EXIST(a):a e u
Join, 37, 71
As Required:
73 ~[x e u & x e v]
4 Conclusion, 69
Joining results...
74 [x e t | x e u | x e v] & ~[x e t & x e u]
Join, 58, 63
75 [x e t | x e u | x e v] & ~[x e t & x e u]
& ~[x e t & x e v]
Join, 74, 68
76 [x e t | x e u | x e v] & ~[x e t & x e u]
& ~[x e t & x e v]
& ~[x e u & x e v]
Join, 75, 73
As Required:
77 ALL(a):[a e s
=> [a e t | a e u | a e v] & ~[a e t & a e u]
& ~[a e t & a e v]
& ~[a e u & a e v]]
4 Conclusion, 54
Joining results...
78 Set(t) & Set(u)
Join, 4, 23
79 Set(t) & Set(u) & Set(v)
Join, 78, 39
80 Set(t) & Set(u) & Set(v)
& ALL(a):[a e t => a e s]
Join, 79, 13
81 Set(t) & Set(u) & Set(v)
& ALL(a):[a e t => a e s]
& ALL(a):[a e u => a e s]
Join, 80, 31
82 Set(t) & Set(u) & Set(v)
& ALL(a):[a e t => a e s]
& ALL(a):[a e u => a e s]
& ALL(a):[a e v => a e s]
Join, 81, 47
83 Set(t) & Set(u) & Set(v)
& ALL(a):[a e t => a e s]
& ALL(a):[a e u => a e s]
& ALL(a):[a e v => a e s]
& ALL(a):[a e s
=> [a e t | a e u | a e v] & ~[a e t & a e u]
& ~[a e t & a e v]
& ~[a e u & a e v]]
Join, 82, 77
As Required:
84 ALL(s):[Set(s)
=> EXIST(t):EXIST(u):EXIST(v):[Set(t) & Set(u) & Set(v)
& ALL(a):[a e t => a e s]
& ALL(a):[a e u => a e s]
& ALL(a):[a e v => a e s]
& ALL(a):[a e s
=> [a e t | a e u | a e v] & ~[a e t & a e u]
& ~[a e t & a e v]
& ~[a e u & a e v]]]]
4 Conclusion, 1