Theorem mlalem 814

Description: Lemma for Mladen's OML.

Assertion

Ref	Expression
mlalem	((a == b) ^ (b ->1 c)) =< (a ->1 c)

Proof of Theorem mlalem

Step	Hyp	Ref	Expression
1		comanr2 447	. . . . . 6 b C (a ^ b)
2	1	comcom3 436	. . . . 5 b_|_ C (a ^ b)
3		comanr1 446	. . . . . 6 b C (b ^ c)
4	3	comcom3 436	. . . . 5 b_|_ C (b ^ c)
5	2, 4	fh2 452	. . . 4 ((a ^ b) ^ (b_|_ v (b ^ c))) = (((a ^ b) ^ b_|_) v ((a ^ b) ^ (b ^ c)))
6		anass 69	. . . . . . 7 ((a ^ b) ^ b_|_) = (a ^ (b ^ b_|_))
7		dff 93	. . . . . . . . 9 0 = (b ^ b_|_)
8	7	ax-r1 34	. . . . . . . 8 (b ^ b_|_) = 0
9	8	lan 70	. . . . . . 7 (a ^ (b ^ b_|_)) = (a ^ 0)
10		an0 100	. . . . . . 7 (a ^ 0) = 0
11	6, 9, 10	3tr 62	. . . . . 6 ((a ^ b) ^ b_|_) = 0
12		le0 139	. . . . . 6 0 =< (a_|_ v (a ^ c))
13	11, 12	bltr 130	. . . . 5 ((a ^ b) ^ b_|_) =< (a_|_ v (a ^ c))
14		anass 69	. . . . . . 7 ((a ^ b) ^ (b ^ c)) = (a ^ (b ^ (b ^ c)))
15		an12 74	. . . . . . 7 (a ^ (b ^ (b ^ c))) = (b ^ (a ^ (b ^ c)))
16		anass 69	. . . . . . . . 9 ((b ^ a) ^ (b ^ c)) = (b ^ (a ^ (b ^ c)))
17	16	ax-r1 34	. . . . . . . 8 (b ^ (a ^ (b ^ c))) = ((b ^ a) ^ (b ^ c))
18		an4 78	. . . . . . . 8 ((b ^ a) ^ (b ^ c)) = ((b ^ b) ^ (a ^ c))
19	17, 18	ax-r2 35	. . . . . . 7 (b ^ (a ^ (b ^ c))) = ((b ^ b) ^ (a ^ c))
20	14, 15, 19	3tr 62	. . . . . 6 ((a ^ b) ^ (b ^ c)) = ((b ^ b) ^ (a ^ c))
21		lear 153	. . . . . . 7 ((b ^ b) ^ (a ^ c)) =< (a ^ c)
22		leor 151	. . . . . . 7 (a ^ c) =< (a_|_ v (a ^ c))
23	21, 22	letr 129	. . . . . 6 ((b ^ b) ^ (a ^ c)) =< (a_|_ v (a ^ c))
24	20, 23	bltr 130	. . . . 5 ((a ^ b) ^ (b ^ c)) =< (a_|_ v (a ^ c))
25	13, 24	lel2or 162	. . . 4 (((a ^ b) ^ b_|_) v ((a ^ b) ^ (b ^ c))) =< (a_|_ v (a ^ c))
26	5, 25	bltr 130	. . 3 ((a ^ b) ^ (b_|_ v (b ^ c))) =< (a_|_ v (a ^ c))
27		anass 69	. . . 4 ((a_|_ ^ b_|_) ^ (b_|_ v (b ^ c))) = (a_|_ ^ (b_|_ ^ (b_|_ v (b ^ c))))
28		lea 152	. . . . 5 (a_|_ ^ (b_|_ ^ (b_|_ v (b ^ c)))) =< a_|_
29		leo 150	. . . . 5 a_|_ =< (a_|_ v (a ^ c))
30	28, 29	letr 129	. . . 4 (a_|_ ^ (b_|_ ^ (b_|_ v (b ^ c)))) =< (a_|_ v (a ^ c))
31	27, 30	bltr 130	. . 3 ((a_|_ ^ b_|_) ^ (b_|_ v (b ^ c))) =< (a_|_ v (a ^ c))
32	26, 31	lel2or 162	. 2 (((a ^ b) ^ (b_|_ v (b ^ c))) v ((a_|_ ^ b_|_) ^ (b_|_ v (b ^ c)))) =< (a_|_ v (a ^ c))
33		dfb 86	. . . 4 (a == b) = ((a ^ b) v (a_|_ ^ b_|_))
34		df-i1 43	. . . 4 (b ->1 c) = (b_|_ v (b ^ c))
35	33, 34	2an 72	. . 3 ((a == b) ^ (b ->1 c)) = (((a ^ b) v (a_|_ ^ b_|_)) ^ (b_|_ v (b ^ c)))
36		lear 153	. . . . . 6 (a_|_ ^ b_|_) =< b_|_
37		leo 150	. . . . . 6 b_|_ =< (b_|_ v (b ^ c))
38	36, 37	letr 129	. . . . 5 (a_|_ ^ b_|_) =< (b_|_ v (b ^ c))
39	38	lecom 172	. . . 4 (a_|_ ^ b_|_) C (b_|_ v (b ^ c))
40		coman1 177	. . . . . . 7 (a_|_ ^ b_|_) C a_|_
41		coman2 178	. . . . . . 7 (a_|_ ^ b_|_) C b_|_
42	40, 41	com2or 465	. . . . . 6 (a_|_ ^ b_|_) C (a_|_ v b_|_)
43		oran3 85	. . . . . 6 (a_|_ v b_|_) = (a ^ b)_|_
44	42, 43	cbtr 174	. . . . 5 (a_|_ ^ b_|_) C (a ^ b)_|_
45	44	comcom7 442	. . . 4 (a_|_ ^ b_|_) C (a ^ b)
46	39, 45	fh2rc 462	. . 3 (((a ^ b) v (a_|_ ^ b_|_)) ^ (b_|_ v (b ^ c))) = (((a ^ b) ^ (b_|_ v (b ^ c))) v ((a_|_ ^ b_|_) ^ (b_|_ v (b ^ c))))
47	35, 46	ax-r2 35	. 2 ((a == b) ^ (b ->1 c)) = (((a ^ b) ^ (b_|_ v (b ^ c))) v ((a_|_ ^ b_|_) ^ (b_|_ v (b ^ c))))
48		df-i1 43	. 2 (a ->1 c) = (a_|_ v (a ^ c))
49	32, 47, 48	le3tr1 132	1 ((a == b) ^ (b ->1 c)) =< (a ->1 c)

Syntax hints:   =< wle 2  _|_wn 4   == tb 5   v wo 6   ^ wa 7  0wf 10   ->1 wi1 13

This theorem is referenced by:  mlaoml 815

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

metamath.org