Theorem neg3antlem2 865

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

Hypothesis

Ref	Expression
neg3ant.1	(a →3 c) = (b →3 c)

Assertion

Ref	Expression
neg3antlem2	a⊥ ≤ (b →1 c)

Proof of Theorem neg3antlem2

Step	Hyp	Ref	Expression
1		leor 159	. . . . 5 (a⊥ ∩ c) ≤ ((a ∩ c) ∪ (a⊥ ∩ c))
2		neg3ant.1	. . . . . . 7 (a →3 c) = (b →3 c)
3	2	ran 78	. . . . . 6 ((a →3 c) ∩ c) = ((b →3 c) ∩ c)
4		u3lemab 612	. . . . . 6 ((a →3 c) ∩ c) = ((a ∩ c) ∪ (a⊥ ∩ c))
5		u3lemab 612	. . . . . 6 ((b →3 c) ∩ c) = ((b ∩ c) ∪ (b⊥ ∩ c))
6	3, 4, 5	3tr2 64	. . . . 5 ((a ∩ c) ∪ (a⊥ ∩ c)) = ((b ∩ c) ∪ (b⊥ ∩ c))
7	1, 6	lbtr 139	. . . 4 (a⊥ ∩ c) ≤ ((b ∩ c) ∪ (b⊥ ∩ c))
8		leor 159	. . . . 5 (b ∩ c) ≤ (b⊥ ∪ (b ∩ c))
9		leao1 162	. . . . 5 (b⊥ ∩ c) ≤ (b⊥ ∪ (b ∩ c))
10	8, 9	lel2or 170	. . . 4 ((b ∩ c) ∪ (b⊥ ∩ c)) ≤ (b⊥ ∪ (b ∩ c))
11	7, 10	letr 137	. . 3 (a⊥ ∩ c) ≤ (b⊥ ∪ (b ∩ c))
12		leor 159	. . . . . . . . . . . 12 (b ∩ (b⊥ ∪ c)) ≤ (((b⊥ ∩ c) ∪ (b⊥ ∩ c⊥ )) ∪ (b ∩ (b⊥ ∪ c)))
13		df-i3 46	. . . . . . . . . . . . . 14 (b →3 c) = (((b⊥ ∩ c) ∪ (b⊥ ∩ c⊥ )) ∪ (b ∩ (b⊥ ∪ c)))
14	2, 13	ax-r2 36	. . . . . . . . . . . . 13 (a →3 c) = (((b⊥ ∩ c) ∪ (b⊥ ∩ c⊥ )) ∪ (b ∩ (b⊥ ∪ c)))
15	14	ax-r1 35	. . . . . . . . . . . 12 (((b⊥ ∩ c) ∪ (b⊥ ∩ c⊥ )) ∪ (b ∩ (b⊥ ∪ c))) = (a →3 c)
16	12, 15	lbtr 139	. . . . . . . . . . 11 (b ∩ (b⊥ ∪ c)) ≤ (a →3 c)
17		leao1 162	. . . . . . . . . . . 12 (b ∩ (b⊥ ∪ c)) ≤ (b ∪ c)
18	2	ran 78	. . . . . . . . . . . . . . . 16 ((a →3 c) ∩ c⊥ ) = ((b →3 c) ∩ c⊥ )
19		u3lemanb 617	. . . . . . . . . . . . . . . 16 ((a →3 c) ∩ c⊥ ) = (a⊥ ∩ c⊥ )
20		u3lemanb 617	. . . . . . . . . . . . . . . 16 ((b →3 c) ∩ c⊥ ) = (b⊥ ∩ c⊥ )
21	18, 19, 20	3tr2 64	. . . . . . . . . . . . . . 15 (a⊥ ∩ c⊥ ) = (b⊥ ∩ c⊥ )
22		anor3 90	. . . . . . . . . . . . . . 15 (a⊥ ∩ c⊥ ) = (a ∪ c)⊥
23		anor3 90	. . . . . . . . . . . . . . 15 (b⊥ ∩ c⊥ ) = (b ∪ c)⊥
24	21, 22, 23	3tr2 64	. . . . . . . . . . . . . 14 (a ∪ c)⊥ = (b ∪ c)⊥
25	24	con1 66	. . . . . . . . . . . . 13 (a ∪ c) = (b ∪ c)
26	25	ax-r1 35	. . . . . . . . . . . 12 (b ∪ c) = (a ∪ c)
27	17, 26	lbtr 139	. . . . . . . . . . 11 (b ∩ (b⊥ ∪ c)) ≤ (a ∪ c)
28	16, 27	ler2an 173	. . . . . . . . . 10 (b ∩ (b⊥ ∪ c)) ≤ ((a →3 c) ∩ (a ∪ c))
29		u3lem15 795	. . . . . . . . . 10 ((a →3 c) ∩ (a ∪ c)) = ((a⊥ ∪ c) ∩ (a ∪ (a⊥ ∩ c)))
30	28, 29	lbtr 139	. . . . . . . . 9 (b ∩ (b⊥ ∪ c)) ≤ ((a⊥ ∪ c) ∩ (a ∪ (a⊥ ∩ c)))
31		lear 161	. . . . . . . . 9 ((a⊥ ∪ c) ∩ (a ∪ (a⊥ ∩ c))) ≤ (a ∪ (a⊥ ∩ c))
32	30, 31	letr 137	. . . . . . . 8 (b ∩ (b⊥ ∪ c)) ≤ (a ∪ (a⊥ ∩ c))
33		oran2 92	. . . . . . . . . 10 (b⊥ ∪ c) = (b ∩ c⊥ )⊥
34	33	lan 77	. . . . . . . . 9 (b ∩ (b⊥ ∪ c)) = (b ∩ (b ∩ c⊥ )⊥ )
35		anor1 88	. . . . . . . . 9 (b ∩ (b ∩ c⊥ )⊥ ) = (b⊥ ∪ (b ∩ c⊥ ))⊥
36	34, 35	ax-r2 36	. . . . . . . 8 (b ∩ (b⊥ ∪ c)) = (b⊥ ∪ (b ∩ c⊥ ))⊥
37		anor2 89	. . . . . . . . . 10 (a⊥ ∩ c) = (a ∪ c⊥ )⊥
38	37	lor 70	. . . . . . . . 9 (a ∪ (a⊥ ∩ c)) = (a ∪ (a ∪ c⊥ )⊥ )
39		oran1 91	. . . . . . . . 9 (a ∪ (a ∪ c⊥ )⊥ ) = (a⊥ ∩ (a ∪ c⊥ ))⊥
40	38, 39	ax-r2 36	. . . . . . . 8 (a ∪ (a⊥ ∩ c)) = (a⊥ ∩ (a ∪ c⊥ ))⊥
41	32, 36, 40	le3tr2 141	. . . . . . 7 (b⊥ ∪ (b ∩ c⊥ ))⊥ ≤ (a⊥ ∩ (a ∪ c⊥ ))⊥
42	41	lecon1 155	. . . . . 6 (a⊥ ∩ (a ∪ c⊥ )) ≤ (b⊥ ∪ (b ∩ c⊥ ))
43		leo 158	. . . . . . . 8 a⊥ ≤ (a⊥ ∪ c)
44	2	ax-r5 38	. . . . . . . . 9 ((a →3 c) ∪ c) = ((b →3 c) ∪ c)
45		u3lemob 632	. . . . . . . . 9 ((a →3 c) ∪ c) = (a⊥ ∪ c)
46		u3lemob 632	. . . . . . . . 9 ((b →3 c) ∪ c) = (b⊥ ∪ c)
47	44, 45, 46	3tr2 64	. . . . . . . 8 (a⊥ ∪ c) = (b⊥ ∪ c)
48	43, 47	lbtr 139	. . . . . . 7 a⊥ ≤ (b⊥ ∪ c)
49	48	lel 151	. . . . . 6 (a⊥ ∩ (a ∪ c⊥ )) ≤ (b⊥ ∪ c)
50	42, 49	ler2an 173	. . . . 5 (a⊥ ∩ (a ∪ c⊥ )) ≤ ((b⊥ ∪ (b ∩ c⊥ )) ∩ (b⊥ ∪ c))
51		comor1 461	. . . . . . 7 (b⊥ ∪ c) C b⊥
52	51	comcom7 460	. . . . . . . 8 (b⊥ ∪ c) C b
53		comor2 462	. . . . . . . . 9 (b⊥ ∪ c) C c
54	53	comcom2 183	. . . . . . . 8 (b⊥ ∪ c) C c⊥
55	52, 54	com2an 484	. . . . . . 7 (b⊥ ∪ c) C (b ∩ c⊥ )
56	51, 55	fh1r 473	. . . . . 6 ((b⊥ ∪ (b ∩ c⊥ )) ∩ (b⊥ ∪ c)) = ((b⊥ ∩ (b⊥ ∪ c)) ∪ ((b ∩ c⊥ ) ∩ (b⊥ ∪ c)))
57		anabs 121	. . . . . . 7 (b⊥ ∩ (b⊥ ∪ c)) = b⊥
58	33	lan 77	. . . . . . . 8 ((b ∩ c⊥ ) ∩ (b⊥ ∪ c)) = ((b ∩ c⊥ ) ∩ (b ∩ c⊥ )⊥ )
59		dff 101	. . . . . . . . 9 0 = ((b ∩ c⊥ ) ∩ (b ∩ c⊥ )⊥ )
60	59	ax-r1 35	. . . . . . . 8 ((b ∩ c⊥ ) ∩ (b ∩ c⊥ )⊥ ) = 0
61	58, 60	ax-r2 36	. . . . . . 7 ((b ∩ c⊥ ) ∩ (b⊥ ∪ c)) = 0
62	57, 61	2or 72	. . . . . 6 ((b⊥ ∩ (b⊥ ∪ c)) ∪ ((b ∩ c⊥ ) ∩ (b⊥ ∪ c))) = (b⊥ ∪ 0)
63		or0 102	. . . . . 6 (b⊥ ∪ 0) = b⊥
64	56, 62, 63	3tr 65	. . . . 5 ((b⊥ ∪ (b ∩ c⊥ )) ∩ (b⊥ ∪ c)) = b⊥
65	50, 64	lbtr 139	. . . 4 (a⊥ ∩ (a ∪ c⊥ )) ≤ b⊥
66	65	ler 149	. . 3 (a⊥ ∩ (a ∪ c⊥ )) ≤ (b⊥ ∪ (b ∩ c))
67	11, 66	lel2or 170	. 2 ((a⊥ ∩ c) ∪ (a⊥ ∩ (a ∪ c⊥ ))) ≤ (b⊥ ∪ (b ∩ c))
68		id 59	. . . . 5 a⊥ = a⊥
69		ax-a2 31	. . . . . 6 ((a⊥ ∩ c) ∪ a⊥ ) = (a⊥ ∪ (a⊥ ∩ c))
70		orabs 120	. . . . . 6 (a⊥ ∪ (a⊥ ∩ c)) = a⊥
71	69, 70	ax-r2 36	. . . . 5 ((a⊥ ∩ c) ∪ a⊥ ) = a⊥
72	68, 68, 71	3tr1 63	. . . 4 a⊥ = ((a⊥ ∩ c) ∪ a⊥ )
73		df-t 41	. . . . 5 1 = ((a⊥ ∩ c) ∪ (a⊥ ∩ c)⊥ )
74		oran1 91	. . . . . . 7 (a ∪ c⊥ ) = (a⊥ ∩ c)⊥
75	74	lor 70	. . . . . 6 ((a⊥ ∩ c) ∪ (a ∪ c⊥ )) = ((a⊥ ∩ c) ∪ (a⊥ ∩ c)⊥ )
76	75	ax-r1 35	. . . . 5 ((a⊥ ∩ c) ∪ (a⊥ ∩ c)⊥ ) = ((a⊥ ∩ c) ∪ (a ∪ c⊥ ))
77	73, 76	ax-r2 36	. . . 4 1 = ((a⊥ ∩ c) ∪ (a ∪ c⊥ ))
78	72, 77	2an 79	. . 3 (a⊥ ∩ 1) = (((a⊥ ∩ c) ∪ a⊥ ) ∩ ((a⊥ ∩ c) ∪ (a ∪ c⊥ )))
79		an1 106	. . . 4 (a⊥ ∩ 1) = a⊥
80	79	ax-r1 35	. . 3 a⊥ = (a⊥ ∩ 1)
81		coman1 185	. . . 4 (a⊥ ∩ c) C a⊥
82	81	comcom7 460	. . . . 5 (a⊥ ∩ c) C a
83		coman2 186	. . . . . 6 (a⊥ ∩ c) C c
84	83	comcom2 183	. . . . 5 (a⊥ ∩ c) C c⊥
85	82, 84	com2or 483	. . . 4 (a⊥ ∩ c) C (a ∪ c⊥ )
86	81, 85	fh3 471	. . 3 ((a⊥ ∩ c) ∪ (a⊥ ∩ (a ∪ c⊥ ))) = (((a⊥ ∩ c) ∪ a⊥ ) ∩ ((a⊥ ∩ c) ∪ (a ∪ c⊥ )))
87	78, 80, 86	3tr1 63	. 2 a⊥ = ((a⊥ ∩ c) ∪ (a⊥ ∩ (a ∪ c⊥ )))
88		df-i1 44	. 2 (b →1 c) = (b⊥ ∪ (b ∩ c))
89	67, 87, 88	le3tr1 140	1 a⊥ ≤ (b →1 c)

This proof depends on syntax axioms:   = wb 1   ≤ wle 2  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8  0wf 9   →₁ wi1 12   →₃ wi3 14

This proof depends on 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 proof depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-i3 46  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is used by:  neg3ant1  866