Theorem cancellem 891

Description: Lemma for cancellation law eliminating →₁ consequent. (Contributed by NM, 21-Feb-2002.)

Hypothesis

Ref	Expression
cancel.1	((d ∪ (a →1 c)) →1 c) = ((d ∪ (b →1 c)) →1 c)

Assertion

Ref	Expression
cancellem	(d ∪ (a →1 c)) ≤ (d ∪ (b →1 c))

Proof of Theorem cancellem

Step	Hyp	Ref	Expression
1		i1abs 801	. . 3 (((d ∪ (a →1 c)) →1 c)⊥ ∪ ((d ∪ (a →1 c)) ∩ c)) = (d ∪ (a →1 c))
2	1	ax-r1 35	. 2 (d ∪ (a →1 c)) = (((d ∪ (a →1 c)) →1 c)⊥ ∪ ((d ∪ (a →1 c)) ∩ c))
3		leo 158	. . . . 5 (d ∪ (b →1 c))⊥ ≤ ((d ∪ (b →1 c))⊥ ∪ ((d ∪ (b →1 c)) ∩ c))
4		cancel.1	. . . . . . 7 ((d ∪ (a →1 c)) →1 c) = ((d ∪ (b →1 c)) →1 c)
5		df-i1 44	. . . . . . 7 ((d ∪ (b →1 c)) →1 c) = ((d ∪ (b →1 c))⊥ ∪ ((d ∪ (b →1 c)) ∩ c))
6	4, 5	ax-r2 36	. . . . . 6 ((d ∪ (a →1 c)) →1 c) = ((d ∪ (b →1 c))⊥ ∪ ((d ∪ (b →1 c)) ∩ c))
7	6	ax-r1 35	. . . . 5 ((d ∪ (b →1 c))⊥ ∪ ((d ∪ (b →1 c)) ∩ c)) = ((d ∪ (a →1 c)) →1 c)
8	3, 7	lbtr 139	. . . 4 (d ∪ (b →1 c))⊥ ≤ ((d ∪ (a →1 c)) →1 c)
9	8	lecon2 156	. . 3 ((d ∪ (a →1 c)) →1 c)⊥ ≤ (d ∪ (b →1 c))
10		leor 159	. . . . . 6 ((d ∪ (a →1 c)) ∩ c) ≤ ((d ∪ (a →1 c))⊥ ∪ ((d ∪ (a →1 c)) ∩ c))
11		df-i1 44	. . . . . . . 8 ((d ∪ (a →1 c)) →1 c) = ((d ∪ (a →1 c))⊥ ∪ ((d ∪ (a →1 c)) ∩ c))
12	11	ax-r1 35	. . . . . . 7 ((d ∪ (a →1 c))⊥ ∪ ((d ∪ (a →1 c)) ∩ c)) = ((d ∪ (a →1 c)) →1 c)
13	12, 4	ax-r2 36	. . . . . 6 ((d ∪ (a →1 c))⊥ ∪ ((d ∪ (a →1 c)) ∩ c)) = ((d ∪ (b →1 c)) →1 c)
14	10, 13	lbtr 139	. . . . 5 ((d ∪ (a →1 c)) ∩ c) ≤ ((d ∪ (b →1 c)) →1 c)
15		lear 161	. . . . 5 ((d ∪ (a →1 c)) ∩ c) ≤ c
16	14, 15	ler2an 173	. . . 4 ((d ∪ (a →1 c)) ∩ c) ≤ (((d ∪ (b →1 c)) →1 c) ∩ c)
17		coman2 186	. . . . . . 7 ((d ∪ (b →1 c)) ∩ c) C c
18		coman1 185	. . . . . . . 8 ((d ∪ (b →1 c)) ∩ c) C (d ∪ (b →1 c))
19	18	comcom2 183	. . . . . . 7 ((d ∪ (b →1 c)) ∩ c) C (d ∪ (b →1 c))⊥
20	17, 19	fh2rc 480	. . . . . 6 (((d ∪ (b →1 c))⊥ ∪ ((d ∪ (b →1 c)) ∩ c)) ∩ c) = (((d ∪ (b →1 c))⊥ ∩ c) ∪ (((d ∪ (b →1 c)) ∩ c) ∩ c))
21	5	ran 78	. . . . . 6 (((d ∪ (b →1 c)) →1 c) ∩ c) = (((d ∪ (b →1 c))⊥ ∪ ((d ∪ (b →1 c)) ∩ c)) ∩ c)
22		id 59	. . . . . 6 (((d ∪ (b →1 c))⊥ ∩ c) ∪ (((d ∪ (b →1 c)) ∩ c) ∩ c)) = (((d ∪ (b →1 c))⊥ ∩ c) ∪ (((d ∪ (b →1 c)) ∩ c) ∩ c))
23	20, 21, 22	3tr1 63	. . . . 5 (((d ∪ (b →1 c)) →1 c) ∩ c) = (((d ∪ (b →1 c))⊥ ∩ c) ∪ (((d ∪ (b →1 c)) ∩ c) ∩ c))
24		leao4 165	. . . . . . . 8 ((d⊥ ∩ (b ∩ c)⊥ ) ∩ (b ∩ c)) ≤ (b⊥ ∪ (b ∩ c))
25	24	lerr 150	. . . . . . 7 ((d⊥ ∩ (b ∩ c)⊥ ) ∩ (b ∩ c)) ≤ (d ∪ (b⊥ ∪ (b ∩ c)))
26		df-i1 44	. . . . . . . . . . . 12 (b →1 c) = (b⊥ ∪ (b ∩ c))
27	26	lor 70	. . . . . . . . . . 11 (d ∪ (b →1 c)) = (d ∪ (b⊥ ∪ (b ∩ c)))
28	27	ax-r4 37	. . . . . . . . . 10 (d ∪ (b →1 c))⊥ = (d ∪ (b⊥ ∪ (b ∩ c)))⊥
29		an12 81	. . . . . . . . . . . 12 (b ∩ (d⊥ ∩ (b ∩ c)⊥ )) = (d⊥ ∩ (b ∩ (b ∩ c)⊥ ))
30		anor1 88	. . . . . . . . . . . . 13 (b ∩ (b ∩ c)⊥ ) = (b⊥ ∪ (b ∩ c))⊥
31	30	lan 77	. . . . . . . . . . . 12 (d⊥ ∩ (b ∩ (b ∩ c)⊥ )) = (d⊥ ∩ (b⊥ ∪ (b ∩ c))⊥ )
32		anor3 90	. . . . . . . . . . . 12 (d⊥ ∩ (b⊥ ∪ (b ∩ c))⊥ ) = (d ∪ (b⊥ ∪ (b ∩ c)))⊥
33	29, 31, 32	3tr 65	. . . . . . . . . . 11 (b ∩ (d⊥ ∩ (b ∩ c)⊥ )) = (d ∪ (b⊥ ∪ (b ∩ c)))⊥
34	33	ax-r1 35	. . . . . . . . . 10 (d ∪ (b⊥ ∪ (b ∩ c)))⊥ = (b ∩ (d⊥ ∩ (b ∩ c)⊥ ))
35		ancom 74	. . . . . . . . . 10 (b ∩ (d⊥ ∩ (b ∩ c)⊥ )) = ((d⊥ ∩ (b ∩ c)⊥ ) ∩ b)
36	28, 34, 35	3tr 65	. . . . . . . . 9 (d ∪ (b →1 c))⊥ = ((d⊥ ∩ (b ∩ c)⊥ ) ∩ b)
37	36	ran 78	. . . . . . . 8 ((d ∪ (b →1 c))⊥ ∩ c) = (((d⊥ ∩ (b ∩ c)⊥ ) ∩ b) ∩ c)
38		anass 76	. . . . . . . 8 (((d⊥ ∩ (b ∩ c)⊥ ) ∩ b) ∩ c) = ((d⊥ ∩ (b ∩ c)⊥ ) ∩ (b ∩ c))
39	37, 38	ax-r2 36	. . . . . . 7 ((d ∪ (b →1 c))⊥ ∩ c) = ((d⊥ ∩ (b ∩ c)⊥ ) ∩ (b ∩ c))
40	25, 39, 27	le3tr1 140	. . . . . 6 ((d ∪ (b →1 c))⊥ ∩ c) ≤ (d ∪ (b →1 c))
41		lea 160	. . . . . . 7 ((d ∪ (b →1 c)) ∩ c) ≤ (d ∪ (b →1 c))
42	41	lel 151	. . . . . 6 (((d ∪ (b →1 c)) ∩ c) ∩ c) ≤ (d ∪ (b →1 c))
43	40, 42	lel2or 170	. . . . 5 (((d ∪ (b →1 c))⊥ ∩ c) ∪ (((d ∪ (b →1 c)) ∩ c) ∩ c)) ≤ (d ∪ (b →1 c))
44	23, 43	bltr 138	. . . 4 (((d ∪ (b →1 c)) →1 c) ∩ c) ≤ (d ∪ (b →1 c))
45	16, 44	letr 137	. . 3 ((d ∪ (a →1 c)) ∩ c) ≤ (d ∪ (b →1 c))
46	9, 45	lel2or 170	. 2 (((d ∪ (a →1 c)) →1 c)⊥ ∪ ((d ∪ (a →1 c)) ∩ c)) ≤ (d ∪ (b →1 c))
47	2, 46	bltr 138	1 (d ∪ (a →1 c)) ≤ (d ∪ (b →1 c))

Syntax hints:   = wb 1   ≤ 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:  cancel  892