Theorem ka4lemo 228

Description: Lemma for KA4 soundness (OR version) - uses OL only. (Contributed by NM, 25-Oct-1997.)

Assertion

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

Proof of Theorem ka4lemo

Step	Hyp	Ref	Expression
1		le1 146	. 2 ((a ∪ b) ∪ ((a ∪ c) ≡ (b ∪ c))) ≤ 1
2		df-t 41	. . 3 1 = (((a ∪ b) ∪ c) ∪ ((a ∪ b) ∪ c)⊥ )
3		leo 158	. . . . . . 7 c ≤ (c ∪ (a ∩ b))
4		ax-a2 31	. . . . . . 7 (c ∪ (a ∩ b)) = ((a ∩ b) ∪ c)
5	3, 4	lbtr 139	. . . . . 6 c ≤ ((a ∩ b) ∪ c)
6	5	lelor 166	. . . . 5 ((a ∪ b) ∪ c) ≤ ((a ∪ b) ∪ ((a ∩ b) ∪ c))
7	6	leror 152	. . . 4 (((a ∪ b) ∪ c) ∪ ((a ∪ b) ∪ c)⊥ ) ≤ (((a ∪ b) ∪ ((a ∩ b) ∪ c)) ∪ ((a ∪ b) ∪ c)⊥ )
8		ax-a3 32	. . . . 5 (((a ∪ b) ∪ ((a ∩ b) ∪ c)) ∪ ((a ∪ b) ∪ c)⊥ ) = ((a ∪ b) ∪ (((a ∩ b) ∪ c) ∪ ((a ∪ b) ∪ c)⊥ ))
9		ledio 176	. . . . . . . . 9 (c ∪ (a ∩ b)) ≤ ((c ∪ a) ∩ (c ∪ b))
10		ax-a2 31	. . . . . . . . 9 ((a ∩ b) ∪ c) = (c ∪ (a ∩ b))
11		ax-a2 31	. . . . . . . . . 10 (a ∪ c) = (c ∪ a)
12		ax-a2 31	. . . . . . . . . 10 (b ∪ c) = (c ∪ b)
13	11, 12	2an 79	. . . . . . . . 9 ((a ∪ c) ∩ (b ∪ c)) = ((c ∪ a) ∩ (c ∪ b))
14	9, 10, 13	le3tr1 140	. . . . . . . 8 ((a ∩ b) ∪ c) ≤ ((a ∪ c) ∩ (b ∪ c))
15	14	leror 152	. . . . . . 7 (((a ∩ b) ∪ c) ∪ ((a ∪ b) ∪ c)⊥ ) ≤ (((a ∪ c) ∩ (b ∪ c)) ∪ ((a ∪ b) ∪ c)⊥ )
16		dfb 94	. . . . . . . . 9 ((a ∪ c) ≡ (b ∪ c)) = (((a ∪ c) ∩ (b ∪ c)) ∪ ((a ∪ c)⊥ ∩ (b ∪ c)⊥ ))
17		oran 87	. . . . . . . . . . . . 13 (a ∪ c) = (a⊥ ∩ c⊥ )⊥
18	17	con2 67	. . . . . . . . . . . 12 (a ∪ c)⊥ = (a⊥ ∩ c⊥ )
19		oran 87	. . . . . . . . . . . . 13 (b ∪ c) = (b⊥ ∩ c⊥ )⊥
20	19	con2 67	. . . . . . . . . . . 12 (b ∪ c)⊥ = (b⊥ ∩ c⊥ )
21	18, 20	2an 79	. . . . . . . . . . 11 ((a ∪ c)⊥ ∩ (b ∪ c)⊥ ) = ((a⊥ ∩ c⊥ ) ∩ (b⊥ ∩ c⊥ ))
22		anor1 88	. . . . . . . . . . . 12 ((a⊥ ∩ b⊥ ) ∩ c⊥ ) = ((a⊥ ∩ b⊥ )⊥ ∪ c)⊥
23		anandir 115	. . . . . . . . . . . . 13 ((a⊥ ∩ b⊥ ) ∩ c⊥ ) = ((a⊥ ∩ c⊥ ) ∩ (b⊥ ∩ c⊥ ))
24	23	ax-r1 35	. . . . . . . . . . . 12 ((a⊥ ∩ c⊥ ) ∩ (b⊥ ∩ c⊥ )) = ((a⊥ ∩ b⊥ ) ∩ c⊥ )
25		oran 87	. . . . . . . . . . . . . 14 (a ∪ b) = (a⊥ ∩ b⊥ )⊥
26	25	ax-r5 38	. . . . . . . . . . . . 13 ((a ∪ b) ∪ c) = ((a⊥ ∩ b⊥ )⊥ ∪ c)
27	26	ax-r4 37	. . . . . . . . . . . 12 ((a ∪ b) ∪ c)⊥ = ((a⊥ ∩ b⊥ )⊥ ∪ c)⊥
28	22, 24, 27	3tr1 63	. . . . . . . . . . 11 ((a⊥ ∩ c⊥ ) ∩ (b⊥ ∩ c⊥ )) = ((a ∪ b) ∪ c)⊥
29	21, 28	ax-r2 36	. . . . . . . . . 10 ((a ∪ c)⊥ ∩ (b ∪ c)⊥ ) = ((a ∪ b) ∪ c)⊥
30	29	lor 70	. . . . . . . . 9 (((a ∪ c) ∩ (b ∪ c)) ∪ ((a ∪ c)⊥ ∩ (b ∪ c)⊥ )) = (((a ∪ c) ∩ (b ∪ c)) ∪ ((a ∪ b) ∪ c)⊥ )
31	16, 30	ax-r2 36	. . . . . . . 8 ((a ∪ c) ≡ (b ∪ c)) = (((a ∪ c) ∩ (b ∪ c)) ∪ ((a ∪ b) ∪ c)⊥ )
32	31	ax-r1 35	. . . . . . 7 (((a ∪ c) ∩ (b ∪ c)) ∪ ((a ∪ b) ∪ c)⊥ ) = ((a ∪ c) ≡ (b ∪ c))
33	15, 32	lbtr 139	. . . . . 6 (((a ∩ b) ∪ c) ∪ ((a ∪ b) ∪ c)⊥ ) ≤ ((a ∪ c) ≡ (b ∪ c))
34	33	lelor 166	. . . . 5 ((a ∪ b) ∪ (((a ∩ b) ∪ c) ∪ ((a ∪ b) ∪ c)⊥ )) ≤ ((a ∪ b) ∪ ((a ∪ c) ≡ (b ∪ c)))
35	8, 34	bltr 138	. . . 4 (((a ∪ b) ∪ ((a ∩ b) ∪ c)) ∪ ((a ∪ b) ∪ c)⊥ ) ≤ ((a ∪ b) ∪ ((a ∪ c) ≡ (b ∪ c)))
36	7, 35	letr 137	. . 3 (((a ∪ b) ∪ c) ∪ ((a ∪ b) ∪ c)⊥ ) ≤ ((a ∪ b) ∪ ((a ∪ c) ≡ (b ∪ c)))
37	2, 36	bltr 138	. 2 1 ≤ ((a ∪ b) ∪ ((a ∪ c) ≡ (b ∪ c)))
38	1, 37	lebi 145	1 ((a ∪ b) ∪ ((a ∪ c) ≡ (b ∪ c))) = 1

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

This proof depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131

This theorem is used by:  ka4lem  229  ka4ot  435