Quantum Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  QLE Home  >  Th. List  >  ska2 GIF version

Theorem ska2 432
 Description: Soundness theorem for Kalmbach's quantum propositional logic axiom KA2.
Assertion
Ref Expression
ska2 ((ab) ∪ ((bc) ∪ (ac))) = 1

Proof of Theorem ska2
StepHypRef Expression
1 dfnb 95 . . 3 (ab) = ((ab) ∩ (ab ))
2 dfnb 95 . . . 4 (bc) = ((bc) ∩ (bc ))
3 dfb 94 . . . 4 (ac) = ((ac) ∪ (ac ))
42, 32or 72 . . 3 ((bc) ∪ (ac)) = (((bc) ∩ (bc )) ∪ ((ac) ∪ (ac )))
51, 42or 72 . 2 ((ab) ∪ ((bc) ∪ (ac))) = (((ab) ∩ (ab )) ∪ (((bc) ∩ (bc )) ∪ ((ac) ∪ (ac ))))
6 ax-a3 32 . . . 4 ((((ab) ∩ (ab )) ∪ ((bc) ∩ (bc ))) ∪ ((ac) ∪ (ac ))) = (((ab) ∩ (ab )) ∪ (((bc) ∩ (bc )) ∪ ((ac) ∪ (ac ))))
76ax-r1 35 . . 3 (((ab) ∩ (ab )) ∪ (((bc) ∩ (bc )) ∪ ((ac) ∪ (ac )))) = ((((ab) ∩ (ab )) ∪ ((bc) ∩ (bc ))) ∪ ((ac) ∪ (ac )))
8 id 59 . . . 4 ((((ab) ∩ (ab )) ∪ ((bc) ∩ (bc ))) ∪ ((ac) ∪ (ac ))) = ((((ab) ∩ (ab )) ∪ ((bc) ∩ (bc ))) ∪ ((ac) ∪ (ac )))
9 le1 146 . . . . 5 ((((ab) ∩ (ab )) ∪ ((bc) ∩ (bc ))) ∪ ((ac) ∪ (ac ))) ≤ 1
10 ax-a2 31 . . . . . . . . . 10 ((((ab) ∩ a ) ∪ ((b ∩ ((ab) ∪ (bc))) ∪ ((bc) ∩ c ))) ∪ ((ac) ∪ (ac ))) = (((ac) ∪ (ac )) ∪ (((ab) ∩ a ) ∪ ((b ∩ ((ab) ∪ (bc))) ∪ ((bc) ∩ c ))))
11 or12 80 . . . . . . . . . . 11 (((ac) ∪ (ac )) ∪ (((ab) ∩ a ) ∪ ((b ∩ ((ab) ∪ (bc))) ∪ ((bc) ∩ c )))) = (((ab) ∩ a ) ∪ (((ac) ∪ (ac )) ∪ ((b ∩ ((ab) ∪ (bc))) ∪ ((bc) ∩ c ))))
12 or12 80 . . . . . . . . . . . . 13 (((ab) ∩ a ) ∪ ((ac) ∪ (((ac ) ∪ b ) ∪ ((bc) ∩ c )))) = ((ac) ∪ (((ab) ∩ a ) ∪ (((ac ) ∪ b ) ∪ ((bc) ∩ c ))))
13 or12 80 . . . . . . . . . . . . . . . 16 (((ab) ∩ a ) ∪ (((ac ) ∪ b ) ∪ ((bc) ∩ c ))) = (((ac ) ∪ b ) ∪ (((ab) ∩ a ) ∪ ((bc) ∩ c )))
14 ax-a3 32 . . . . . . . . . . . . . . . . 17 (((ac ) ∪ b ) ∪ (((ab) ∩ a ) ∪ ((bc) ∩ c ))) = ((ac ) ∪ (b ∪ (((ab) ∩ a ) ∪ ((bc) ∩ c ))))
15 orordi 112 . . . . . . . . . . . . . . . . . 18 (b ∪ (((ab) ∩ a ) ∪ ((bc) ∩ c ))) = ((b ∪ ((ab) ∩ a )) ∪ (b ∪ ((bc) ∩ c )))
1615lor 70 . . . . . . . . . . . . . . . . 17 ((ac ) ∪ (b ∪ (((ab) ∩ a ) ∪ ((bc) ∩ c )))) = ((ac ) ∪ ((b ∪ ((ab) ∩ a )) ∪ (b ∪ ((bc) ∩ c ))))
1714, 16ax-r2 36 . . . . . . . . . . . . . . . 16 (((ac ) ∪ b ) ∪ (((ab) ∩ a ) ∪ ((bc) ∩ c ))) = ((ac ) ∪ ((b ∪ ((ab) ∩ a )) ∪ (b ∪ ((bc) ∩ c ))))
1813, 17ax-r2 36 . . . . . . . . . . . . . . 15 (((ab) ∩ a ) ∪ (((ac ) ∪ b ) ∪ ((bc) ∩ c ))) = ((ac ) ∪ ((b ∪ ((ab) ∩ a )) ∪ (b ∪ ((bc) ∩ c ))))
1918lor 70 . . . . . . . . . . . . . 14 ((ac) ∪ (((ab) ∩ a ) ∪ (((ac ) ∪ b ) ∪ ((bc) ∩ c )))) = ((ac) ∪ ((ac ) ∪ ((b ∪ ((ab) ∩ a )) ∪ (b ∪ ((bc) ∩ c )))))
20 or12 80 . . . . . . . . . . . . . . . 16 ((ac) ∪ ((ac ) ∪ ((ba ) ∪ (bc )))) = ((ac ) ∪ ((ac) ∪ ((ba ) ∪ (bc ))))
21 le1 146 . . . . . . . . . . . . . . . . 17 ((ac ) ∪ ((ac) ∪ ((ba ) ∪ (bc )))) ≤ 1
22 df-t 41 . . . . . . . . . . . . . . . . . . . 20 1 = ((ac) ∪ (ac) )
23 oran3 93 . . . . . . . . . . . . . . . . . . . . . 22 (ac ) = (ac)
2423lor 70 . . . . . . . . . . . . . . . . . . . . 21 ((ac) ∪ (ac )) = ((ac) ∪ (ac) )
2524ax-r1 35 . . . . . . . . . . . . . . . . . . . 20 ((ac) ∪ (ac) ) = ((ac) ∪ (ac ))
2622, 25ax-r2 36 . . . . . . . . . . . . . . . . . . 19 1 = ((ac) ∪ (ac ))
27 leor 159 . . . . . . . . . . . . . . . . . . . . 21 a ≤ (ba )
28 leor 159 . . . . . . . . . . . . . . . . . . . . 21 c ≤ (bc )
2927, 28le2or 168 . . . . . . . . . . . . . . . . . . . 20 (ac ) ≤ ((ba ) ∪ (bc ))
3029lelor 166 . . . . . . . . . . . . . . . . . . 19 ((ac) ∪ (ac )) ≤ ((ac) ∪ ((ba ) ∪ (bc )))
3126, 30bltr 138 . . . . . . . . . . . . . . . . . 18 1 ≤ ((ac) ∪ ((ba ) ∪ (bc )))
32 leor 159 . . . . . . . . . . . . . . . . . 18 ((ac) ∪ ((ba ) ∪ (bc ))) ≤ ((ac ) ∪ ((ac) ∪ ((ba ) ∪ (bc ))))
3331, 32letr 137 . . . . . . . . . . . . . . . . 17 1 ≤ ((ac ) ∪ ((ac) ∪ ((ba ) ∪ (bc ))))
3421, 33lebi 145 . . . . . . . . . . . . . . . 16 ((ac ) ∪ ((ac) ∪ ((ba ) ∪ (bc )))) = 1
3520, 34ax-r2 36 . . . . . . . . . . . . . . 15 ((ac) ∪ ((ac ) ∪ ((ba ) ∪ (bc )))) = 1
36 wcomorr 412 . . . . . . . . . . . . . . . . . . . . . . 23 C (b, (ba)) = 1
37 ax-a2 31 . . . . . . . . . . . . . . . . . . . . . . . 24 (ba) = (ab)
3837bi1 118 . . . . . . . . . . . . . . . . . . . . . . 23 ((ba) ≡ (ab)) = 1
3936, 38wcbtr 411 . . . . . . . . . . . . . . . . . . . . . 22 C (b, (ab)) = 1
4039wcomcom 414 . . . . . . . . . . . . . . . . . . . . 21 C ((ab), b) = 1
4140wcomcom2 415 . . . . . . . . . . . . . . . . . . . 20 C ((ab), b ) = 1
42 wcomorr 412 . . . . . . . . . . . . . . . . . . . . . 22 C (a, (ab)) = 1
4342wcomcom 414 . . . . . . . . . . . . . . . . . . . . 21 C ((ab), a) = 1
4443wcomcom2 415 . . . . . . . . . . . . . . . . . . . 20 C ((ab), a ) = 1
4541, 44wfh4 426 . . . . . . . . . . . . . . . . . . 19 ((b ∪ ((ab) ∩ a )) ≡ ((b ∪ (ab)) ∩ (ba ))) = 1
46 or12 80 . . . . . . . . . . . . . . . . . . . . . . 23 (b ∪ (ab)) = (a ∪ (bb))
47 ax-a2 31 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (bb) = (bb )
48 df-t 41 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 1 = (bb )
4948ax-r1 35 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (bb ) = 1
5047, 49ax-r2 36 . . . . . . . . . . . . . . . . . . . . . . . . 25 (bb) = 1
5150lor 70 . . . . . . . . . . . . . . . . . . . . . . . 24 (a ∪ (bb)) = (a ∪ 1)
52 or1 104 . . . . . . . . . . . . . . . . . . . . . . . 24 (a ∪ 1) = 1
5351, 52ax-r2 36 . . . . . . . . . . . . . . . . . . . . . . 23 (a ∪ (bb)) = 1
5446, 53ax-r2 36 . . . . . . . . . . . . . . . . . . . . . 22 (b ∪ (ab)) = 1
5554ran 78 . . . . . . . . . . . . . . . . . . . . 21 ((b ∪ (ab)) ∩ (ba )) = (1 ∩ (ba ))
56 ancom 74 . . . . . . . . . . . . . . . . . . . . . 22 (1 ∩ (ba )) = ((ba ) ∩ 1)
57 an1 106 . . . . . . . . . . . . . . . . . . . . . 22 ((ba ) ∩ 1) = (ba )
5856, 57ax-r2 36 . . . . . . . . . . . . . . . . . . . . 21 (1 ∩ (ba )) = (ba )
5955, 58ax-r2 36 . . . . . . . . . . . . . . . . . . . 20 ((b ∪ (ab)) ∩ (ba )) = (ba )
6059bi1 118 . . . . . . . . . . . . . . . . . . 19 (((b ∪ (ab)) ∩ (ba )) ≡ (ba )) = 1
6145, 60wr2 371 . . . . . . . . . . . . . . . . . 18 ((b ∪ ((ab) ∩ a )) ≡ (ba )) = 1
62 wcomorr 412 . . . . . . . . . . . . . . . . . . . . . 22 C (b, (bc)) = 1
6362wcomcom 414 . . . . . . . . . . . . . . . . . . . . 21 C ((bc), b) = 1
6463wcomcom2 415 . . . . . . . . . . . . . . . . . . . 20 C ((bc), b ) = 1
65 wcomorr 412 . . . . . . . . . . . . . . . . . . . . . . 23 C (c, (cb)) = 1
66 ax-a2 31 . . . . . . . . . . . . . . . . . . . . . . . 24 (cb) = (bc)
6766bi1 118 . . . . . . . . . . . . . . . . . . . . . . 23 ((cb) ≡ (bc)) = 1
6865, 67wcbtr 411 . . . . . . . . . . . . . . . . . . . . . 22 C (c, (bc)) = 1
6968wcomcom 414 . . . . . . . . . . . . . . . . . . . . 21 C ((bc), c) = 1
7069wcomcom2 415 . . . . . . . . . . . . . . . . . . . 20 C ((bc), c ) = 1
7164, 70wfh4 426 . . . . . . . . . . . . . . . . . . 19 ((b ∪ ((bc) ∩ c )) ≡ ((b ∪ (bc)) ∩ (bc ))) = 1
72 ax-a2 31 . . . . . . . . . . . . . . . . . . . . . . 23 (b ∪ (bc)) = ((bc) ∪ b )
73 or32 82 . . . . . . . . . . . . . . . . . . . . . . . 24 ((bc) ∪ b ) = ((bb ) ∪ c)
74 ax-a2 31 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((bb ) ∪ c) = (c ∪ (bb ))
7549lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (c ∪ (bb )) = (c ∪ 1)
76 or1 104 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (c ∪ 1) = 1
7775, 76ax-r2 36 . . . . . . . . . . . . . . . . . . . . . . . . 25 (c ∪ (bb )) = 1
7874, 77ax-r2 36 . . . . . . . . . . . . . . . . . . . . . . . 24 ((bb ) ∪ c) = 1
7973, 78ax-r2 36 . . . . . . . . . . . . . . . . . . . . . . 23 ((bc) ∪ b ) = 1
8072, 79ax-r2 36 . . . . . . . . . . . . . . . . . . . . . 22 (b ∪ (bc)) = 1
8180ran 78 . . . . . . . . . . . . . . . . . . . . 21 ((b ∪ (bc)) ∩ (bc )) = (1 ∩ (bc ))
82 ancom 74 . . . . . . . . . . . . . . . . . . . . . 22 (1 ∩ (bc )) = ((bc ) ∩ 1)
83 an1 106 . . . . . . . . . . . . . . . . . . . . . 22 ((bc ) ∩ 1) = (bc )
8482, 83ax-r2 36 . . . . . . . . . . . . . . . . . . . . 21 (1 ∩ (bc )) = (bc )
8581, 84ax-r2 36 . . . . . . . . . . . . . . . . . . . 20 ((b ∪ (bc)) ∩ (bc )) = (bc )
8685bi1 118 . . . . . . . . . . . . . . . . . . 19 (((b ∪ (bc)) ∩ (bc )) ≡ (bc )) = 1
8771, 86wr2 371 . . . . . . . . . . . . . . . . . 18 ((b ∪ ((bc) ∩ c )) ≡ (bc )) = 1
8861, 87w2or 372 . . . . . . . . . . . . . . . . 17 (((b ∪ ((ab) ∩ a )) ∪ (b ∪ ((bc) ∩ c ))) ≡ ((ba ) ∪ (bc ))) = 1
8988wlor 368 . . . . . . . . . . . . . . . 16 (((ac ) ∪ ((b ∪ ((ab) ∩ a )) ∪ (b ∪ ((bc) ∩ c )))) ≡ ((ac ) ∪ ((ba ) ∪ (bc )))) = 1
9089wlor 368 . . . . . . . . . . . . . . 15 (((ac) ∪ ((ac ) ∪ ((b ∪ ((ab) ∩ a )) ∪ (b ∪ ((bc) ∩ c ))))) ≡ ((ac) ∪ ((ac ) ∪ ((ba ) ∪ (bc ))))) = 1
9135, 90wwbmpr 206 . . . . . . . . . . . . . 14 ((ac) ∪ ((ac ) ∪ ((b ∪ ((ab) ∩ a )) ∪ (b ∪ ((bc) ∩ c ))))) = 1
9219, 91ax-r2 36 . . . . . . . . . . . . 13 ((ac) ∪ (((ab) ∩ a ) ∪ (((ac ) ∪ b ) ∪ ((bc) ∩ c )))) = 1
9312, 92ax-r2 36 . . . . . . . . . . . 12 (((ab) ∩ a ) ∪ ((ac) ∪ (((ac ) ∪ b ) ∪ ((bc) ∩ c )))) = 1
94 ax-a3 32 . . . . . . . . . . . . . . 15 (((ac) ∪ (ac )) ∪ ((b ∩ ((ab) ∪ (bc))) ∪ ((bc) ∩ c ))) = ((ac) ∪ ((ac ) ∪ ((b ∩ ((ab) ∪ (bc))) ∪ ((bc) ∩ c ))))
9594bi1 118 . . . . . . . . . . . . . 14 ((((ac) ∪ (ac )) ∪ ((b ∩ ((ab) ∪ (bc))) ∪ ((bc) ∩ c ))) ≡ ((ac) ∪ ((ac ) ∪ ((b ∩ ((ab) ∪ (bc))) ∪ ((bc) ∩ c ))))) = 1
96 ax-a3 32 . . . . . . . . . . . . . . . . . 18 (((ac ) ∪ (b ∩ ((ab) ∪ (bc)))) ∪ ((bc) ∩ c )) = ((ac ) ∪ ((b ∩ ((ab) ∪ (bc))) ∪ ((bc) ∩ c )))
9796ax-r1 35 . . . . . . . . . . . . . . . . 17 ((ac ) ∪ ((b ∩ ((ab) ∪ (bc))) ∪ ((bc) ∩ c ))) = (((ac ) ∪ (b ∩ ((ab) ∪ (bc)))) ∪ ((bc) ∩ c ))
9897bi1 118 . . . . . . . . . . . . . . . 16 (((ac ) ∪ ((b ∩ ((ab) ∪ (bc))) ∪ ((bc) ∩ c ))) ≡ (((ac ) ∪ (b ∩ ((ab) ∪ (bc)))) ∪ ((bc) ∩ c ))) = 1
99 ancom 74 . . . . . . . . . . . . . . . . . . . 20 (b ∩ ((ab) ∪ (bc))) = (((ab) ∪ (bc)) ∩ b )
10099lor 70 . . . . . . . . . . . . . . . . . . 19 ((ac ) ∪ (b ∩ ((ab) ∪ (bc)))) = ((ac ) ∪ (((ab) ∪ (bc)) ∩ b ))
101100bi1 118 . . . . . . . . . . . . . . . . . 18 (((ac ) ∪ (b ∩ ((ab) ∪ (bc)))) ≡ ((ac ) ∪ (((ab) ∪ (bc)) ∩ b ))) = 1
102 wcomorr 412 . . . . . . . . . . . . . . . . . . . . . . . 24 C ((ac), ((ac) ∪ b)) = 1
103 orordir 113 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ac) ∪ b) = ((ab) ∪ (cb))
10466lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ab) ∪ (cb)) = ((ab) ∪ (bc))
105103, 104ax-r2 36 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((ac) ∪ b) = ((ab) ∪ (bc))
106105bi1 118 . . . . . . . . . . . . . . . . . . . . . . . 24 (((ac) ∪ b) ≡ ((ab) ∪ (bc))) = 1
107102, 106wcbtr 411 . . . . . . . . . . . . . . . . . . . . . . 23 C ((ac), ((ab) ∪ (bc))) = 1
108107wcomcom 414 . . . . . . . . . . . . . . . . . . . . . 22 C (((ab) ∪ (bc)), (ac)) = 1
109108wcomcom2 415 . . . . . . . . . . . . . . . . . . . . 21 C (((ab) ∪ (bc)), (ac) ) = 1
110 anor3 90 . . . . . . . . . . . . . . . . . . . . . . 23 (ac ) = (ac)
111110ax-r1 35 . . . . . . . . . . . . . . . . . . . . . 22 (ac) = (ac )
112111bi1 118 . . . . . . . . . . . . . . . . . . . . 21 ((ac) ≡ (ac )) = 1
113109, 112wcbtr 411 . . . . . . . . . . . . . . . . . . . 20 C (((ab) ∪ (bc)), (ac )) = 1
11439, 62wcom2or 427 . . . . . . . . . . . . . . . . . . . . . 22 C (b, ((ab) ∪ (bc))) = 1
115114wcomcom 414 . . . . . . . . . . . . . . . . . . . . 21 C (((ab) ∪ (bc)), b) = 1
116115wcomcom2 415 . . . . . . . . . . . . . . . . . . . 20 C (((ab) ∪ (bc)), b ) = 1
117113, 116wfh4 426 . . . . . . . . . . . . . . . . . . 19 (((ac ) ∪ (((ab) ∪ (bc)) ∩ b )) ≡ (((ac ) ∪ ((ab) ∪ (bc))) ∩ ((ac ) ∪ b ))) = 1
118 le1 146 . . . . . . . . . . . . . . . . . . . . . . 23 ((ac ) ∪ ((ab) ∪ (bc))) ≤ 1
119 df-t 41 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 = ((ac ) ∪ (ac ) )
120 oran 87 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (ac) = (ac )
121120ax-r1 35 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (ac ) = (ac)
122121lor 70 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((ac ) ∪ (ac ) ) = ((ac ) ∪ (ac))
123119, 122ax-r2 36 . . . . . . . . . . . . . . . . . . . . . . . 24 1 = ((ac ) ∪ (ac))
124 leo 158 . . . . . . . . . . . . . . . . . . . . . . . . . 26 a ≤ (ab)
125 leor 159 . . . . . . . . . . . . . . . . . . . . . . . . . 26 c ≤ (bc)
126124, 125le2or 168 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ac) ≤ ((ab) ∪ (bc))
127126lelor 166 . . . . . . . . . . . . . . . . . . . . . . . 24 ((ac ) ∪ (ac)) ≤ ((ac ) ∪ ((ab) ∪ (bc)))
128123, 127bltr 138 . . . . . . . . . . . . . . . . . . . . . . 23 1 ≤ ((ac ) ∪ ((ab) ∪ (bc)))
129118, 128lebi 145 . . . . . . . . . . . . . . . . . . . . . 22 ((ac ) ∪ ((ab) ∪ (bc))) = 1
130129ran 78 . . . . . . . . . . . . . . . . . . . . 21 (((ac ) ∪ ((ab) ∪ (bc))) ∩ ((ac ) ∪ b )) = (1 ∩ ((ac ) ∪ b ))
131 ancom 74 . . . . . . . . . . . . . . . . . . . . . 22 (1 ∩ ((ac ) ∪ b )) = (((ac ) ∪ b ) ∩ 1)
132 an1 106 . . . . . . . . . . . . . . . . . . . . . 22 (((ac ) ∪ b ) ∩ 1) = ((ac ) ∪ b )
133131, 132ax-r2 36 . . . . . . . . . . . . . . . . . . . . 21 (1 ∩ ((ac ) ∪ b )) = ((ac ) ∪ b )
134130, 133ax-r2 36 . . . . . . . . . . . . . . . . . . . 20 (((ac ) ∪ ((ab) ∪ (bc))) ∩ ((ac ) ∪ b )) = ((ac ) ∪ b )
135134bi1 118 . . . . . . . . . . . . . . . . . . 19 ((((ac ) ∪ ((ab) ∪ (bc))) ∩ ((ac ) ∪ b )) ≡ ((ac ) ∪ b )) = 1
136117, 135wr2 371 . . . . . . . . . . . . . . . . . 18 (((ac ) ∪ (((ab) ∪ (bc)) ∩ b )) ≡ ((ac ) ∪ b )) = 1
137101, 136wr2 371 . . . . . . . . . . . . . . . . 17 (((ac ) ∪ (b ∩ ((ab) ∪ (bc)))) ≡ ((ac ) ∪ b )) = 1
138137wr5-2v 366 . . . . . . . . . . . . . . . 16 ((((ac ) ∪ (b ∩ ((ab) ∪ (bc)))) ∪ ((bc) ∩ c )) ≡ (((ac ) ∪ b ) ∪ ((bc) ∩ c ))) = 1
13998, 138wr2 371 . . . . . . . . . . . . . . 15 (((ac ) ∪ ((b ∩ ((ab) ∪ (bc))) ∪ ((bc) ∩ c ))) ≡ (((ac ) ∪ b ) ∪ ((bc) ∩ c ))) = 1
140139wlor 368 . . . . . . . . . . . . . 14 (((ac) ∪ ((ac ) ∪ ((b ∩ ((ab) ∪ (bc))) ∪ ((bc) ∩ c )))) ≡ ((ac) ∪ (((ac ) ∪ b ) ∪ ((bc) ∩ c )))) = 1
14195, 140wr2 371 . . . . . . . . . . . . 13 ((((ac) ∪ (ac )) ∪ ((b ∩ ((ab) ∪ (bc))) ∪ ((bc) ∩ c ))) ≡ ((ac) ∪ (((ac ) ∪ b ) ∪ ((bc) ∩ c )))) = 1
142141wlor 368 . . . . . . . . . . . 12 ((((ab) ∩ a ) ∪ (((ac) ∪ (ac )) ∪ ((b ∩ ((ab) ∪ (bc))) ∪ ((bc) ∩ c )))) ≡ (((ab) ∩ a ) ∪ ((ac) ∪ (((ac ) ∪ b ) ∪ ((bc) ∩ c ))))) = 1
14393, 142wwbmpr 206 . . . . . . . . . . 11 (((ab) ∩ a ) ∪ (((ac) ∪ (ac )) ∪ ((b ∩ ((ab) ∪ (bc))) ∪ ((bc) ∩ c )))) = 1
14411, 143ax-r2 36 . . . . . . . . . 10 (((ac) ∪ (ac )) ∪ (((ab) ∩ a ) ∪ ((b ∩ ((ab) ∪ (bc))) ∪ ((bc) ∩ c )))) = 1
14510, 144ax-r2 36 . . . . . . . . 9 ((((ab) ∩ a ) ∪ ((b ∩ ((ab) ∪ (bc))) ∪ ((bc) ∩ c ))) ∪ ((ac) ∪ (ac ))) = 1
14639wcomcom3 416 . . . . . . . . . . . . 13 C (b , (ab)) = 1
14762wcomcom3 416 . . . . . . . . . . . . 13 C (b , (bc)) = 1
148146, 147wfh1 423 . . . . . . . . . . . 12 ((b ∩ ((ab) ∪ (bc))) ≡ ((b ∩ (ab)) ∪ (b ∩ (bc)))) = 1
149148wr5-2v 366 . . . . . . . . . . 11 (((b ∩ ((ab) ∪ (bc))) ∪ ((bc) ∩ c )) ≡ (((b ∩ (ab)) ∪ (b ∩ (bc))) ∪ ((bc) ∩ c ))) = 1
150149wlor 368 . . . . . . . . . 10 ((((ab) ∩ a ) ∪ ((b ∩ ((ab) ∪ (bc))) ∪ ((bc) ∩ c ))) ≡ (((ab) ∩ a ) ∪ (((b ∩ (ab)) ∪ (b ∩ (bc))) ∪ ((bc) ∩ c )))) = 1
151150wr5-2v 366 . . . . . . . . 9 (((((ab) ∩ a ) ∪ ((b ∩ ((ab) ∪ (bc))) ∪ ((bc) ∩ c ))) ∪ ((ac) ∪ (ac ))) ≡ ((((ab) ∩ a ) ∪ (((b ∩ (ab)) ∪ (b ∩ (bc))) ∪ ((bc) ∩ c ))) ∪ ((ac) ∪ (ac )))) = 1
152145, 151wwbmp 205 . . . . . . . 8 ((((ab) ∩ a ) ∪ (((b ∩ (ab)) ∪ (b ∩ (bc))) ∪ ((bc) ∩ c ))) ∪ ((ac) ∪ (ac ))) = 1
153152ax-r1 35 . . . . . . 7 1 = ((((ab) ∩ a ) ∪ (((b ∩ (ab)) ∪ (b ∩ (bc))) ∪ ((bc) ∩ c ))) ∪ ((ac) ∪ (ac )))
154 ax-a3 32 . . . . . . . . . . 11 ((((ab) ∩ a ) ∪ ((b ∩ (ab)) ∪ (b ∩ (bc)))) ∪ ((bc) ∩ c )) = (((ab) ∩ a ) ∪ (((b ∩ (ab)) ∪ (b ∩ (bc))) ∪ ((bc) ∩ c )))
155154ax-r1 35 . . . . . . . . . 10 (((ab) ∩ a ) ∪ (((b ∩ (ab)) ∪ (b ∩ (bc))) ∪ ((bc) ∩ c ))) = ((((ab) ∩ a ) ∪ ((b ∩ (ab)) ∪ (b ∩ (bc)))) ∪ ((bc) ∩ c ))
156 ax-a3 32 . . . . . . . . . . . 12 ((((ab) ∩ a ) ∪ (b ∩ (ab))) ∪ (b ∩ (bc))) = (((ab) ∩ a ) ∪ ((b ∩ (ab)) ∪ (b ∩ (bc))))
157156ax-r1 35 . . . . . . . . . . 11 (((ab) ∩ a ) ∪ ((b ∩ (ab)) ∪ (b ∩ (bc)))) = ((((ab) ∩ a ) ∪ (b ∩ (ab))) ∪ (b ∩ (bc)))
158157ax-r5 38 . . . . . . . . . 10 ((((ab) ∩ a ) ∪ ((b ∩ (ab)) ∪ (b ∩ (bc)))) ∪ ((bc) ∩ c )) = (((((ab) ∩ a ) ∪ (b ∩ (ab))) ∪ (b ∩ (bc))) ∪ ((bc) ∩ c ))
159155, 158ax-r2 36 . . . . . . . . 9 (((ab) ∩ a ) ∪ (((b ∩ (ab)) ∪ (b ∩ (bc))) ∪ ((bc) ∩ c ))) = (((((ab) ∩ a ) ∪ (b ∩ (ab))) ∪ (b ∩ (bc))) ∪ ((bc) ∩ c ))
160 ax-a3 32 . . . . . . . . 9 (((((ab) ∩ a ) ∪ (b ∩ (ab))) ∪ (b ∩ (bc))) ∪ ((bc) ∩ c )) = ((((ab) ∩ a ) ∪ (b ∩ (ab))) ∪ ((b ∩ (bc)) ∪ ((bc) ∩ c )))
161159, 160ax-r2 36 . . . . . . . 8 (((ab) ∩ a ) ∪ (((b ∩ (ab)) ∪ (b ∩ (bc))) ∪ ((bc) ∩ c ))) = ((((ab) ∩ a ) ∪ (b ∩ (ab))) ∪ ((b ∩ (bc)) ∪ ((bc) ∩ c )))
162161ax-r5 38 . . . . . . 7 ((((ab) ∩ a ) ∪ (((b ∩ (ab)) ∪ (b ∩ (bc))) ∪ ((bc) ∩ c ))) ∪ ((ac) ∪ (ac ))) = (((((ab) ∩ a ) ∪ (b ∩ (ab))) ∪ ((b ∩ (bc)) ∪ ((bc) ∩ c ))) ∪ ((ac) ∪ (ac )))
163153, 162ax-r2 36 . . . . . 6 1 = (((((ab) ∩ a ) ∪ (b ∩ (ab))) ∪ ((b ∩ (bc)) ∪ ((bc) ∩ c ))) ∪ ((ac) ∪ (ac )))
164 ancom 74 . . . . . . . . . 10 (b ∩ (ab)) = ((ab) ∩ b )
165164lor 70 . . . . . . . . 9 (((ab) ∩ a ) ∪ (b ∩ (ab))) = (((ab) ∩ a ) ∪ ((ab) ∩ b ))
166 ledi 174 . . . . . . . . 9 (((ab) ∩ a ) ∪ ((ab) ∩ b )) ≤ ((ab) ∩ (ab ))
167165, 166bltr 138 . . . . . . . 8 (((ab) ∩ a ) ∪ (b ∩ (ab))) ≤ ((ab) ∩ (ab ))
168 ancom 74 . . . . . . . . . 10 (b ∩ (bc)) = ((bc) ∩ b )
169168ax-r5 38 . . . . . . . . 9 ((b ∩ (bc)) ∪ ((bc) ∩ c )) = (((bc) ∩ b ) ∪ ((bc) ∩ c ))
170 ledi 174 . . . . . . . . 9 (((bc) ∩ b ) ∪ ((bc) ∩ c )) ≤ ((bc) ∩ (bc ))
171169, 170bltr 138 . . . . . . . 8 ((b ∩ (bc)) ∪ ((bc) ∩ c )) ≤ ((bc) ∩ (bc ))
172167, 171le2or 168 . . . . . . 7 ((((ab) ∩ a ) ∪ (b ∩ (ab))) ∪ ((b ∩ (bc)) ∪ ((bc) ∩ c ))) ≤ (((ab) ∩ (ab )) ∪ ((bc) ∩ (bc )))
173172leror 152 . . . . . 6 (((((ab) ∩ a ) ∪ (b ∩ (ab))) ∪ ((b ∩ (bc)) ∪ ((bc) ∩ c ))) ∪ ((ac) ∪ (ac ))) ≤ ((((ab) ∩ (ab )) ∪ ((bc) ∩ (bc ))) ∪ ((ac) ∪ (ac )))
174163, 173bltr 138 . . . . 5 1 ≤ ((((ab) ∩ (ab )) ∪ ((bc) ∩ (bc ))) ∪ ((ac) ∪ (ac )))
1759, 174lebi 145 . . . 4 ((((ab) ∩ (ab )) ∪ ((bc) ∩ (bc ))) ∪ ((ac) ∪ (ac ))) = 1
1768, 175ax-r2 36 . . 3 ((((ab) ∩ (ab )) ∪ ((bc) ∩ (bc ))) ∪ ((ac) ∪ (ac ))) = 1
1777, 176ax-r2 36 . 2 (((ab) ∩ (ab )) ∪ (((bc) ∩ (bc )) ∪ ((ac) ∪ (ac )))) = 1
1785, 177ax-r2 36 1 ((ab) ∪ ((bc) ∪ (ac))) = 1
 Colors of variables: term Syntax hints:   = wb 1  ⊥ wn 4   ≡ tb 5   ∪ wo 6   ∩ wa 7  1wt 8 This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-wom 361 This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-i2 45  df-le 129  df-le1 130  df-le2 131  df-cmtr 134 This theorem is referenced by:  u3lemax5  797
 Copyright terms: Public domain W3C validator