Theorem oaidlem2g 912

Description: Lemma for identity-like OA law (generalized).

Hypothesis

Ref	Expression
oaidlem2g.1	((c v (a ^ b))_|_ v (a ->1 b)) = 1

Assertion

Ref	Expression
oaidlem2g	(a ^ (c v (a ^ b))) =< b

Proof of Theorem oaidlem2g

Step	Hyp	Ref	Expression
1		anidm 103	. . . . . . . . . 10 (a ^ a) = a
2	1	ax-r1 34	. . . . . . . . 9 a = (a ^ a)
3	2	ran 71	. . . . . . . 8 (a ^ b) = ((a ^ a) ^ b)
4		anass 69	. . . . . . . 8 ((a ^ a) ^ b) = (a ^ (a ^ b))
5	3, 4	ax-r2 35	. . . . . . 7 (a ^ b) = (a ^ (a ^ b))
6		leor 151	. . . . . . . 8 (a ^ b) =< (c v (a ^ b))
7	6	lelan 159	. . . . . . 7 (a ^ (a ^ b)) =< (a ^ (c v (a ^ b)))
8	5, 7	bltr 130	. . . . . 6 (a ^ b) =< (a ^ (c v (a ^ b)))
9	8	df-le2 123	. . . . 5 ((a ^ b) v (a ^ (c v (a ^ b)))) = (a ^ (c v (a ^ b)))
10		ax-a3 31	. . . . . 6 (((c v (a ^ b))_|_ v a_|_) v (a ^ b)) = ((c v (a ^ b))_|_ v (a_|_ v (a ^ b)))
11		ax-a2 30	. . . . . . . 8 ((c v (a ^ b))_|_ v a_|_) = (a_|_ v (c v (a ^ b))_|_)
12		oran3 85	. . . . . . . 8 (a_|_ v (c v (a ^ b))_|_) = (a ^ (c v (a ^ b)))_|_
13	11, 12	ax-r2 35	. . . . . . 7 ((c v (a ^ b))_|_ v a_|_) = (a ^ (c v (a ^ b)))_|_
14	13	ax-r5 37	. . . . . 6 (((c v (a ^ b))_|_ v a_|_) v (a ^ b)) = ((a ^ (c v (a ^ b)))_|_ v (a ^ b))
15		df-i1 43	. . . . . . . . 9 (a ->1 b) = (a_|_ v (a ^ b))
16	15	lor 66	. . . . . . . 8 ((c v (a ^ b))_|_ v (a ->1 b)) = ((c v (a ^ b))_|_ v (a_|_ v (a ^ b)))
17	16	ax-r1 34	. . . . . . 7 ((c v (a ^ b))_|_ v (a_|_ v (a ^ b))) = ((c v (a ^ b))_|_ v (a ->1 b))
18		oaidlem2g.1	. . . . . . 7 ((c v (a ^ b))_|_ v (a ->1 b)) = 1
19	17, 18	ax-r2 35	. . . . . 6 ((c v (a ^ b))_|_ v (a_|_ v (a ^ b))) = 1
20	10, 14, 19	3tr2 61	. . . . 5 ((a ^ (c v (a ^ b)))_|_ v (a ^ b)) = 1
21	9, 20	lem3.1 425	. . . 4 (a ^ b) = (a ^ (c v (a ^ b)))
22	21	ax-r1 34	. . 3 (a ^ (c v (a ^ b))) = (a ^ b)
23	22	bile 134	. 2 (a ^ (c v (a ^ b))) =< (a ^ b)
24		lear 153	. 2 (a ^ b) =< b
25	23, 24	letr 129	1 (a ^ (c v (a ^ b))) =< b

Syntax hints:   = wb 1   =< wle 2  _|_wn 4   v wo 6   ^ wa 7  1wt 9   ->1 wi1 13

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a3 31  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

metamath.org