Theorem elimcons 850

Description: Consequent elimination law.

Hypotheses

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

Assertion

Ref	Expression
elimcons	a ≤ b

Proof of Theorem elimcons

Step	Hyp	Ref	Expression
1		df-t 40	. . . . . . . 8 1 = (a ∪ a⊥ )
2		elimcons.1	. . . . . . . . . 10 (a →1 c) = (b →1 c)
3		elimcons.2	. . . . . . . . . 10 (a ∩ c) ≤ (b ∪ c⊥ )
4	2, 3	elimconslem 849	. . . . . . . . 9 a ≤ (b ∪ c⊥ )
5	4	leror 144	. . . . . . . 8 (a ∪ a⊥ ) ≤ ((b ∪ c⊥ ) ∪ a⊥ )
6	1, 5	bltr 130	. . . . . . 7 1 ≤ ((b ∪ c⊥ ) ∪ a⊥ )
7	6	lelan 159	. . . . . 6 (b⊥ ∩ 1) ≤ (b⊥ ∩ ((b ∪ c⊥ ) ∪ a⊥ ))
8		an1 98	. . . . . 6 (b⊥ ∩ 1) = b⊥
9		comor1 443	. . . . . . . 8 (b ∪ c⊥ ) C b
10	9	comcom2 175	. . . . . . 7 (b ∪ c⊥ ) C b⊥
11	4	lecom 172	. . . . . . . . 9 a C (b ∪ c⊥ )
12	11	comcom3 436	. . . . . . . 8 a⊥ C (b ∪ c⊥ )
13	12	comcom 435	. . . . . . 7 (b ∪ c⊥ ) C a⊥
14	10, 13	fh2 452	. . . . . 6 (b⊥ ∩ ((b ∪ c⊥ ) ∪ a⊥ )) = ((b⊥ ∩ (b ∪ c⊥ )) ∪ (b⊥ ∩ a⊥ ))
15	7, 8, 14	le3tr2 133	. . . . 5 b⊥ ≤ ((b⊥ ∩ (b ∪ c⊥ )) ∪ (b⊥ ∩ a⊥ ))
16	2	negant 834	. . . . . . . . . . 11 (a⊥ →1 c) = (b⊥ →1 c)
17		df-i1 43	. . . . . . . . . . 11 (a⊥ →1 c) = (a⊥ ⊥ ∪ (a⊥ ∩ c))
18		df-i1 43	. . . . . . . . . . 11 (b⊥ →1 c) = (b⊥ ⊥ ∪ (b⊥ ∩ c))
19	16, 17, 18	3tr2 61	. . . . . . . . . 10 (a⊥ ⊥ ∪ (a⊥ ∩ c)) = (b⊥ ⊥ ∪ (b⊥ ∩ c))
20		anor2 81	. . . . . . . . . . 11 (a⊥ ∩ c) = (a ∪ c⊥ )⊥
21	20	lor 66	. . . . . . . . . 10 (a⊥ ⊥ ∪ (a⊥ ∩ c)) = (a⊥ ⊥ ∪ (a ∪ c⊥ )⊥ )
22		anor2 81	. . . . . . . . . . 11 (b⊥ ∩ c) = (b ∪ c⊥ )⊥
23	22	lor 66	. . . . . . . . . 10 (b⊥ ⊥ ∪ (b⊥ ∩ c)) = (b⊥ ⊥ ∪ (b ∪ c⊥ )⊥ )
24	19, 21, 23	3tr2 61	. . . . . . . . 9 (a⊥ ⊥ ∪ (a ∪ c⊥ )⊥ ) = (b⊥ ⊥ ∪ (b ∪ c⊥ )⊥ )
25	24	ax-r1 34	. . . . . . . 8 (b⊥ ⊥ ∪ (b ∪ c⊥ )⊥ ) = (a⊥ ⊥ ∪ (a ∪ c⊥ )⊥ )
26	25	ax-r4 36	. . . . . . 7 (b⊥ ⊥ ∪ (b ∪ c⊥ )⊥ )⊥ = (a⊥ ⊥ ∪ (a ∪ c⊥ )⊥ )⊥
27		df-a 39	. . . . . . 7 (b⊥ ∩ (b ∪ c⊥ )) = (b⊥ ⊥ ∪ (b ∪ c⊥ )⊥ )⊥
28		df-a 39	. . . . . . 7 (a⊥ ∩ (a ∪ c⊥ )) = (a⊥ ⊥ ∪ (a ∪ c⊥ )⊥ )⊥
29	26, 27, 28	3tr1 60	. . . . . 6 (b⊥ ∩ (b ∪ c⊥ )) = (a⊥ ∩ (a ∪ c⊥ ))
30	29	ax-r5 37	. . . . 5 ((b⊥ ∩ (b ∪ c⊥ )) ∪ (b⊥ ∩ a⊥ )) = ((a⊥ ∩ (a ∪ c⊥ )) ∪ (b⊥ ∩ a⊥ ))
31	15, 30	lbtr 131	. . . 4 b⊥ ≤ ((a⊥ ∩ (a ∪ c⊥ )) ∪ (b⊥ ∩ a⊥ ))
32		lear 153	. . . . 5 (b⊥ ∩ a⊥ ) ≤ a⊥
33	32	lelor 158	. . . 4 ((a⊥ ∩ (a ∪ c⊥ )) ∪ (b⊥ ∩ a⊥ )) ≤ ((a⊥ ∩ (a ∪ c⊥ )) ∪ a⊥ )
34	31, 33	letr 129	. . 3 b⊥ ≤ ((a⊥ ∩ (a ∪ c⊥ )) ∪ a⊥ )
35		lea 152	. . . 4 (a⊥ ∩ (a ∪ c⊥ )) ≤ a⊥
36	35	df-le2 123	. . 3 ((a⊥ ∩ (a ∪ c⊥ )) ∪ a⊥ ) = a⊥
37	34, 36	lbtr 131	. 2 b⊥ ≤ a⊥
38	37	lecon1 147	1 a ≤ b

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

This theorem is referenced by:  elimcons2 851

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