Theorem wlem14 412

Description: Lemma for KA14 soundness.

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 40	. . . 4 1 = (((a ∩ b⊥ ) ∪ a⊥ ) ∪ ((a ∩ b⊥ ) ∪ a⊥ )⊥ )
2	1	ax-r1 34	. . 3 (((a ∩ b⊥ ) ∪ a⊥ ) ∪ ((a ∩ b⊥ ) ∪ a⊥ )⊥ ) = 1
3		ax-a2 30	. . . 4 (((a ∩ b⊥ ) ∪ a⊥ )⊥ ∪ ((a ∩ b⊥ ) ∪ a⊥ )) = (((a ∩ b⊥ ) ∪ a⊥ ) ∪ ((a ∩ b⊥ ) ∪ a⊥ )⊥ )
4	3	bi1 110	. . 3 ((((a ∩ b⊥ ) ∪ a⊥ )⊥ ∪ ((a ∩ b⊥ ) ∪ a⊥ )) ≡ (((a ∩ b⊥ ) ∪ a⊥ ) ∪ ((a ∩ b⊥ ) ∪ a⊥ )⊥ )) = 1
5	2, 4	wwbmpr 198	. 2 (((a ∩ b⊥ ) ∪ a⊥ )⊥ ∪ ((a ∩ b⊥ ) ∪ a⊥ )) = 1
6		df-t 40	. . . . . . . 8 1 = (((a ∪ b⊥ ) ∩ (a ∪ b)) ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )
7	6	ax-r1 34	. . . . . . 7 (((a ∪ b⊥ ) ∩ (a ∪ b)) ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ ) = 1
8	7	bi1 110	. . . . . 6 ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ ) ≡ 1) = 1
9	8	wlan 352	. . . . 5 ((a⊥ ∩ (((a ∪ b⊥ ) ∩ (a ∪ b)) ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )) ≡ (a⊥ ∩ 1)) = 1
10		anidm 103	. . . . . . . . . . 11 (a ∩ a) = a
11	10	bi1 110	. . . . . . . . . 10 ((a ∩ a) ≡ a) = 1
12	11	wr1 189	. . . . . . . . 9 (a ≡ (a ∩ a)) = 1
13		wleo 369	. . . . . . . . . 10 (a ≤2 (a ∪ b⊥ )) = 1
14		wleo 369	. . . . . . . . . 10 (a ≤2 (a ∪ b)) = 1
15	13, 14	wle2an 386	. . . . . . . . 9 ((a ∩ a) ≤2 ((a ∪ b⊥ ) ∩ (a ∪ b))) = 1
16	12, 15	wbltr 379	. . . . . . . 8 (a ≤2 ((a ∪ b⊥ ) ∩ (a ∪ b))) = 1
17	16	wlecom 391	. . . . . . 7 C (a, ((a ∪ b⊥ ) ∩ (a ∪ b))) = 1
18	17	wcomcom3 398	. . . . . 6 C (a⊥ , ((a ∪ b⊥ ) ∩ (a ∪ b))) = 1
19	17	wcomcom4 399	. . . . . 6 C (a⊥ , ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ ) = 1
20	18, 19	wfh1 405	. . . . 5 ((a⊥ ∩ (((a ∪ b⊥ ) ∩ (a ∪ b)) ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )) ≡ ((a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))) ∪ (a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ ))) = 1
21		an1 98	. . . . . 6 (a⊥ ∩ 1) = a⊥
22	21	bi1 110	. . . . 5 ((a⊥ ∩ 1) ≡ a⊥ ) = 1
23	9, 20, 22	w3tr2 357	. . . 4 (((a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))) ∪ (a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )) ≡ a⊥ ) = 1
24	23	wlor 350	. . 3 (((a ∩ b⊥ ) ∪ ((a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))) ∪ (a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ ))) ≡ ((a ∩ b⊥ ) ∪ a⊥ )) = 1
25	24	wlor 350	. 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 198	1 (((a ∩ b⊥ ) ∪ a⊥ )⊥ ∪ ((a ∩ b⊥ ) ∪ ((a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))) ∪ (a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )))) = 1

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

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  ax-wom 343

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-i1 43  df-i2 44  df-le 121  df-le1 122  df-le2 123  df-cmtr 126

metamath.org