Theorem negantlem10 861

Description: Lemma for negated antecedent identity. (Contributed by NM, 6-Aug-2001.)

Hypothesis

Ref	Expression
negant.1	(a →1 c) = (b →1 c)

Assertion

Ref	Expression
negantlem10	(a →4 c) ≤ (b →4 c)

Proof of Theorem negantlem10

Step	Hyp	Ref	Expression
1		leao4 165	. . . . 5 (a ∩ c) ≤ (b⊥ ∪ c)
2		leor 159	. . . . . . . 8 (a ∩ c) ≤ (a⊥ ∪ (a ∩ c))
3		df-i1 44	. . . . . . . . 9 (a →1 c) = (a⊥ ∪ (a ∩ c))
4	3	ax-r1 35	. . . . . . . 8 (a⊥ ∪ (a ∩ c)) = (a →1 c)
5	2, 4	lbtr 139	. . . . . . 7 (a ∩ c) ≤ (a →1 c)
6		lear 161	. . . . . . 7 (a ∩ c) ≤ c
7	5, 6	ler2an 173	. . . . . 6 (a ∩ c) ≤ ((a →1 c) ∩ c)
8		negant.1	. . . . . . . 8 (a →1 c) = (b →1 c)
9	8	ran 78	. . . . . . 7 ((a →1 c) ∩ c) = ((b →1 c) ∩ c)
10		u1lemab 610	. . . . . . . 8 ((b →1 c) ∩ c) = ((b ∩ c) ∪ (b⊥ ∩ c))
11		leor 159	. . . . . . . . 9 ((b ∩ c) ∪ (b⊥ ∩ c)) ≤ (c⊥ ∪ ((b ∩ c) ∪ (b⊥ ∩ c)))
12		ancom 74	. . . . . . . . . . . . 13 (b ∩ c) = (c ∩ b)
13		ancom 74	. . . . . . . . . . . . 13 (b⊥ ∩ c) = (c ∩ b⊥ )
14	12, 13	2or 72	. . . . . . . . . . . 12 ((b ∩ c) ∪ (b⊥ ∩ c)) = ((c ∩ b) ∪ (c ∩ b⊥ ))
15		ax-a2 31	. . . . . . . . . . . 12 ((c ∩ b) ∪ (c ∩ b⊥ )) = ((c ∩ b⊥ ) ∪ (c ∩ b))
16	14, 15	ax-r2 36	. . . . . . . . . . 11 ((b ∩ c) ∪ (b⊥ ∩ c)) = ((c ∩ b⊥ ) ∪ (c ∩ b))
17	16	lor 70	. . . . . . . . . 10 (c⊥ ∪ ((b ∩ c) ∪ (b⊥ ∩ c))) = (c⊥ ∪ ((c ∩ b⊥ ) ∪ (c ∩ b)))
18		ax-a3 32	. . . . . . . . . . 11 ((c⊥ ∪ (c ∩ b⊥ )) ∪ (c ∩ b)) = (c⊥ ∪ ((c ∩ b⊥ ) ∪ (c ∩ b)))
19	18	ax-r1 35	. . . . . . . . . 10 (c⊥ ∪ ((c ∩ b⊥ ) ∪ (c ∩ b))) = ((c⊥ ∪ (c ∩ b⊥ )) ∪ (c ∩ b))
20	17, 19	ax-r2 36	. . . . . . . . 9 (c⊥ ∪ ((b ∩ c) ∪ (b⊥ ∩ c))) = ((c⊥ ∪ (c ∩ b⊥ )) ∪ (c ∩ b))
21	11, 20	lbtr 139	. . . . . . . 8 ((b ∩ c) ∪ (b⊥ ∩ c)) ≤ ((c⊥ ∪ (c ∩ b⊥ )) ∪ (c ∩ b))
22	10, 21	bltr 138	. . . . . . 7 ((b →1 c) ∩ c) ≤ ((c⊥ ∪ (c ∩ b⊥ )) ∪ (c ∩ b))
23	9, 22	bltr 138	. . . . . 6 ((a →1 c) ∩ c) ≤ ((c⊥ ∪ (c ∩ b⊥ )) ∪ (c ∩ b))
24	7, 23	letr 137	. . . . 5 (a ∩ c) ≤ ((c⊥ ∪ (c ∩ b⊥ )) ∪ (c ∩ b))
25	1, 24	ler2an 173	. . . 4 (a ∩ c) ≤ ((b⊥ ∪ c) ∩ ((c⊥ ∪ (c ∩ b⊥ )) ∪ (c ∩ b)))
26		leao4 165	. . . . 5 (a⊥ ∩ c) ≤ (b⊥ ∪ c)
27		leor 159	. . . . . . . 8 (a⊥ ∩ c) ≤ (a⊥ ⊥ ∪ (a⊥ ∩ c))
28		df-i1 44	. . . . . . . . 9 (a⊥ →1 c) = (a⊥ ⊥ ∪ (a⊥ ∩ c))
29	28	ax-r1 35	. . . . . . . 8 (a⊥ ⊥ ∪ (a⊥ ∩ c)) = (a⊥ →1 c)
30	27, 29	lbtr 139	. . . . . . 7 (a⊥ ∩ c) ≤ (a⊥ →1 c)
31		lear 161	. . . . . . 7 (a⊥ ∩ c) ≤ c
32	30, 31	ler2an 173	. . . . . 6 (a⊥ ∩ c) ≤ ((a⊥ →1 c) ∩ c)
33	8	negant 852	. . . . . . . 8 (a⊥ →1 c) = (b⊥ →1 c)
34	33	ran 78	. . . . . . 7 ((a⊥ →1 c) ∩ c) = ((b⊥ →1 c) ∩ c)
35		u1lemab 610	. . . . . . . 8 ((b⊥ →1 c) ∩ c) = ((b⊥ ∩ c) ∪ (b⊥ ⊥ ∩ c))
36		leor 159	. . . . . . . . 9 ((b⊥ ∩ c) ∪ (b⊥ ⊥ ∩ c)) ≤ (c⊥ ∪ ((b⊥ ∩ c) ∪ (b⊥ ⊥ ∩ c)))
37		ancom 74	. . . . . . . . . . . . 13 (c ∩ b⊥ ) = (b⊥ ∩ c)
38		ancom 74	. . . . . . . . . . . . . 14 (c ∩ b) = (b ∩ c)
39		ax-a1 30	. . . . . . . . . . . . . . 15 b = b⊥ ⊥
40	39	ran 78	. . . . . . . . . . . . . 14 (b ∩ c) = (b⊥ ⊥ ∩ c)
41	38, 40	ax-r2 36	. . . . . . . . . . . . 13 (c ∩ b) = (b⊥ ⊥ ∩ c)
42	37, 41	2or 72	. . . . . . . . . . . 12 ((c ∩ b⊥ ) ∪ (c ∩ b)) = ((b⊥ ∩ c) ∪ (b⊥ ⊥ ∩ c))
43	42	lor 70	. . . . . . . . . . 11 (c⊥ ∪ ((c ∩ b⊥ ) ∪ (c ∩ b))) = (c⊥ ∪ ((b⊥ ∩ c) ∪ (b⊥ ⊥ ∩ c)))
44	43	ax-r1 35	. . . . . . . . . 10 (c⊥ ∪ ((b⊥ ∩ c) ∪ (b⊥ ⊥ ∩ c))) = (c⊥ ∪ ((c ∩ b⊥ ) ∪ (c ∩ b)))
45	44, 19	ax-r2 36	. . . . . . . . 9 (c⊥ ∪ ((b⊥ ∩ c) ∪ (b⊥ ⊥ ∩ c))) = ((c⊥ ∪ (c ∩ b⊥ )) ∪ (c ∩ b))
46	36, 45	lbtr 139	. . . . . . . 8 ((b⊥ ∩ c) ∪ (b⊥ ⊥ ∩ c)) ≤ ((c⊥ ∪ (c ∩ b⊥ )) ∪ (c ∩ b))
47	35, 46	bltr 138	. . . . . . 7 ((b⊥ →1 c) ∩ c) ≤ ((c⊥ ∪ (c ∩ b⊥ )) ∪ (c ∩ b))
48	34, 47	bltr 138	. . . . . 6 ((a⊥ →1 c) ∩ c) ≤ ((c⊥ ∪ (c ∩ b⊥ )) ∪ (c ∩ b))
49	32, 48	letr 137	. . . . 5 (a⊥ ∩ c) ≤ ((c⊥ ∪ (c ∩ b⊥ )) ∪ (c ∩ b))
50	26, 49	ler2an 173	. . . 4 (a⊥ ∩ c) ≤ ((b⊥ ∪ c) ∩ ((c⊥ ∪ (c ∩ b⊥ )) ∪ (c ∩ b)))
51	25, 50	lel2or 170	. . 3 ((a ∩ c) ∪ (a⊥ ∩ c)) ≤ ((b⊥ ∪ c) ∩ ((c⊥ ∪ (c ∩ b⊥ )) ∪ (c ∩ b)))
52		lea 160	. . . . 5 ((a⊥ ∪ c) ∩ c⊥ ) ≤ (a⊥ ∪ c)
53	8	negantlem8 856	. . . . 5 (a⊥ ∪ c) = (b⊥ ∪ c)
54	52, 53	lbtr 139	. . . 4 ((a⊥ ∪ c) ∩ c⊥ ) ≤ (b⊥ ∪ c)
55		leao2 163	. . . . 5 ((a⊥ ∪ c) ∩ c⊥ ) ≤ (c⊥ ∪ (c ∩ b⊥ ))
56	55	ler 149	. . . 4 ((a⊥ ∪ c) ∩ c⊥ ) ≤ ((c⊥ ∪ (c ∩ b⊥ )) ∪ (c ∩ b))
57	54, 56	ler2an 173	. . 3 ((a⊥ ∪ c) ∩ c⊥ ) ≤ ((b⊥ ∪ c) ∩ ((c⊥ ∪ (c ∩ b⊥ )) ∪ (c ∩ b)))
58	51, 57	lel2or 170	. 2 (((a ∩ c) ∪ (a⊥ ∩ c)) ∪ ((a⊥ ∪ c) ∩ c⊥ )) ≤ ((b⊥ ∪ c) ∩ ((c⊥ ∪ (c ∩ b⊥ )) ∪ (c ∩ b)))
59		df-i4 47	. 2 (a →4 c) = (((a ∩ c) ∪ (a⊥ ∩ c)) ∪ ((a⊥ ∪ c) ∩ c⊥ ))
60		dfi4b 500	. 2 (b →4 c) = ((b⊥ ∪ c) ∩ ((c⊥ ∪ (c ∩ b⊥ )) ∪ (c ∩ b)))
61	58, 59, 60	le3tr1 140	1 (a →4 c) ≤ (b →4 c)

Syntax hints:   = wb 1   ≤ wle 2  ^⊥ wn 4   ∪ wo 6   ∩ wa 7   →₁ wi1 12   →₄ wi4 15

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-i3 46  df-i4 47  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is referenced by:  negant4  862