Theorem wlem14 430

Description: Lemma for KA14 soundness. (Contributed by NM, 25-Oct-1997.)

Assertion

Ref	Expression
wlem14	(((a ∩ b⊥ ) ∪ a⊥ )⊥ ∪ ((a ∩ b⊥ ) ∪ ((a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))) ∪ (a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )))) = 1

Proof of Theorem wlem14

Step	Hyp	Ref	Expression
1		df-t 41	. . . 4 1 = (((a ∩ b⊥ ) ∪ a⊥ ) ∪ ((a ∩ b⊥ ) ∪ a⊥ )⊥ )
2	1	ax-r1 35	. . 3 (((a ∩ b⊥ ) ∪ a⊥ ) ∪ ((a ∩ b⊥ ) ∪ a⊥ )⊥ ) = 1
3		ax-a2 31	. . . 4 (((a ∩ b⊥ ) ∪ a⊥ )⊥ ∪ ((a ∩ b⊥ ) ∪ a⊥ )) = (((a ∩ b⊥ ) ∪ a⊥ ) ∪ ((a ∩ b⊥ ) ∪ a⊥ )⊥ )
4	3	bi1 118	. . 3 ((((a ∩ b⊥ ) ∪ a⊥ )⊥ ∪ ((a ∩ b⊥ ) ∪ a⊥ )) ≡ (((a ∩ b⊥ ) ∪ a⊥ ) ∪ ((a ∩ b⊥ ) ∪ a⊥ )⊥ )) = 1
5	2, 4	wwbmpr 206	. 2 (((a ∩ b⊥ ) ∪ a⊥ )⊥ ∪ ((a ∩ b⊥ ) ∪ a⊥ )) = 1
6		df-t 41	. . . . . . . 8 1 = (((a ∪ b⊥ ) ∩ (a ∪ b)) ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )
7	6	ax-r1 35	. . . . . . 7 (((a ∪ b⊥ ) ∩ (a ∪ b)) ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ ) = 1
8	7	bi1 118	. . . . . 6 ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ ) ≡ 1) = 1
9	8	wlan 370	. . . . 5 ((a⊥ ∩ (((a ∪ b⊥ ) ∩ (a ∪ b)) ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )) ≡ (a⊥ ∩ 1)) = 1
10		anidm 111	. . . . . . . . . . 11 (a ∩ a) = a
11	10	bi1 118	. . . . . . . . . 10 ((a ∩ a) ≡ a) = 1
12	11	wr1 197	. . . . . . . . 9 (a ≡ (a ∩ a)) = 1
13		wleo 387	. . . . . . . . . 10 (a ≤2 (a ∪ b⊥ )) = 1
14		wleo 387	. . . . . . . . . 10 (a ≤2 (a ∪ b)) = 1
15	13, 14	wle2an 404	. . . . . . . . 9 ((a ∩ a) ≤2 ((a ∪ b⊥ ) ∩ (a ∪ b))) = 1
16	12, 15	wbltr 397	. . . . . . . 8 (a ≤2 ((a ∪ b⊥ ) ∩ (a ∪ b))) = 1
17	16	wlecom 409	. . . . . . 7 C (a, ((a ∪ b⊥ ) ∩ (a ∪ b))) = 1
18	17	wcomcom3 416	. . . . . 6 C (a⊥ , ((a ∪ b⊥ ) ∩ (a ∪ b))) = 1
19	17	wcomcom4 417	. . . . . 6 C (a⊥ , ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ ) = 1
20	18, 19	wfh1 423	. . . . 5 ((a⊥ ∩ (((a ∪ b⊥ ) ∩ (a ∪ b)) ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )) ≡ ((a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))) ∪ (a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ ))) = 1
21		an1 106	. . . . . 6 (a⊥ ∩ 1) = a⊥
22	21	bi1 118	. . . . 5 ((a⊥ ∩ 1) ≡ a⊥ ) = 1
23	9, 20, 22	w3tr2 375	. . . 4 (((a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))) ∪ (a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )) ≡ a⊥ ) = 1
24	23	wlor 368	. . 3 (((a ∩ b⊥ ) ∪ ((a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))) ∪ (a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ ))) ≡ ((a ∩ b⊥ ) ∪ a⊥ )) = 1
25	24	wlor 368	. 2 ((((a ∩ b⊥ ) ∪ a⊥ )⊥ ∪ ((a ∩ b⊥ ) ∪ ((a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))) ∪ (a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )))) ≡ (((a ∩ b⊥ ) ∪ a⊥ )⊥ ∪ ((a ∩ b⊥ ) ∪ a⊥ ))) = 1
26	5, 25	wwbmpr 206	1 (((a ∩ b⊥ ) ∪ a⊥ )⊥ ∪ ((a ∩ b⊥ ) ∪ ((a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))) ∪ (a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )))) = 1

This proof depends on syntax axioms:   = wb 1  ^⊥ wn 4   ∪ 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: (None)