Theorem ka4lemo 220

Description: Lemma for KA4 soundness (OR version) - uses OL only.

Assertion

Ref	Expression
ka4lemo	((a ∪ b) ∪ ((a ∪ c) ≡ (b ∪ c))) = 1

Proof of Theorem ka4lemo

Step	Hyp	Ref	Expression
1		le1 138	. 2 ((a ∪ b) ∪ ((a ∪ c) ≡ (b ∪ c))) ≤ 1
2		df-t 40	. . 3 1 = (((a ∪ b) ∪ c) ∪ ((a ∪ b) ∪ c)⊥ )
3		leo 150	. . . . . . 7 c ≤ (c ∪ (a ∩ b))
4		ax-a2 30	. . . . . . 7 (c ∪ (a ∩ b)) = ((a ∩ b) ∪ c)
5	3, 4	lbtr 131	. . . . . 6 c ≤ ((a ∩ b) ∪ c)
6	5	lelor 158	. . . . 5 ((a ∪ b) ∪ c) ≤ ((a ∪ b) ∪ ((a ∩ b) ∪ c))
7	6	leror 144	. . . 4 (((a ∪ b) ∪ c) ∪ ((a ∪ b) ∪ c)⊥ ) ≤ (((a ∪ b) ∪ ((a ∩ b) ∪ c)) ∪ ((a ∪ b) ∪ c)⊥ )
8		ax-a3 31	. . . . 5 (((a ∪ b) ∪ ((a ∩ b) ∪ c)) ∪ ((a ∪ b) ∪ c)⊥ ) = ((a ∪ b) ∪ (((a ∩ b) ∪ c) ∪ ((a ∪ b) ∪ c)⊥ ))
9		ledio 168	. . . . . . . . 9 (c ∪ (a ∩ b)) ≤ ((c ∪ a) ∩ (c ∪ b))
10		ax-a2 30	. . . . . . . . 9 ((a ∩ b) ∪ c) = (c ∪ (a ∩ b))
11		ax-a2 30	. . . . . . . . . 10 (a ∪ c) = (c ∪ a)
12		ax-a2 30	. . . . . . . . . 10 (b ∪ c) = (c ∪ b)
13	11, 12	2an 72	. . . . . . . . 9 ((a ∪ c) ∩ (b ∪ c)) = ((c ∪ a) ∩ (c ∪ b))
14	9, 10, 13	le3tr1 132	. . . . . . . 8 ((a ∩ b) ∪ c) ≤ ((a ∪ c) ∩ (b ∪ c))
15	14	leror 144	. . . . . . 7 (((a ∩ b) ∪ c) ∪ ((a ∪ b) ∪ c)⊥ ) ≤ (((a ∪ c) ∩ (b ∪ c)) ∪ ((a ∪ b) ∪ c)⊥ )
16		dfb 86	. . . . . . . . 9 ((a ∪ c) ≡ (b ∪ c)) = (((a ∪ c) ∩ (b ∪ c)) ∪ ((a ∪ c)⊥ ∩ (b ∪ c)⊥ ))
17		oran 79	. . . . . . . . . . . . 13 (a ∪ c) = (a⊥ ∩ c⊥ )⊥
18	17	con2 64	. . . . . . . . . . . 12 (a ∪ c)⊥ = (a⊥ ∩ c⊥ )
19		oran 79	. . . . . . . . . . . . 13 (b ∪ c) = (b⊥ ∩ c⊥ )⊥
20	19	con2 64	. . . . . . . . . . . 12 (b ∪ c)⊥ = (b⊥ ∩ c⊥ )
21	18, 20	2an 72	. . . . . . . . . . 11 ((a ∪ c)⊥ ∩ (b ∪ c)⊥ ) = ((a⊥ ∩ c⊥ ) ∩ (b⊥ ∩ c⊥ ))
22		anor1 80	. . . . . . . . . . . 12 ((a⊥ ∩ b⊥ ) ∩ c⊥ ) = ((a⊥ ∩ b⊥ )⊥ ∪ c)⊥
23		anandir 107	. . . . . . . . . . . . 13 ((a⊥ ∩ b⊥ ) ∩ c⊥ ) = ((a⊥ ∩ c⊥ ) ∩ (b⊥ ∩ c⊥ ))
24	23	ax-r1 34	. . . . . . . . . . . 12 ((a⊥ ∩ c⊥ ) ∩ (b⊥ ∩ c⊥ )) = ((a⊥ ∩ b⊥ ) ∩ c⊥ )
25		oran 79	. . . . . . . . . . . . . 14 (a ∪ b) = (a⊥ ∩ b⊥ )⊥
26	25	ax-r5 37	. . . . . . . . . . . . 13 ((a ∪ b) ∪ c) = ((a⊥ ∩ b⊥ )⊥ ∪ c)
27	26	ax-r4 36	. . . . . . . . . . . 12 ((a ∪ b) ∪ c)⊥ = ((a⊥ ∩ b⊥ )⊥ ∪ c)⊥
28	22, 24, 27	3tr1 60	. . . . . . . . . . 11 ((a⊥ ∩ c⊥ ) ∩ (b⊥ ∩ c⊥ )) = ((a ∪ b) ∪ c)⊥
29	21, 28	ax-r2 35	. . . . . . . . . 10 ((a ∪ c)⊥ ∩ (b ∪ c)⊥ ) = ((a ∪ b) ∪ c)⊥
30	29	lor 66	. . . . . . . . 9 (((a ∪ c) ∩ (b ∪ c)) ∪ ((a ∪ c)⊥ ∩ (b ∪ c)⊥ )) = (((a ∪ c) ∩ (b ∪ c)) ∪ ((a ∪ b) ∪ c)⊥ )
31	16, 30	ax-r2 35	. . . . . . . 8 ((a ∪ c) ≡ (b ∪ c)) = (((a ∪ c) ∩ (b ∪ c)) ∪ ((a ∪ b) ∪ c)⊥ )
32	31	ax-r1 34	. . . . . . 7 (((a ∪ c) ∩ (b ∪ c)) ∪ ((a ∪ b) ∪ c)⊥ ) = ((a ∪ c) ≡ (b ∪ c))
33	15, 32	lbtr 131	. . . . . 6 (((a ∩ b) ∪ c) ∪ ((a ∪ b) ∪ c)⊥ ) ≤ ((a ∪ c) ≡ (b ∪ c))
34	33	lelor 158	. . . . 5 ((a ∪ b) ∪ (((a ∩ b) ∪ c) ∪ ((a ∪ b) ∪ c)⊥ )) ≤ ((a ∪ b) ∪ ((a ∪ c) ≡ (b ∪ c)))
35	8, 34	bltr 130	. . . 4 (((a ∪ b) ∪ ((a ∩ b) ∪ c)) ∪ ((a ∪ b) ∪ c)⊥ ) ≤ ((a ∪ b) ∪ ((a ∪ c) ≡ (b ∪ c)))
36	7, 35	letr 129	. . 3 (((a ∪ b) ∪ c) ∪ ((a ∪ b) ∪ c)⊥ ) ≤ ((a ∪ b) ∪ ((a ∪ c) ≡ (b ∪ c)))
37	2, 36	bltr 130	. 2 1 ≤ ((a ∪ b) ∪ ((a ∪ c) ≡ (b ∪ c)))
38	1, 37	lebi 137	1 ((a ∪ b) ∪ ((a ∪ c) ≡ (b ∪ c))) = 1

Syntax hints:   = wb 1  ^⊥ wn 4   ≡ tb 5   ∪ wo 6   ∩ wa 7  1wt 9

This theorem is referenced by:  ka4lem 221  wr5 413  ka4ot 417

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a3 31  ax-a4 32  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-le1 122  df-le2 123

metamath.org