Theorem mccune2 239

Description: E2 - OL theorem proved by EQP

Assertion

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

Proof of Theorem mccune2

Step	Hyp	Ref	Expression
1		ax-a3 31	. . 3 ((a ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ ) ∪ (a ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )⊥ ) = (a ∪ (((a ∪ b⊥ ) ∩ (a ∪ b))⊥ ∪ (a ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )⊥ ))
2	1	ax-r1 34	. 2 (a ∪ (((a ∪ b⊥ ) ∩ (a ∪ b))⊥ ∪ (a ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )⊥ )) = ((a ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ ) ∪ (a ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )⊥ )
3		anor2 81	. . . . 5 (a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))) = (a ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )⊥
4		lear 153	. . . . . . 7 (a⊥ ∩ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))) ≤ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))
5		lea 152	. . . . . . . . 9 (a⊥ ∩ b) ≤ a⊥
6		lea 152	. . . . . . . . 9 (a⊥ ∩ b⊥ ) ≤ a⊥
7	5, 6	lel2or 162	. . . . . . . 8 ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) ≤ a⊥
8		id 58	. . . . . . . . 9 ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) = ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))
9	8	bile 134	. . . . . . . 8 ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) ≤ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))
10	7, 9	ler2an 165	. . . . . . 7 ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) ≤ (a⊥ ∩ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))
11	4, 10	lebi 137	. . . . . 6 (a⊥ ∩ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))) = ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))
12		anor2 81	. . . . . . . 8 (a⊥ ∩ b) = (a ∪ b⊥ )⊥
13		anor3 82	. . . . . . . 8 (a⊥ ∩ b⊥ ) = (a ∪ b)⊥
14	12, 13	2or 67	. . . . . . 7 ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) = ((a ∪ b⊥ )⊥ ∪ (a ∪ b)⊥ )
15		oran3 85	. . . . . . 7 ((a ∪ b⊥ )⊥ ∪ (a ∪ b)⊥ ) = ((a ∪ b⊥ ) ∩ (a ∪ b))⊥
16	14, 15	ax-r2 35	. . . . . 6 ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) = ((a ∪ b⊥ ) ∩ (a ∪ b))⊥
17	11, 16	ax-r2 35	. . . . 5 (a⊥ ∩ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))) = ((a ∪ b⊥ ) ∩ (a ∪ b))⊥
18	3, 17	2or 67	. . . 4 ((a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))) ∪ (a⊥ ∩ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))) = ((a ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )⊥ ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )
19		ax-a2 30	. . . 4 ((a ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )⊥ ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ ) = (((a ∪ b⊥ ) ∩ (a ∪ b))⊥ ∪ (a ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )⊥ )
20	18, 19	ax-r2 35	. . 3 ((a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))) ∪ (a⊥ ∩ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))) = (((a ∪ b⊥ ) ∩ (a ∪ b))⊥ ∪ (a ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )⊥ )
21	20	lor 66	. 2 (a ∪ ((a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))) ∪ (a⊥ ∩ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))))) = (a ∪ (((a ∪ b⊥ ) ∩ (a ∪ b))⊥ ∪ (a ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )⊥ ))
22		df-t 40	. 2 1 = ((a ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ ) ∪ (a ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )⊥ )
23	2, 21, 22	3tr1 60	1 (a ∪ ((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-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37

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

metamath.org