Theorem elimconslem 849

Description: Lemma for consequent elimination law.

Hypotheses

Ref	Expression
elimcons.1	(a →1 c) = (b →1 c)
elimcons.2	(a ∩ c) ≤ (b ∪ c⊥ )

Assertion

Ref	Expression
elimconslem	a ≤ (b ∪ c⊥ )

Proof of Theorem elimconslem

Step	Hyp	Ref	Expression
1		df-t 40	. . . . . . 7 1 = ((b ∪ c⊥ ) ∪ (b ∪ c⊥ )⊥ )
2		elimcons.2	. . . . . . . . . 10 (a ∩ c) ≤ (b ∪ c⊥ )
3	2	lecon 146	. . . . . . . . 9 (b ∪ c⊥ )⊥ ≤ (a ∩ c)⊥
4		oran3 85	. . . . . . . . . 10 (a⊥ ∪ c⊥ ) = (a ∩ c)⊥
5	4	ax-r1 34	. . . . . . . . 9 (a ∩ c)⊥ = (a⊥ ∪ c⊥ )
6	3, 5	lbtr 131	. . . . . . . 8 (b ∪ c⊥ )⊥ ≤ (a⊥ ∪ c⊥ )
7	6	lelor 158	. . . . . . 7 ((b ∪ c⊥ ) ∪ (b ∪ c⊥ )⊥ ) ≤ ((b ∪ c⊥ ) ∪ (a⊥ ∪ c⊥ ))
8	1, 7	bltr 130	. . . . . 6 1 ≤ ((b ∪ c⊥ ) ∪ (a⊥ ∪ c⊥ ))
9	8	lelan 159	. . . . 5 (a ∩ 1) ≤ (a ∩ ((b ∪ c⊥ ) ∪ (a⊥ ∪ c⊥ )))
10		an1 98	. . . . 5 (a ∩ 1) = a
11		comor1 443	. . . . . . 7 (a⊥ ∪ c⊥ ) C a⊥
12	11	comcom7 442	. . . . . 6 (a⊥ ∪ c⊥ ) C a
13		df-a 39	. . . . . . . . . 10 (a ∩ c) = (a⊥ ∪ c⊥ )⊥
14	13	ax-r1 34	. . . . . . . . 9 (a⊥ ∪ c⊥ )⊥ = (a ∩ c)
15	14, 2	bltr 130	. . . . . . . 8 (a⊥ ∪ c⊥ )⊥ ≤ (b ∪ c⊥ )
16	15	lecom 172	. . . . . . 7 (a⊥ ∪ c⊥ )⊥ C (b ∪ c⊥ )
17	16	comcom6 441	. . . . . 6 (a⊥ ∪ c⊥ ) C (b ∪ c⊥ )
18	12, 17	fh2c 459	. . . . 5 (a ∩ ((b ∪ c⊥ ) ∪ (a⊥ ∪ c⊥ ))) = ((a ∩ (b ∪ c⊥ )) ∪ (a ∩ (a⊥ ∪ c⊥ )))
19	9, 10, 18	le3tr2 133	. . . 4 a ≤ ((a ∩ (b ∪ c⊥ )) ∪ (a ∩ (a⊥ ∪ c⊥ )))
20		elimcons.1	. . . . . . . . 9 (a →1 c) = (b →1 c)
21		df-i1 43	. . . . . . . . 9 (a →1 c) = (a⊥ ∪ (a ∩ c))
22		df-i1 43	. . . . . . . . 9 (b →1 c) = (b⊥ ∪ (b ∩ c))
23	20, 21, 22	3tr2 61	. . . . . . . 8 (a⊥ ∪ (a ∩ c)) = (b⊥ ∪ (b ∩ c))
24	13	lor 66	. . . . . . . 8 (a⊥ ∪ (a ∩ c)) = (a⊥ ∪ (a⊥ ∪ c⊥ )⊥ )
25		df-a 39	. . . . . . . . 9 (b ∩ c) = (b⊥ ∪ c⊥ )⊥
26	25	lor 66	. . . . . . . 8 (b⊥ ∪ (b ∩ c)) = (b⊥ ∪ (b⊥ ∪ c⊥ )⊥ )
27	23, 24, 26	3tr2 61	. . . . . . 7 (a⊥ ∪ (a⊥ ∪ c⊥ )⊥ ) = (b⊥ ∪ (b⊥ ∪ c⊥ )⊥ )
28	27	ax-r4 36	. . . . . 6 (a⊥ ∪ (a⊥ ∪ c⊥ )⊥ )⊥ = (b⊥ ∪ (b⊥ ∪ c⊥ )⊥ )⊥
29		df-a 39	. . . . . 6 (a ∩ (a⊥ ∪ c⊥ )) = (a⊥ ∪ (a⊥ ∪ c⊥ )⊥ )⊥
30		df-a 39	. . . . . 6 (b ∩ (b⊥ ∪ c⊥ )) = (b⊥ ∪ (b⊥ ∪ c⊥ )⊥ )⊥
31	28, 29, 30	3tr1 60	. . . . 5 (a ∩ (a⊥ ∪ c⊥ )) = (b ∩ (b⊥ ∪ c⊥ ))
32	31	lor 66	. . . 4 ((a ∩ (b ∪ c⊥ )) ∪ (a ∩ (a⊥ ∪ c⊥ ))) = ((a ∩ (b ∪ c⊥ )) ∪ (b ∩ (b⊥ ∪ c⊥ )))
33	19, 32	lbtr 131	. . 3 a ≤ ((a ∩ (b ∪ c⊥ )) ∪ (b ∩ (b⊥ ∪ c⊥ )))
34		lear 153	. . . 4 (a ∩ (b ∪ c⊥ )) ≤ (b ∪ c⊥ )
35	34	leror 144	. . 3 ((a ∩ (b ∪ c⊥ )) ∪ (b ∩ (b⊥ ∪ c⊥ ))) ≤ ((b ∪ c⊥ ) ∪ (b ∩ (b⊥ ∪ c⊥ )))
36	33, 35	letr 129	. 2 a ≤ ((b ∪ c⊥ ) ∪ (b ∩ (b⊥ ∪ c⊥ )))
37		ax-a2 30	. . 3 ((b ∪ c⊥ ) ∪ (b ∩ (b⊥ ∪ c⊥ ))) = ((b ∩ (b⊥ ∪ c⊥ )) ∪ (b ∪ c⊥ ))
38		leao1 154	. . . 4 (b ∩ (b⊥ ∪ c⊥ )) ≤ (b ∪ c⊥ )
39	38	df-le2 123	. . 3 ((b ∩ (b⊥ ∪ c⊥ )) ∪ (b ∪ c⊥ )) = (b ∪ c⊥ )
40	37, 39	ax-r2 35	. 2 ((b ∪ c⊥ ) ∪ (b ∩ (b⊥ ∪ c⊥ ))) = (b ∪ c⊥ )
41	36, 40	lbtr 131	1 a ≤ (b ∪ c⊥ )

Syntax hints:   = wb 1   ≤ wle 2  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 9   →₁ wi1 13

This theorem is referenced by:  elimcons 850

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-r3 421

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-i1 43  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org