Theorem oas 925

Description: "Strengthening" lemma for studying the orthoarguesian law. (Contributed by NM, 25-Dec-1998.)

Hypothesis

Ref	Expression
oas.1	(a⊥ ∩ (a ∪ b)) ≤ c

Assertion

Ref	Expression
oas	((a →1 c) ∩ (a ∪ b)) ≤ c

Proof of Theorem oas

Step	Hyp	Ref	Expression
1		oml 445	. . . . . 6 (a ∪ (a⊥ ∩ (a ∪ b))) = (a ∪ b)
2	1	ax-r1 35	. . . . 5 (a ∪ b) = (a ∪ (a⊥ ∩ (a ∪ b)))
3		lea 160	. . . . . . 7 (a⊥ ∩ (a ∪ b)) ≤ a⊥
4		oas.1	. . . . . . 7 (a⊥ ∩ (a ∪ b)) ≤ c
5	3, 4	ler2an 173	. . . . . 6 (a⊥ ∩ (a ∪ b)) ≤ (a⊥ ∩ c)
6	5	lelor 166	. . . . 5 (a ∪ (a⊥ ∩ (a ∪ b))) ≤ (a ∪ (a⊥ ∩ c))
7	2, 6	bltr 138	. . . 4 (a ∪ b) ≤ (a ∪ (a⊥ ∩ c))
8	7	lelan 167	. . 3 ((a →1 c) ∩ (a ∪ b)) ≤ ((a →1 c) ∩ (a ∪ (a⊥ ∩ c)))
9		u1lemc1 680	. . . . 5 a C (a →1 c)
10		comanr1 464	. . . . . 6 a⊥ C (a⊥ ∩ c)
11	10	comcom6 459	. . . . 5 a C (a⊥ ∩ c)
12	9, 11	fh2 470	. . . 4 ((a →1 c) ∩ (a ∪ (a⊥ ∩ c))) = (((a →1 c) ∩ a) ∪ ((a →1 c) ∩ (a⊥ ∩ c)))
13		u1lemaa 600	. . . . 5 ((a →1 c) ∩ a) = (a ∩ c)
14		ancom 74	. . . . . 6 ((a →1 c) ∩ (a⊥ ∩ c)) = ((a⊥ ∩ c) ∩ (a →1 c))
15		lea 160	. . . . . . . 8 (a⊥ ∩ c) ≤ a⊥
16		leo 158	. . . . . . . . 9 a⊥ ≤ (a⊥ ∪ (a ∩ c))
17		df-i1 44	. . . . . . . . . 10 (a →1 c) = (a⊥ ∪ (a ∩ c))
18	17	ax-r1 35	. . . . . . . . 9 (a⊥ ∪ (a ∩ c)) = (a →1 c)
19	16, 18	lbtr 139	. . . . . . . 8 a⊥ ≤ (a →1 c)
20	15, 19	letr 137	. . . . . . 7 (a⊥ ∩ c) ≤ (a →1 c)
21	20	df2le2 136	. . . . . 6 ((a⊥ ∩ c) ∩ (a →1 c)) = (a⊥ ∩ c)
22	14, 21	ax-r2 36	. . . . 5 ((a →1 c) ∩ (a⊥ ∩ c)) = (a⊥ ∩ c)
23	13, 22	2or 72	. . . 4 (((a →1 c) ∩ a) ∪ ((a →1 c) ∩ (a⊥ ∩ c))) = ((a ∩ c) ∪ (a⊥ ∩ c))
24	12, 23	ax-r2 36	. . 3 ((a →1 c) ∩ (a ∪ (a⊥ ∩ c))) = ((a ∩ c) ∪ (a⊥ ∩ c))
25	8, 24	lbtr 139	. 2 ((a →1 c) ∩ (a ∪ b)) ≤ ((a ∩ c) ∪ (a⊥ ∩ c))
26		lear 161	. . 3 (a ∩ c) ≤ c
27		lear 161	. . 3 (a⊥ ∩ c) ≤ c
28	26, 27	lel2or 170	. 2 ((a ∩ c) ∪ (a⊥ ∩ c)) ≤ c
29	25, 28	letr 137	1 ((a →1 c) ∩ (a ∪ b)) ≤ c

Syntax hints:   ≤ wle 2  ^⊥ wn 4   ∪ wo 6   ∩ wa 7   →₁ wi1 12

This theorem was proved from 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-r3 439

This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is referenced by:  oa4ctob  967  oa3-2wto2  989