Theorem mccune2 247

Description: E2 - OL theorem proved by EQP. (Contributed by NM, 14-Nov-1998.)

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 32	. . 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 35	. 2 (a ∪ (((a ∪ b⊥ ) ∩ (a ∪ b))⊥ ∪ (a ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )⊥ )) = ((a ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ ) ∪ (a ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )⊥ )
3		anor2 89	. . . . 5 (a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))) = (a ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )⊥
4		lear 161	. . . . . . 7 (a⊥ ∩ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))) ≤ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))
5		lea 160	. . . . . . . . 9 (a⊥ ∩ b) ≤ a⊥
6		lea 160	. . . . . . . . 9 (a⊥ ∩ b⊥ ) ≤ a⊥
7	5, 6	lel2or 170	. . . . . . . 8 ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) ≤ a⊥
8		id 59	. . . . . . . . 9 ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) = ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))
9	8	bile 142	. . . . . . . 8 ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) ≤ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))
10	7, 9	ler2an 173	. . . . . . 7 ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) ≤ (a⊥ ∩ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))
11	4, 10	lebi 145	. . . . . 6 (a⊥ ∩ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))) = ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))
12		anor2 89	. . . . . . . 8 (a⊥ ∩ b) = (a ∪ b⊥ )⊥
13		anor3 90	. . . . . . . 8 (a⊥ ∩ b⊥ ) = (a ∪ b)⊥
14	12, 13	2or 72	. . . . . . 7 ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) = ((a ∪ b⊥ )⊥ ∪ (a ∪ b)⊥ )
15		oran3 93	. . . . . . 7 ((a ∪ b⊥ )⊥ ∪ (a ∪ b)⊥ ) = ((a ∪ b⊥ ) ∩ (a ∪ b))⊥
16	14, 15	ax-r2 36	. . . . . 6 ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) = ((a ∪ b⊥ ) ∩ (a ∪ b))⊥
17	11, 16	ax-r2 36	. . . . 5 (a⊥ ∩ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))) = ((a ∪ b⊥ ) ∩ (a ∪ b))⊥
18	3, 17	2or 72	. . . 4 ((a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))) ∪ (a⊥ ∩ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))) = ((a ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )⊥ ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )
19		ax-a2 31	. . . 4 ((a ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )⊥ ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ ) = (((a ∪ b⊥ ) ∩ (a ∪ b))⊥ ∪ (a ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )⊥ )
20	18, 19	ax-r2 36	. . 3 ((a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))) ∪ (a⊥ ∩ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))) = (((a ∪ b⊥ ) ∩ (a ∪ b))⊥ ∪ (a ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )⊥ )
21	20	lor 70	. 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 41	. 2 1 = ((a ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ ) ∪ (a ∪ ((a ∪ b⊥ ) ∩ (a ∪ b))⊥ )⊥ )
23	2, 21, 22	3tr1 63	1 (a ∪ ((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-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

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

This theorem is used by: (None)