Theorem neg3antlem2 847

Description: Lemma for negated antecedent identity.

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 151	. . . . 5 (a⊥ ∩ c) ≤ ((a ∩ c) ∪ (a⊥ ∩ c))
2		neg3ant.1	. . . . . . 7 (a →3 c) = (b →3 c)
3	2	ran 71	. . . . . 6 ((a →3 c) ∩ c) = ((b →3 c) ∩ c)
4		u3lemab 594	. . . . . 6 ((a →3 c) ∩ c) = ((a ∩ c) ∪ (a⊥ ∩ c))
5		u3lemab 594	. . . . . 6 ((b →3 c) ∩ c) = ((b ∩ c) ∪ (b⊥ ∩ c))
6	3, 4, 5	3tr2 61	. . . . 5 ((a ∩ c) ∪ (a⊥ ∩ c)) = ((b ∩ c) ∪ (b⊥ ∩ c))
7	1, 6	lbtr 131	. . . 4 (a⊥ ∩ c) ≤ ((b ∩ c) ∪ (b⊥ ∩ c))
8		leor 151	. . . . 5 (b ∩ c) ≤ (b⊥ ∪ (b ∩ c))
9		leao1 154	. . . . 5 (b⊥ ∩ c) ≤ (b⊥ ∪ (b ∩ c))
10	8, 9	lel2or 162	. . . 4 ((b ∩ c) ∪ (b⊥ ∩ c)) ≤ (b⊥ ∪ (b ∩ c))
11	7, 10	letr 129	. . 3 (a⊥ ∩ c) ≤ (b⊥ ∪ (b ∩ c))
12		leor 151	. . . . . . . . . . . 12 (b ∩ (b⊥ ∪ c)) ≤ (((b⊥ ∩ c) ∪ (b⊥ ∩ c⊥ )) ∪ (b ∩ (b⊥ ∪ c)))
13		df-i3 45	. . . . . . . . . . . . . 14 (b →3 c) = (((b⊥ ∩ c) ∪ (b⊥ ∩ c⊥ )) ∪ (b ∩ (b⊥ ∪ c)))
14	2, 13	ax-r2 35	. . . . . . . . . . . . 13 (a →3 c) = (((b⊥ ∩ c) ∪ (b⊥ ∩ c⊥ )) ∪ (b ∩ (b⊥ ∪ c)))
15	14	ax-r1 34	. . . . . . . . . . . 12 (((b⊥ ∩ c) ∪ (b⊥ ∩ c⊥ )) ∪ (b ∩ (b⊥ ∪ c))) = (a →3 c)
16	12, 15	lbtr 131	. . . . . . . . . . 11 (b ∩ (b⊥ ∪ c)) ≤ (a →3 c)
17		leao1 154	. . . . . . . . . . . 12 (b ∩ (b⊥ ∪ c)) ≤ (b ∪ c)
18	2	ran 71	. . . . . . . . . . . . . . . 16 ((a →3 c) ∩ c⊥ ) = ((b →3 c) ∩ c⊥ )
19		u3lemanb 599	. . . . . . . . . . . . . . . 16 ((a →3 c) ∩ c⊥ ) = (a⊥ ∩ c⊥ )
20		u3lemanb 599	. . . . . . . . . . . . . . . 16 ((b →3 c) ∩ c⊥ ) = (b⊥ ∩ c⊥ )
21	18, 19, 20	3tr2 61	. . . . . . . . . . . . . . 15 (a⊥ ∩ c⊥ ) = (b⊥ ∩ c⊥ )
22		anor3 82	. . . . . . . . . . . . . . 15 (a⊥ ∩ c⊥ ) = (a ∪ c)⊥
23		anor3 82	. . . . . . . . . . . . . . 15 (b⊥ ∩ c⊥ ) = (b ∪ c)⊥
24	21, 22, 23	3tr2 61	. . . . . . . . . . . . . 14 (a ∪ c)⊥ = (b ∪ c)⊥
25	24	con1 63	. . . . . . . . . . . . 13 (a ∪ c) = (b ∪ c)
26	25	ax-r1 34	. . . . . . . . . . . 12 (b ∪ c) = (a ∪ c)
27	17, 26	lbtr 131	. . . . . . . . . . 11 (b ∩ (b⊥ ∪ c)) ≤ (a ∪ c)
28	16, 27	ler2an 165	. . . . . . . . . 10 (b ∩ (b⊥ ∪ c)) ≤ ((a →3 c) ∩ (a ∪ c))
29		u3lem15 777	. . . . . . . . . 10 ((a →3 c) ∩ (a ∪ c)) = ((a⊥ ∪ c) ∩ (a ∪ (a⊥ ∩ c)))
30	28, 29	lbtr 131	. . . . . . . . 9 (b ∩ (b⊥ ∪ c)) ≤ ((a⊥ ∪ c) ∩ (a ∪ (a⊥ ∩ c)))
31		lear 153	. . . . . . . . 9 ((a⊥ ∪ c) ∩ (a ∪ (a⊥ ∩ c))) ≤ (a ∪ (a⊥ ∩ c))
32	30, 31	letr 129	. . . . . . . 8 (b ∩ (b⊥ ∪ c)) ≤ (a ∪ (a⊥ ∩ c))
33		oran2 84	. . . . . . . . . 10 (b⊥ ∪ c) = (b ∩ c⊥ )⊥
34	33	lan 70	. . . . . . . . 9 (b ∩ (b⊥ ∪ c)) = (b ∩ (b ∩ c⊥ )⊥ )
35		anor1 80	. . . . . . . . 9 (b ∩ (b ∩ c⊥ )⊥ ) = (b⊥ ∪ (b ∩ c⊥ ))⊥
36	34, 35	ax-r2 35	. . . . . . . 8 (b ∩ (b⊥ ∪ c)) = (b⊥ ∪ (b ∩ c⊥ ))⊥
37		anor2 81	. . . . . . . . . 10 (a⊥ ∩ c) = (a ∪ c⊥ )⊥
38	37	lor 66	. . . . . . . . 9 (a ∪ (a⊥ ∩ c)) = (a ∪ (a ∪ c⊥ )⊥ )
39		oran1 83	. . . . . . . . 9 (a ∪ (a ∪ c⊥ )⊥ ) = (a⊥ ∩ (a ∪ c⊥ ))⊥
40	38, 39	ax-r2 35	. . . . . . . 8 (a ∪ (a⊥ ∩ c)) = (a⊥ ∩ (a ∪ c⊥ ))⊥
41	32, 36, 40	le3tr2 133	. . . . . . 7 (b⊥ ∪ (b ∩ c⊥ ))⊥ ≤ (a⊥ ∩ (a ∪ c⊥ ))⊥
42	41	lecon1 147	. . . . . 6 (a⊥ ∩ (a ∪ c⊥ )) ≤ (b⊥ ∪ (b ∩ c⊥ ))
43		leo 150	. . . . . . . 8 a⊥ ≤ (a⊥ ∪ c)
44	2	ax-r5 37	. . . . . . . . 9 ((a →3 c) ∪ c) = ((b →3 c) ∪ c)
45		u3lemob 614	. . . . . . . . 9 ((a →3 c) ∪ c) = (a⊥ ∪ c)
46		u3lemob 614	. . . . . . . . 9 ((b →3 c) ∪ c) = (b⊥ ∪ c)
47	44, 45, 46	3tr2 61	. . . . . . . 8 (a⊥ ∪ c) = (b⊥ ∪ c)
48	43, 47	lbtr 131	. . . . . . 7 a⊥ ≤ (b⊥ ∪ c)
49	48	lel 143	. . . . . 6 (a⊥ ∩ (a ∪ c⊥ )) ≤ (b⊥ ∪ c)
50	42, 49	ler2an 165	. . . . 5 (a⊥ ∩ (a ∪ c⊥ )) ≤ ((b⊥ ∪ (b ∩ c⊥ )) ∩ (b⊥ ∪ c))
51		comor1 443	. . . . . . 7 (b⊥ ∪ c) C b⊥
52	51	comcom7 442	. . . . . . . 8 (b⊥ ∪ c) C b
53		comor2 444	. . . . . . . . 9 (b⊥ ∪ c) C c
54	53	comcom2 175	. . . . . . . 8 (b⊥ ∪ c) C c⊥
55	52, 54	com2an 466	. . . . . . 7 (b⊥ ∪ c) C (b ∩ c⊥ )
56	51, 55	fh1r 455	. . . . . 6 ((b⊥ ∪ (b ∩ c⊥ )) ∩ (b⊥ ∪ c)) = ((b⊥ ∩ (b⊥ ∪ c)) ∪ ((b ∩ c⊥ ) ∩ (b⊥ ∪ c)))
57		a5c 113	. . . . . . 7 (b⊥ ∩ (b⊥ ∪ c)) = b⊥
58	33	lan 70	. . . . . . . 8 ((b ∩ c⊥ ) ∩ (b⊥ ∪ c)) = ((b ∩ c⊥ ) ∩ (b ∩ c⊥ )⊥ )
59		dff 93	. . . . . . . . 9 0 = ((b ∩ c⊥ ) ∩ (b ∩ c⊥ )⊥ )
60	59	ax-r1 34	. . . . . . . 8 ((b ∩ c⊥ ) ∩ (b ∩ c⊥ )⊥ ) = 0
61	58, 60	ax-r2 35	. . . . . . 7 ((b ∩ c⊥ ) ∩ (b⊥ ∪ c)) = 0
62	57, 61	2or 67	. . . . . 6 ((b⊥ ∩ (b⊥ ∪ c)) ∪ ((b ∩ c⊥ ) ∩ (b⊥ ∪ c))) = (b⊥ ∪ 0)
63		or0 94	. . . . . 6 (b⊥ ∪ 0) = b⊥
64	56, 62, 63	3tr 62	. . . . 5 ((b⊥ ∪ (b ∩ c⊥ )) ∩ (b⊥ ∪ c)) = b⊥
65	50, 64	lbtr 131	. . . 4 (a⊥ ∩ (a ∪ c⊥ )) ≤ b⊥
66	65	ler 141	. . 3 (a⊥ ∩ (a ∪ c⊥ )) ≤ (b⊥ ∪ (b ∩ c))
67	11, 66	lel2or 162	. 2 ((a⊥ ∩ c) ∪ (a⊥ ∩ (a ∪ c⊥ ))) ≤ (b⊥ ∪ (b ∩ c))
68		id 58	. . . . 5 a⊥ = a⊥
69		ax-a2 30	. . . . . 6 ((a⊥ ∩ c) ∪ a⊥ ) = (a⊥ ∪ (a⊥ ∩ c))
70		a5b 112	. . . . . 6 (a⊥ ∪ (a⊥ ∩ c)) = a⊥
71	69, 70	ax-r2 35	. . . . 5 ((a⊥ ∩ c) ∪ a⊥ ) = a⊥
72	68, 68, 71	3tr1 60	. . . 4 a⊥ = ((a⊥ ∩ c) ∪ a⊥ )
73		df-t 40	. . . . 5 1 = ((a⊥ ∩ c) ∪ (a⊥ ∩ c)⊥ )
74		oran1 83	. . . . . . 7 (a ∪ c⊥ ) = (a⊥ ∩ c)⊥
75	74	lor 66	. . . . . 6 ((a⊥ ∩ c) ∪ (a ∪ c⊥ )) = ((a⊥ ∩ c) ∪ (a⊥ ∩ c)⊥ )
76	75	ax-r1 34	. . . . 5 ((a⊥ ∩ c) ∪ (a⊥ ∩ c)⊥ ) = ((a⊥ ∩ c) ∪ (a ∪ c⊥ ))
77	73, 76	ax-r2 35	. . . 4 1 = ((a⊥ ∩ c) ∪ (a ∪ c⊥ ))
78	72, 77	2an 72	. . 3 (a⊥ ∩ 1) = (((a⊥ ∩ c) ∪ a⊥ ) ∩ ((a⊥ ∩ c) ∪ (a ∪ c⊥ )))
79		an1 98	. . . 4 (a⊥ ∩ 1) = a⊥
80	79	ax-r1 34	. . 3 a⊥ = (a⊥ ∩ 1)
81		coman1 177	. . . 4 (a⊥ ∩ c) C a⊥
82	81	comcom7 442	. . . . 5 (a⊥ ∩ c) C a
83		coman2 178	. . . . . 6 (a⊥ ∩ c) C c
84	83	comcom2 175	. . . . 5 (a⊥ ∩ c) C c⊥
85	82, 84	com2or 465	. . . 4 (a⊥ ∩ c) C (a ∪ c⊥ )
86	81, 85	fh3 453	. . 3 ((a⊥ ∩ c) ∪ (a⊥ ∩ (a ∪ c⊥ ))) = (((a⊥ ∩ c) ∪ a⊥ ) ∩ ((a⊥ ∩ c) ∪ (a ∪ c⊥ )))
87	78, 80, 86	3tr1 60	. 2 a⊥ = ((a⊥ ∩ c) ∪ (a⊥ ∩ (a ∪ c⊥ )))
88		df-i1 43	. 2 (b →1 c) = (b⊥ ∪ (b ∩ c))
89	67, 87, 88	le3tr1 132	1 a⊥ ≤ (b →1 c)

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

This theorem is referenced by:  neg3ant1 848

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-i3 45  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org