ska2 - Quantum Logic Explorer

	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. (Contributed by NM, 10-Nov-1998.)

**Assertion**
Ref	Expression
ska2	((a ≡ b)^⊥ ∪ ((b ≡ c)^⊥ ∪ (a ≡ c))) = 1

**Proof of Theorem ska2**
Step	Hyp	Ref	Expression
1		dfnb 95	. . 3 (a ≡ b)^⊥ = ((a ∪ b) ∩ (a^⊥ ∪ b^⊥ ))
2		dfnb 95	. . . 4 (b ≡ c)^⊥ = ((b ∪ c) ∩ (b^⊥ ∪ c^⊥ ))
3		dfb 94	. . . 4 (a ≡ c) = ((a ∩ c) ∪ (a^⊥ ∩ c^⊥ ))
4	2, 3	2or 72	. . 3 ((b ≡ c)^⊥ ∪ (a ≡ c)) = (((b ∪ c) ∩ (b^⊥ ∪ c^⊥ )) ∪ ((a ∩ c) ∪ (a^⊥ ∩ c^⊥ )))
5	1, 4	2or 72	. 2 ((a ≡ b)^⊥ ∪ ((b ≡ c)^⊥ ∪ (a ≡ c))) = (((a ∪ b) ∩ (a^⊥ ∪ b^⊥ )) ∪ (((b ∪ c) ∩ (b^⊥ ∪ c^⊥ )) ∪ ((a ∩ c) ∪ (a^⊥ ∩ c^⊥ ))))
6		ax-a3 32	. . 3 ((((a ∪ b) ∩ (a^⊥ ∪ b^⊥ )) ∪ ((b ∪ c) ∩ (b^⊥ ∪ c^⊥ ))) ∪ ((a ∩ c) ∪ (a^⊥ ∩ c^⊥ ))) = (((a ∪ b) ∩ (a^⊥ ∪ b^⊥ )) ∪ (((b ∪ c) ∩ (b^⊥ ∪ c^⊥ )) ∪ ((a ∩ c) ∪ (a^⊥ ∩ c^⊥ ))))
7	6	ax-r1 35	. 2 (((a ∪ b) ∩ (a^⊥ ∪ b^⊥ )) ∪ (((b ∪ c) ∩ (b^⊥ ∪ c^⊥ )) ∪ ((a ∩ c) ∪ (a^⊥ ∩ c^⊥ )))) = ((((a ∪ b) ∩ (a^⊥ ∪ b^⊥ )) ∪ ((b ∪ c) ∩ (b^⊥ ∪ c^⊥ ))) ∪ ((a ∩ c) ∪ (a^⊥ ∩ c^⊥ )))
8		le1 146	. . 3 ((((a ∪ b) ∩ (a^⊥ ∪ b^⊥ )) ∪ ((b ∪ c) ∩ (b^⊥ ∪ c^⊥ ))) ∪ ((a ∩ c) ∪ (a^⊥ ∩ c^⊥ ))) ≤ 1
9		ax-a2 31	. . . . . . . 8 ((((a ∪ b) ∩ a^⊥ ) ∪ ((b^⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c^⊥ ))) ∪ ((a ∩ c) ∪ (a^⊥ ∩ c^⊥ ))) = (((a ∩ c) ∪ (a^⊥ ∩ c^⊥ )) ∪ (((a ∪ b) ∩ a^⊥ ) ∪ ((b^⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c^⊥ ))))
10		or12 80	. . . . . . . 8 (((a ∩ c) ∪ (a^⊥ ∩ c^⊥ )) ∪ (((a ∪ b) ∩ a^⊥ ) ∪ ((b^⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c^⊥ )))) = (((a ∪ b) ∩ a^⊥ ) ∪ (((a ∩ c) ∪ (a^⊥ ∩ c^⊥ )) ∪ ((b^⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c^⊥ ))))
11		or12 80	. . . . . . . . . 10 (((a ∪ b) ∩ a^⊥ ) ∪ ((a ∩ c) ∪ (((a^⊥ ∩ c^⊥ ) ∪ b^⊥ ) ∪ ((b ∪ c) ∩ c^⊥ )))) = ((a ∩ c) ∪ (((a ∪ b) ∩ a^⊥ ) ∪ (((a^⊥ ∩ c^⊥ ) ∪ b^⊥ ) ∪ ((b ∪ c) ∩ c^⊥ ))))
12		or12 80	. . . . . . . . . . . 12 (((a ∪ b) ∩ a^⊥ ) ∪ (((a^⊥ ∩ c^⊥ ) ∪ b^⊥ ) ∪ ((b ∪ c) ∩ c^⊥ ))) = (((a^⊥ ∩ c^⊥ ) ∪ b^⊥ ) ∪ (((a ∪ b) ∩ a^⊥ ) ∪ ((b ∪ c) ∩ c^⊥ )))
13		ax-a3 32	. . . . . . . . . . . 12 (((a^⊥ ∩ c^⊥ ) ∪ b^⊥ ) ∪ (((a ∪ b) ∩ a^⊥ ) ∪ ((b ∪ c) ∩ c^⊥ ))) = ((a^⊥ ∩ c^⊥ ) ∪ (b^⊥ ∪ (((a ∪ b) ∩ a^⊥ ) ∪ ((b ∪ c) ∩ c^⊥ ))))
14		orordi 112	. . . . . . . . . . . . 13 (b^⊥ ∪ (((a ∪ b) ∩ a^⊥ ) ∪ ((b ∪ c) ∩ c^⊥ ))) = ((b^⊥ ∪ ((a ∪ b) ∩ a^⊥ )) ∪ (b^⊥ ∪ ((b ∪ c) ∩ c^⊥ )))
15	14	lor 70	. . . . . . . . . . . 12 ((a^⊥ ∩ c^⊥ ) ∪ (b^⊥ ∪ (((a ∪ b) ∩ a^⊥ ) ∪ ((b ∪ c) ∩ c^⊥ )))) = ((a^⊥ ∩ c^⊥ ) ∪ ((b^⊥ ∪ ((a ∪ b) ∩ a^⊥ )) ∪ (b^⊥ ∪ ((b ∪ c) ∩ c^⊥ ))))
16	12, 13, 15	3tr 65	. . . . . . . . . . 11 (((a ∪ b) ∩ a^⊥ ) ∪ (((a^⊥ ∩ c^⊥ ) ∪ b^⊥ ) ∪ ((b ∪ c) ∩ c^⊥ ))) = ((a^⊥ ∩ c^⊥ ) ∪ ((b^⊥ ∪ ((a ∪ b) ∩ a^⊥ )) ∪ (b^⊥ ∪ ((b ∪ c) ∩ c^⊥ ))))
17	16	lor 70	. . . . . . . . . 10 ((a ∩ c) ∪ (((a ∪ b) ∩ a^⊥ ) ∪ (((a^⊥ ∩ c^⊥ ) ∪ b^⊥ ) ∪ ((b ∪ c) ∩ c^⊥ )))) = ((a ∩ c) ∪ ((a^⊥ ∩ c^⊥ ) ∪ ((b^⊥ ∪ ((a ∪ b) ∩ a^⊥ )) ∪ (b^⊥ ∪ ((b ∪ c) ∩ c^⊥ )))))
18		or12 80	. . . . . . . . . . . 12 ((a ∩ c) ∪ ((a^⊥ ∩ c^⊥ ) ∪ ((b^⊥ ∪ a^⊥ ) ∪ (b^⊥ ∪ c^⊥ )))) = ((a^⊥ ∩ c^⊥ ) ∪ ((a ∩ c) ∪ ((b^⊥ ∪ a^⊥ ) ∪ (b^⊥ ∪ c^⊥ ))))
19		le1 146	. . . . . . . . . . . . 13 ((a^⊥ ∩ c^⊥ ) ∪ ((a ∩ c) ∪ ((b^⊥ ∪ a^⊥ ) ∪ (b^⊥ ∪ c^⊥ )))) ≤ 1
20		df-t 41	. . . . . . . . . . . . . . . 16 1 = ((a ∩ c) ∪ (a ∩ c)^⊥ )
21		oran3 93	. . . . . . . . . . . . . . . . . 18 (a^⊥ ∪ c^⊥ ) = (a ∩ c)^⊥
22	21	lor 70	. . . . . . . . . . . . . . . . 17 ((a ∩ c) ∪ (a^⊥ ∪ c^⊥ )) = ((a ∩ c) ∪ (a ∩ c)^⊥ )
23	22	ax-r1 35	. . . . . . . . . . . . . . . 16 ((a ∩ c) ∪ (a ∩ c)^⊥ ) = ((a ∩ c) ∪ (a^⊥ ∪ c^⊥ ))
24	20, 23	ax-r2 36	. . . . . . . . . . . . . . 15 1 = ((a ∩ c) ∪ (a^⊥ ∪ c^⊥ ))
25		leor 159	. . . . . . . . . . . . . . . . 17 a^⊥ ≤ (b^⊥ ∪ a^⊥ )
26		leor 159	. . . . . . . . . . . . . . . . 17 c^⊥ ≤ (b^⊥ ∪ c^⊥ )
27	25, 26	le2or 168	. . . . . . . . . . . . . . . 16 (a^⊥ ∪ c^⊥ ) ≤ ((b^⊥ ∪ a^⊥ ) ∪ (b^⊥ ∪ c^⊥ ))
28	27	lelor 166	. . . . . . . . . . . . . . 15 ((a ∩ c) ∪ (a^⊥ ∪ c^⊥ )) ≤ ((a ∩ c) ∪ ((b^⊥ ∪ a^⊥ ) ∪ (b^⊥ ∪ c^⊥ )))
29	24, 28	bltr 138	. . . . . . . . . . . . . 14 1 ≤ ((a ∩ c) ∪ ((b^⊥ ∪ a^⊥ ) ∪ (b^⊥ ∪ c^⊥ )))
30	29	lerr 150	. . . . . . . . . . . . 13 1 ≤ ((a^⊥ ∩ c^⊥ ) ∪ ((a ∩ c) ∪ ((b^⊥ ∪ a^⊥ ) ∪ (b^⊥ ∪ c^⊥ ))))
31	19, 30	lebi 145	. . . . . . . . . . . 12 ((a^⊥ ∩ c^⊥ ) ∪ ((a ∩ c) ∪ ((b^⊥ ∪ a^⊥ ) ∪ (b^⊥ ∪ c^⊥ )))) = 1
32	18, 31	ax-r2 36	. . . . . . . . . . 11 ((a ∩ c) ∪ ((a^⊥ ∩ c^⊥ ) ∪ ((b^⊥ ∪ a^⊥ ) ∪ (b^⊥ ∪ c^⊥ )))) = 1
33		wcomorr 412	. . . . . . . . . . . . . . . . . . 19 C (b, (b ∪ a)) = 1
34		wa2 192	. . . . . . . . . . . . . . . . . . 19 ((b ∪ a) ≡ (a ∪ b)) = 1
35	33, 34	wcbtr 411	. . . . . . . . . . . . . . . . . 18 C (b, (a ∪ b)) = 1
36	35	wcomcom 414	. . . . . . . . . . . . . . . . 17 C ((a ∪ b), b) = 1
37	36	wcomcom2 415	. . . . . . . . . . . . . . . 16 C ((a ∪ b), b^⊥ ) = 1
38		wcomorr 412	. . . . . . . . . . . . . . . . . 18 C (a, (a ∪ b)) = 1
39	38	wcomcom 414	. . . . . . . . . . . . . . . . 17 C ((a ∪ b), a) = 1
40	39	wcomcom2 415	. . . . . . . . . . . . . . . 16 C ((a ∪ b), a^⊥ ) = 1
41	37, 40	wfh4 426	. . . . . . . . . . . . . . 15 ((b^⊥ ∪ ((a ∪ b) ∩ a^⊥ )) ≡ ((b^⊥ ∪ (a ∪ b)) ∩ (b^⊥ ∪ a^⊥ ))) = 1
42		or12 80	. . . . . . . . . . . . . . . . . . 19 (b^⊥ ∪ (a ∪ b)) = (a ∪ (b^⊥ ∪ b))
43		ax-a2 31	. . . . . . . . . . . . . . . . . . . . 21 (b^⊥ ∪ b) = (b ∪ b^⊥ )
44		df-t 41	. . . . . . . . . . . . . . . . . . . . . 22 1 = (b ∪ b^⊥ )
45	44	ax-r1 35	. . . . . . . . . . . . . . . . . . . . 21 (b ∪ b^⊥ ) = 1
46	43, 45	ax-r2 36	. . . . . . . . . . . . . . . . . . . 20 (b^⊥ ∪ b) = 1
47	46	lor 70	. . . . . . . . . . . . . . . . . . 19 (a ∪ (b^⊥ ∪ b)) = (a ∪ 1)
48		or1 104	. . . . . . . . . . . . . . . . . . 19 (a ∪ 1) = 1
49	42, 47, 48	3tr 65	. . . . . . . . . . . . . . . . . 18 (b^⊥ ∪ (a ∪ b)) = 1
50	49	ran 78	. . . . . . . . . . . . . . . . 17 ((b^⊥ ∪ (a ∪ b)) ∩ (b^⊥ ∪ a^⊥ )) = (1 ∩ (b^⊥ ∪ a^⊥ ))
51		an1r 107	. . . . . . . . . . . . . . . . 17 (1 ∩ (b^⊥ ∪ a^⊥ )) = (b^⊥ ∪ a^⊥ )
52	50, 51	ax-r2 36	. . . . . . . . . . . . . . . 16 ((b^⊥ ∪ (a ∪ b)) ∩ (b^⊥ ∪ a^⊥ )) = (b^⊥ ∪ a^⊥ )
53	52	bi1 118	. . . . . . . . . . . . . . 15 (((b^⊥ ∪ (a ∪ b)) ∩ (b^⊥ ∪ a^⊥ )) ≡ (b^⊥ ∪ a^⊥ )) = 1
54	41, 53	wr2 371	. . . . . . . . . . . . . 14 ((b^⊥ ∪ ((a ∪ b) ∩ a^⊥ )) ≡ (b^⊥ ∪ a^⊥ )) = 1
55		wcomorr 412	. . . . . . . . . . . . . . . . . 18 C (b, (b ∪ c)) = 1
56	55	wcomcom 414	. . . . . . . . . . . . . . . . 17 C ((b ∪ c), b) = 1
57	56	wcomcom2 415	. . . . . . . . . . . . . . . 16 C ((b ∪ c), b^⊥ ) = 1
58		wcomorr 412	. . . . . . . . . . . . . . . . . . 19 C (c, (c ∪ b)) = 1
59		wa2 192	. . . . . . . . . . . . . . . . . . 19 ((c ∪ b) ≡ (b ∪ c)) = 1
60	58, 59	wcbtr 411	. . . . . . . . . . . . . . . . . 18 C (c, (b ∪ c)) = 1
61	60	wcomcom 414	. . . . . . . . . . . . . . . . 17 C ((b ∪ c), c) = 1
62	61	wcomcom2 415	. . . . . . . . . . . . . . . 16 C ((b ∪ c), c^⊥ ) = 1
63	57, 62	wfh4 426	. . . . . . . . . . . . . . 15 ((b^⊥ ∪ ((b ∪ c) ∩ c^⊥ )) ≡ ((b^⊥ ∪ (b ∪ c)) ∩ (b^⊥ ∪ c^⊥ ))) = 1
64		ax-a2 31	. . . . . . . . . . . . . . . . . . 19 (b^⊥ ∪ (b ∪ c)) = ((b ∪ c) ∪ b^⊥ )
65		or32 82	. . . . . . . . . . . . . . . . . . 19 ((b ∪ c) ∪ b^⊥ ) = ((b ∪ b^⊥ ) ∪ c)
66		ax-a2 31	. . . . . . . . . . . . . . . . . . . 20 ((b ∪ b^⊥ ) ∪ c) = (c ∪ (b ∪ b^⊥ ))
67	45	lor 70	. . . . . . . . . . . . . . . . . . . 20 (c ∪ (b ∪ b^⊥ )) = (c ∪ 1)
68		or1 104	. . . . . . . . . . . . . . . . . . . 20 (c ∪ 1) = 1
69	66, 67, 68	3tr 65	. . . . . . . . . . . . . . . . . . 19 ((b ∪ b^⊥ ) ∪ c) = 1
70	64, 65, 69	3tr 65	. . . . . . . . . . . . . . . . . 18 (b^⊥ ∪ (b ∪ c)) = 1
71	70	ran 78	. . . . . . . . . . . . . . . . 17 ((b^⊥ ∪ (b ∪ c)) ∩ (b^⊥ ∪ c^⊥ )) = (1 ∩ (b^⊥ ∪ c^⊥ ))
72		an1r 107	. . . . . . . . . . . . . . . . 17 (1 ∩ (b^⊥ ∪ c^⊥ )) = (b^⊥ ∪ c^⊥ )
73	71, 72	ax-r2 36	. . . . . . . . . . . . . . . 16 ((b^⊥ ∪ (b ∪ c)) ∩ (b^⊥ ∪ c^⊥ )) = (b^⊥ ∪ c^⊥ )
74	73	bi1 118	. . . . . . . . . . . . . . 15 (((b^⊥ ∪ (b ∪ c)) ∩ (b^⊥ ∪ c^⊥ )) ≡ (b^⊥ ∪ c^⊥ )) = 1
75	63, 74	wr2 371	. . . . . . . . . . . . . 14 ((b^⊥ ∪ ((b ∪ c) ∩ c^⊥ )) ≡ (b^⊥ ∪ c^⊥ )) = 1
76	54, 75	w2or 372	. . . . . . . . . . . . 13 (((b^⊥ ∪ ((a ∪ b) ∩ a^⊥ )) ∪ (b^⊥ ∪ ((b ∪ c) ∩ c^⊥ ))) ≡ ((b^⊥ ∪ a^⊥ ) ∪ (b^⊥ ∪ c^⊥ ))) = 1
77	76	wlor 368	. . . . . . . . . . . 12 (((a^⊥ ∩ c^⊥ ) ∪ ((b^⊥ ∪ ((a ∪ b) ∩ a^⊥ )) ∪ (b^⊥ ∪ ((b ∪ c) ∩ c^⊥ )))) ≡ ((a^⊥ ∩ c^⊥ ) ∪ ((b^⊥ ∪ a^⊥ ) ∪ (b^⊥ ∪ c^⊥ )))) = 1
78	77	wlor 368	. . . . . . . . . . 11 (((a ∩ c) ∪ ((a^⊥ ∩ c^⊥ ) ∪ ((b^⊥ ∪ ((a ∪ b) ∩ a^⊥ )) ∪ (b^⊥ ∪ ((b ∪ c) ∩ c^⊥ ))))) ≡ ((a ∩ c) ∪ ((a^⊥ ∩ c^⊥ ) ∪ ((b^⊥ ∪ a^⊥ ) ∪ (b^⊥ ∪ c^⊥ ))))) = 1
79	32, 78	wwbmpr 206	. . . . . . . . . 10 ((a ∩ c) ∪ ((a^⊥ ∩ c^⊥ ) ∪ ((b^⊥ ∪ ((a ∪ b) ∩ a^⊥ )) ∪ (b^⊥ ∪ ((b ∪ c) ∩ c^⊥ ))))) = 1
80	11, 17, 79	3tr 65	. . . . . . . . 9 (((a ∪ b) ∩ a^⊥ ) ∪ ((a ∩ c) ∪ (((a^⊥ ∩ c^⊥ ) ∪ b^⊥ ) ∪ ((b ∪ c) ∩ c^⊥ )))) = 1
81		wa3 193	. . . . . . . . . . 11 ((((a ∩ c) ∪ (a^⊥ ∩ c^⊥ )) ∪ ((b^⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c^⊥ ))) ≡ ((a ∩ c) ∪ ((a^⊥ ∩ c^⊥ ) ∪ ((b^⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c^⊥ ))))) = 1
82		ax-a3 32	. . . . . . . . . . . . . . 15 (((a^⊥ ∩ c^⊥ ) ∪ (b^⊥ ∩ ((a ∪ b) ∪ (b ∪ c)))) ∪ ((b ∪ c) ∩ c^⊥ )) = ((a^⊥ ∩ c^⊥ ) ∪ ((b^⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c^⊥ )))
83	82	ax-r1 35	. . . . . . . . . . . . . 14 ((a^⊥ ∩ c^⊥ ) ∪ ((b^⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c^⊥ ))) = (((a^⊥ ∩ c^⊥ ) ∪ (b^⊥ ∩ ((a ∪ b) ∪ (b ∪ c)))) ∪ ((b ∪ c) ∩ c^⊥ ))
84	83	bi1 118	. . . . . . . . . . . . 13 (((a^⊥ ∩ c^⊥ ) ∪ ((b^⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c^⊥ ))) ≡ (((a^⊥ ∩ c^⊥ ) ∪ (b^⊥ ∩ ((a ∪ b) ∪ (b ∪ c)))) ∪ ((b ∪ c) ∩ c^⊥ ))) = 1
85		ancom 74	. . . . . . . . . . . . . . . . 17 (b^⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) = (((a ∪ b) ∪ (b ∪ c)) ∩ b^⊥ )
86	85	lor 70	. . . . . . . . . . . . . . . 16 ((a^⊥ ∩ c^⊥ ) ∪ (b^⊥ ∩ ((a ∪ b) ∪ (b ∪ c)))) = ((a^⊥ ∩ c^⊥ ) ∪ (((a ∪ b) ∪ (b ∪ c)) ∩ b^⊥ ))
87	86	bi1 118	. . . . . . . . . . . . . . 15 (((a^⊥ ∩ c^⊥ ) ∪ (b^⊥ ∩ ((a ∪ b) ∪ (b ∪ c)))) ≡ ((a^⊥ ∩ c^⊥ ) ∪ (((a ∪ b) ∪ (b ∪ c)) ∩ b^⊥ ))) = 1
88		wcomorr 412	. . . . . . . . . . . . . . . . . . . . 21 C ((a ∪ c), ((a ∪ c) ∪ b)) = 1
89		orordir 113	. . . . . . . . . . . . . . . . . . . . . . 23 ((a ∪ c) ∪ b) = ((a ∪ b) ∪ (c ∪ b))
90		ax-a2 31	. . . . . . . . . . . . . . . . . . . . . . . 24 (c ∪ b) = (b ∪ c)
91	90	lor 70	. . . . . . . . . . . . . . . . . . . . . . 23 ((a ∪ b) ∪ (c ∪ b)) = ((a ∪ b) ∪ (b ∪ c))
92	89, 91	ax-r2 36	. . . . . . . . . . . . . . . . . . . . . 22 ((a ∪ c) ∪ b) = ((a ∪ b) ∪ (b ∪ c))
93	92	bi1 118	. . . . . . . . . . . . . . . . . . . . 21 (((a ∪ c) ∪ b) ≡ ((a ∪ b) ∪ (b ∪ c))) = 1
94	88, 93	wcbtr 411	. . . . . . . . . . . . . . . . . . . 20 C ((a ∪ c), ((a ∪ b) ∪ (b ∪ c))) = 1
95	94	wcomcom 414	. . . . . . . . . . . . . . . . . . 19 C (((a ∪ b) ∪ (b ∪ c)), (a ∪ c)) = 1
96	95	wcomcom2 415	. . . . . . . . . . . . . . . . . 18 C (((a ∪ b) ∪ (b ∪ c)), (a ∪ c)^⊥ ) = 1
97		ska10 238	. . . . . . . . . . . . . . . . . 18 ((a ∪ c)^⊥ ≡ (a^⊥ ∩ c^⊥ )) = 1
98	96, 97	wcbtr 411	. . . . . . . . . . . . . . . . 17 C (((a ∪ b) ∪ (b ∪ c)), (a^⊥ ∩ c^⊥ )) = 1
99	35, 55	wcom2or 427	. . . . . . . . . . . . . . . . . . 19 C (b, ((a ∪ b) ∪ (b ∪ c))) = 1
100	99	wcomcom 414	. . . . . . . . . . . . . . . . . 18 C (((a ∪ b) ∪ (b ∪ c)), b) = 1
101	100	wcomcom2 415	. . . . . . . . . . . . . . . . 17 C (((a ∪ b) ∪ (b ∪ c)), b^⊥ ) = 1
102	98, 101	wfh4 426	. . . . . . . . . . . . . . . 16 (((a^⊥ ∩ c^⊥ ) ∪ (((a ∪ b) ∪ (b ∪ c)) ∩ b^⊥ )) ≡ (((a^⊥ ∩ c^⊥ ) ∪ ((a ∪ b) ∪ (b ∪ c))) ∩ ((a^⊥ ∩ c^⊥ ) ∪ b^⊥ ))) = 1
103		le1 146	. . . . . . . . . . . . . . . . . . . 20 ((a^⊥ ∩ c^⊥ ) ∪ ((a ∪ b) ∪ (b ∪ c))) ≤ 1
104		df-t 41	. . . . . . . . . . . . . . . . . . . . . 22 1 = ((a^⊥ ∩ c^⊥ ) ∪ (a^⊥ ∩ c^⊥ )^⊥ )
105		oran 87	. . . . . . . . . . . . . . . . . . . . . . . 24 (a ∪ c) = (a^⊥ ∩ c^⊥ )^⊥
106	105	ax-r1 35	. . . . . . . . . . . . . . . . . . . . . . 23 (a^⊥ ∩ c^⊥ )^⊥ = (a ∪ c)
107	106	lor 70	. . . . . . . . . . . . . . . . . . . . . 22 ((a^⊥ ∩ c^⊥ ) ∪ (a^⊥ ∩ c^⊥ )^⊥ ) = ((a^⊥ ∩ c^⊥ ) ∪ (a ∪ c))
108	104, 107	ax-r2 36	. . . . . . . . . . . . . . . . . . . . 21 1 = ((a^⊥ ∩ c^⊥ ) ∪ (a ∪ c))
109		leo 158	. . . . . . . . . . . . . . . . . . . . . . 23 a ≤ (a ∪ b)
110		leor 159	. . . . . . . . . . . . . . . . . . . . . . 23 c ≤ (b ∪ c)
111	109, 110	le2or 168	. . . . . . . . . . . . . . . . . . . . . 22 (a ∪ c) ≤ ((a ∪ b) ∪ (b ∪ c))
112	111	lelor 166	. . . . . . . . . . . . . . . . . . . . 21 ((a^⊥ ∩ c^⊥ ) ∪ (a ∪ c)) ≤ ((a^⊥ ∩ c^⊥ ) ∪ ((a ∪ b) ∪ (b ∪ c)))
113	108, 112	bltr 138	. . . . . . . . . . . . . . . . . . . 20 1 ≤ ((a^⊥ ∩ c^⊥ ) ∪ ((a ∪ b) ∪ (b ∪ c)))
114	103, 113	lebi 145	. . . . . . . . . . . . . . . . . . 19 ((a^⊥ ∩ c^⊥ ) ∪ ((a ∪ b) ∪ (b ∪ c))) = 1
115	114	ran 78	. . . . . . . . . . . . . . . . . 18 (((a^⊥ ∩ c^⊥ ) ∪ ((a ∪ b) ∪ (b ∪ c))) ∩ ((a^⊥ ∩ c^⊥ ) ∪ b^⊥ )) = (1 ∩ ((a^⊥ ∩ c^⊥ ) ∪ b^⊥ ))
116		an1r 107	. . . . . . . . . . . . . . . . . 18 (1 ∩ ((a^⊥ ∩ c^⊥ ) ∪ b^⊥ )) = ((a^⊥ ∩ c^⊥ ) ∪ b^⊥ )
117	115, 116	ax-r2 36	. . . . . . . . . . . . . . . . 17 (((a^⊥ ∩ c^⊥ ) ∪ ((a ∪ b) ∪ (b ∪ c))) ∩ ((a^⊥ ∩ c^⊥ ) ∪ b^⊥ )) = ((a^⊥ ∩ c^⊥ ) ∪ b^⊥ )
118	117	bi1 118	. . . . . . . . . . . . . . . 16 ((((a^⊥ ∩ c^⊥ ) ∪ ((a ∪ b) ∪ (b ∪ c))) ∩ ((a^⊥ ∩ c^⊥ ) ∪ b^⊥ )) ≡ ((a^⊥ ∩ c^⊥ ) ∪ b^⊥ )) = 1
119	102, 118	wr2 371	. . . . . . . . . . . . . . 15 (((a^⊥ ∩ c^⊥ ) ∪ (((a ∪ b) ∪ (b ∪ c)) ∩ b^⊥ )) ≡ ((a^⊥ ∩ c^⊥ ) ∪ b^⊥ )) = 1
120	87, 119	wr2 371	. . . . . . . . . . . . . 14 (((a^⊥ ∩ c^⊥ ) ∪ (b^⊥ ∩ ((a ∪ b) ∪ (b ∪ c)))) ≡ ((a^⊥ ∩ c^⊥ ) ∪ b^⊥ )) = 1
121	120	wr5-2v 366	. . . . . . . . . . . . 13 ((((a^⊥ ∩ c^⊥ ) ∪ (b^⊥ ∩ ((a ∪ b) ∪ (b ∪ c)))) ∪ ((b ∪ c) ∩ c^⊥ )) ≡ (((a^⊥ ∩ c^⊥ ) ∪ b^⊥ ) ∪ ((b ∪ c) ∩ c^⊥ ))) = 1
122	84, 121	wr2 371	. . . . . . . . . . . 12 (((a^⊥ ∩ c^⊥ ) ∪ ((b^⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c^⊥ ))) ≡ (((a^⊥ ∩ c^⊥ ) ∪ b^⊥ ) ∪ ((b ∪ c) ∩ c^⊥ ))) = 1
123	122	wlor 368	. . . . . . . . . . 11 (((a ∩ c) ∪ ((a^⊥ ∩ c^⊥ ) ∪ ((b^⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c^⊥ )))) ≡ ((a ∩ c) ∪ (((a^⊥ ∩ c^⊥ ) ∪ b^⊥ ) ∪ ((b ∪ c) ∩ c^⊥ )))) = 1
124	81, 123	wr2 371	. . . . . . . . . 10 ((((a ∩ c) ∪ (a^⊥ ∩ c^⊥ )) ∪ ((b^⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c^⊥ ))) ≡ ((a ∩ c) ∪ (((a^⊥ ∩ c^⊥ ) ∪ b^⊥ ) ∪ ((b ∪ c) ∩ c^⊥ )))) = 1
125	124	wlor 368	. . . . . . . . 9 ((((a ∪ b) ∩ a^⊥ ) ∪ (((a ∩ c) ∪ (a^⊥ ∩ c^⊥ )) ∪ ((b^⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c^⊥ )))) ≡ (((a ∪ b) ∩ a^⊥ ) ∪ ((a ∩ c) ∪ (((a^⊥ ∩ c^⊥ ) ∪ b^⊥ ) ∪ ((b ∪ c) ∩ c^⊥ ))))) = 1
126	80, 125	wwbmpr 206	. . . . . . . 8 (((a ∪ b) ∩ a^⊥ ) ∪ (((a ∩ c) ∪ (a^⊥ ∩ c^⊥ )) ∪ ((b^⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c^⊥ )))) = 1
127	9, 10, 126	3tr 65	. . . . . . 7 ((((a ∪ b) ∩ a^⊥ ) ∪ ((b^⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c^⊥ ))) ∪ ((a ∩ c) ∪ (a^⊥ ∩ c^⊥ ))) = 1
128	35	wcomcom3 416	. . . . . . . . . . 11 C (b^⊥ , (a ∪ b)) = 1
129	55	wcomcom3 416	. . . . . . . . . . 11 C (b^⊥ , (b ∪ c)) = 1
130	128, 129	wfh1 423	. . . . . . . . . 10 ((b^⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ≡ ((b^⊥ ∩ (a ∪ b)) ∪ (b^⊥ ∩ (b ∪ c)))) = 1
131	130	wr5-2v 366	. . . . . . . . 9 (((b^⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c^⊥ )) ≡ (((b^⊥ ∩ (a ∪ b)) ∪ (b^⊥ ∩ (b ∪ c))) ∪ ((b ∪ c) ∩ c^⊥ ))) = 1
132	131	wlor 368	. . . . . . . 8 ((((a ∪ b) ∩ a^⊥ ) ∪ ((b^⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c^⊥ ))) ≡ (((a ∪ b) ∩ a^⊥ ) ∪ (((b^⊥ ∩ (a ∪ b)) ∪ (b^⊥ ∩ (b ∪ c))) ∪ ((b ∪ c) ∩ c^⊥ )))) = 1
133	132	wr5-2v 366	. . . . . . 7 (((((a ∪ b) ∩ a^⊥ ) ∪ ((b^⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c^⊥ ))) ∪ ((a ∩ c) ∪ (a^⊥ ∩ c^⊥ ))) ≡ ((((a ∪ b) ∩ a^⊥ ) ∪ (((b^⊥ ∩ (a ∪ b)) ∪ (b^⊥ ∩ (b ∪ c))) ∪ ((b ∪ c) ∩ c^⊥ ))) ∪ ((a ∩ c) ∪ (a^⊥ ∩ c^⊥ )))) = 1
134	127, 133	wwbmp 205	. . . . . 6 ((((a ∪ b) ∩ a^⊥ ) ∪ (((b^⊥ ∩ (a ∪ b)) ∪ (b^⊥ ∩ (b ∪ c))) ∪ ((b ∪ c) ∩ c^⊥ ))) ∪ ((a ∩ c) ∪ (a^⊥ ∩ c^⊥ ))) = 1
135	134	ax-r1 35	. . . . 5 1 = ((((a ∪ b) ∩ a^⊥ ) ∪ (((b^⊥ ∩ (a ∪ b)) ∪ (b^⊥ ∩ (b ∪ c))) ∪ ((b ∪ c) ∩ c^⊥ ))) ∪ ((a ∩ c) ∪ (a^⊥ ∩ c^⊥ )))
136		ax-a3 32	. . . . . . . 8 ((((a ∪ b) ∩ a^⊥ ) ∪ ((b^⊥ ∩ (a ∪ b)) ∪ (b^⊥ ∩ (b ∪ c)))) ∪ ((b ∪ c) ∩ c^⊥ )) = (((a ∪ b) ∩ a^⊥ ) ∪ (((b^⊥ ∩ (a ∪ b)) ∪ (b^⊥ ∩ (b ∪ c))) ∪ ((b ∪ c) ∩ c^⊥ )))
137	136	ax-r1 35	. . . . . . 7 (((a ∪ b) ∩ a^⊥ ) ∪ (((b^⊥ ∩ (a ∪ b)) ∪ (b^⊥ ∩ (b ∪ c))) ∪ ((b ∪ c) ∩ c^⊥ ))) = ((((a ∪ b) ∩ a^⊥ ) ∪ ((b^⊥ ∩ (a ∪ b)) ∪ (b^⊥ ∩ (b ∪ c)))) ∪ ((b ∪ c) ∩ c^⊥ ))
138		ax-a3 32	. . . . . . . . 9 ((((a ∪ b) ∩ a^⊥ ) ∪ (b^⊥ ∩ (a ∪ b))) ∪ (b^⊥ ∩ (b ∪ c))) = (((a ∪ b) ∩ a^⊥ ) ∪ ((b^⊥ ∩ (a ∪ b)) ∪ (b^⊥ ∩ (b ∪ c))))
139	138	ax-r1 35	. . . . . . . 8 (((a ∪ b) ∩ a^⊥ ) ∪ ((b^⊥ ∩ (a ∪ b)) ∪ (b^⊥ ∩ (b ∪ c)))) = ((((a ∪ b) ∩ a^⊥ ) ∪ (b^⊥ ∩ (a ∪ b))) ∪ (b^⊥ ∩ (b ∪ c)))
140	139	ax-r5 38	. . . . . . 7 ((((a ∪ b) ∩ a^⊥ ) ∪ ((b^⊥ ∩ (a ∪ b)) ∪ (b^⊥ ∩ (b ∪ c)))) ∪ ((b ∪ c) ∩ c^⊥ )) = (((((a ∪ b) ∩ a^⊥ ) ∪ (b^⊥ ∩ (a ∪ b))) ∪ (b^⊥ ∩ (b ∪ c))) ∪ ((b ∪ c) ∩ c^⊥ ))
141		ax-a3 32	. . . . . . 7 (((((a ∪ b) ∩ a^⊥ ) ∪ (b^⊥ ∩ (a ∪ b))) ∪ (b^⊥ ∩ (b ∪ c))) ∪ ((b ∪ c) ∩ c^⊥ )) = ((((a ∪ b) ∩ a^⊥ ) ∪ (b^⊥ ∩ (a ∪ b))) ∪ ((b^⊥ ∩ (b ∪ c)) ∪ ((b ∪ c) ∩ c^⊥ )))
142	137, 140, 141	3tr 65	. . . . . 6 (((a ∪ b) ∩ a^⊥ ) ∪ (((b^⊥ ∩ (a ∪ b)) ∪ (b^⊥ ∩ (b ∪ c))) ∪ ((b ∪ c) ∩ c^⊥ ))) = ((((a ∪ b) ∩ a^⊥ ) ∪ (b^⊥ ∩ (a ∪ b))) ∪ ((b^⊥ ∩ (b ∪ c)) ∪ ((b ∪ c) ∩ c^⊥ )))
143	142	ax-r5 38	. . . . 5 ((((a ∪ b) ∩ a^⊥ ) ∪ (((b^⊥ ∩ (a ∪ b)) ∪ (b^⊥ ∩ (b ∪ c))) ∪ ((b ∪ c) ∩ c^⊥ ))) ∪ ((a ∩ c) ∪ (a^⊥ ∩ c^⊥ ))) = (((((a ∪ b) ∩ a^⊥ ) ∪ (b^⊥ ∩ (a ∪ b))) ∪ ((b^⊥ ∩ (b ∪ c)) ∪ ((b ∪ c) ∩ c^⊥ ))) ∪ ((a ∩ c) ∪ (a^⊥ ∩ c^⊥ )))
144	135, 143	ax-r2 36	. . . 4 1 = (((((a ∪ b) ∩ a^⊥ ) ∪ (b^⊥ ∩ (a ∪ b))) ∪ ((b^⊥ ∩ (b ∪ c)) ∪ ((b ∪ c) ∩ c^⊥ ))) ∪ ((a ∩ c) ∪ (a^⊥ ∩ c^⊥ )))
145		ancom 74	. . . . . . . 8 (b^⊥ ∩ (a ∪ b)) = ((a ∪ b) ∩ b^⊥ )
146	145	lor 70	. . . . . . 7 (((a ∪ b) ∩ a^⊥ ) ∪ (b^⊥ ∩ (a ∪ b))) = (((a ∪ b) ∩ a^⊥ ) ∪ ((a ∪ b) ∩ b^⊥ ))
147		ledi 174	. . . . . . 7 (((a ∪ b) ∩ a^⊥ ) ∪ ((a ∪ b) ∩ b^⊥ )) ≤ ((a ∪ b) ∩ (a^⊥ ∪ b^⊥ ))
148	146, 147	bltr 138	. . . . . 6 (((a ∪ b) ∩ a^⊥ ) ∪ (b^⊥ ∩ (a ∪ b))) ≤ ((a ∪ b) ∩ (a^⊥ ∪ b^⊥ ))
149		ancom 74	. . . . . . . 8 (b^⊥ ∩ (b ∪ c)) = ((b ∪ c) ∩ b^⊥ )
150	149	ax-r5 38	. . . . . . 7 ((b^⊥ ∩ (b ∪ c)) ∪ ((b ∪ c) ∩ c^⊥ )) = (((b ∪ c) ∩ b^⊥ ) ∪ ((b ∪ c) ∩ c^⊥ ))
151		ledi 174	. . . . . . 7 (((b ∪ c) ∩ b^⊥ ) ∪ ((b ∪ c) ∩ c^⊥ )) ≤ ((b ∪ c) ∩ (b^⊥ ∪ c^⊥ ))
152	150, 151	bltr 138	. . . . . 6 ((b^⊥ ∩ (b ∪ c)) ∪ ((b ∪ c) ∩ c^⊥ )) ≤ ((b ∪ c) ∩ (b^⊥ ∪ c^⊥ ))
153	148, 152	le2or 168	. . . . 5 ((((a ∪ b) ∩ a^⊥ ) ∪ (b^⊥ ∩ (a ∪ b))) ∪ ((b^⊥ ∩ (b ∪ c)) ∪ ((b ∪ c) ∩ c^⊥ ))) ≤ (((a ∪ b) ∩ (a^⊥ ∪ b^⊥ )) ∪ ((b ∪ c) ∩ (b^⊥ ∪ c^⊥ )))
154	153	leror 152	. . . 4 (((((a ∪ b) ∩ a^⊥ ) ∪ (b^⊥ ∩ (a ∪ b))) ∪ ((b^⊥ ∩ (b ∪ c)) ∪ ((b ∪ c) ∩ c^⊥ ))) ∪ ((a ∩ c) ∪ (a^⊥ ∩ c^⊥ ))) ≤ ((((a ∪ b) ∩ (a^⊥ ∪ b^⊥ )) ∪ ((b ∪ c) ∩ (b^⊥ ∪ c^⊥ ))) ∪ ((a ∩ c) ∪ (a^⊥ ∩ c^⊥ )))
155	144, 154	bltr 138	. . 3 1 ≤ ((((a ∪ b) ∩ (a^⊥ ∪ b^⊥ )) ∪ ((b ∪ c) ∩ (b^⊥ ∪ c^⊥ ))) ∪ ((a ∩ c) ∪ (a^⊥ ∩ c^⊥ )))
156	8, 155	lebi 145	. 2 ((((a ∪ b) ∩ (a^⊥ ∪ b^⊥ )) ∪ ((b ∪ c) ∩ (b^⊥ ∪ c^⊥ ))) ∪ ((a ∩ c) ∪ (a^⊥ ∩ c^⊥ ))) = 1
157	5, 7, 156	3tr 65	1 ((a ≡ b)^⊥ ∪ ((b ≡ c)^⊥ ∪ (a ≡ c))) = 1

Colors of variables: term

This proof depends on syntax axioms: = wb 1 ^⊥ wn 4 ≡ tb 5 ∪ wo 6 ∩ wa 7 1wt 8

This proof depends on 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 proof 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 used by: u3lemax5 797

W3C validator