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

Syntax hints:   = wb 1   =< wle 2  _|_wn 4   v wo 6   ^ wa 7  1wt 9  0wf 10   ->1 wi1 13   ->3 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