Theorem oa4to4u2 954

Description: A weaker-looking "universal" proper 4-OA.

Hypotheses

Ref	Expression
oa4to4u.1	((e ->1 d) ^ (e v (f ^ (((e ^ f) v ((e ->1 d) ^ (f ->1 d))) v (((e ^ g) v ((e ->1 d) ^ (g ->1 d))) ^ ((f ^ g) v ((f ->1 d) ^ (g ->1 d)))))))) =< (((e ^ d) v (f ^ d)) v (g ^ d))
oa4to4u.2	e = (a_|_ ->1 d)
oa4to4u3	f = (b_|_ ->1 d)
oa4to4u.4	g = (c_|_ ->1 d)

Assertion

Ref	Expression
oa4to4u2	((a ->1 d) ^ ((a_|_ ->1 d) v ((b_|_ ->1 d) ^ ((((a ->1 d) ^ (b ->1 d)) v ((a_|_ ->1 d) ^ (b_|_ ->1 d))) v ((((a ->1 d) ^ (c ->1 d)) v ((a_|_ ->1 d) ^ (c_|_ ->1 d))) ^ (((b ->1 d) ^ (c ->1 d)) v ((b_|_ ->1 d) ^ (c_|_ ->1 d)))))))) =< d

Proof of Theorem oa4to4u2

Step	Hyp	Ref	Expression
1		oa4to4u.1	. . 3 ((e ->1 d) ^ (e v (f ^ (((e ^ f) v ((e ->1 d) ^ (f ->1 d))) v (((e ^ g) v ((e ->1 d) ^ (g ->1 d))) ^ ((f ^ g) v ((f ->1 d) ^ (g ->1 d)))))))) =< (((e ^ d) v (f ^ d)) v (g ^ d))
2		oa4to4u.2	. . 3 e = (a_|_ ->1 d)
3		oa4to4u3	. . 3 f = (b_|_ ->1 d)
4		oa4to4u.4	. . 3 g = (c_|_ ->1 d)
5	1, 2, 3, 4	oa4to4u 953	. 2 ((a ->1 d) ^ ((a_|_ ->1 d) v ((b_|_ ->1 d) ^ ((((a ->1 d) ^ (b ->1 d)) v ((a_|_ ->1 d) ^ (b_|_ ->1 d))) v ((((a ->1 d) ^ (c ->1 d)) v ((a_|_ ->1 d) ^ (c_|_ ->1 d))) ^ (((b ->1 d) ^ (c ->1 d)) v ((b_|_ ->1 d) ^ (c_|_ ->1 d)))))))) =< ((((a ->1 d) ^ (a_|_ ->1 d)) v ((b ->1 d) ^ (b_|_ ->1 d))) v ((c ->1 d) ^ (c_|_ ->1 d)))
6		u1lem8 758	. . . . 5 ((a ->1 d) ^ (a_|_ ->1 d)) = ((a ^ d) v (a_|_ ^ d))
7		lear 153	. . . . . 6 (a ^ d) =< d
8		lear 153	. . . . . 6 (a_|_ ^ d) =< d
9	7, 8	lel2or 162	. . . . 5 ((a ^ d) v (a_|_ ^ d)) =< d
10	6, 9	bltr 130	. . . 4 ((a ->1 d) ^ (a_|_ ->1 d)) =< d
11		u1lem8 758	. . . . 5 ((b ->1 d) ^ (b_|_ ->1 d)) = ((b ^ d) v (b_|_ ^ d))
12		lear 153	. . . . . 6 (b ^ d) =< d
13		lear 153	. . . . . 6 (b_|_ ^ d) =< d
14	12, 13	lel2or 162	. . . . 5 ((b ^ d) v (b_|_ ^ d)) =< d
15	11, 14	bltr 130	. . . 4 ((b ->1 d) ^ (b_|_ ->1 d)) =< d
16	10, 15	lel2or 162	. . 3 (((a ->1 d) ^ (a_|_ ->1 d)) v ((b ->1 d) ^ (b_|_ ->1 d))) =< d
17		u1lem8 758	. . . 4 ((c ->1 d) ^ (c_|_ ->1 d)) = ((c ^ d) v (c_|_ ^ d))
18		lear 153	. . . . 5 (c ^ d) =< d
19		lear 153	. . . . 5 (c_|_ ^ d) =< d
20	18, 19	lel2or 162	. . . 4 ((c ^ d) v (c_|_ ^ d)) =< d
21	17, 20	bltr 130	. . 3 ((c ->1 d) ^ (c_|_ ->1 d)) =< d
22	16, 21	lel2or 162	. 2 ((((a ->1 d) ^ (a_|_ ->1 d)) v ((b ->1 d) ^ (b_|_ ->1 d))) v ((c ->1 d) ^ (c_|_ ->1 d))) =< d
23	5, 22	letr 129	1 ((a ->1 d) ^ ((a_|_ ->1 d) v ((b_|_ ->1 d) ^ ((((a ->1 d) ^ (b ->1 d)) v ((a_|_ ->1 d) ^ (b_|_ ->1 d))) v ((((a ->1 d) ^ (c ->1 d)) v ((a_|_ ->1 d) ^ (c_|_ ->1 d))) ^ (((b ->1 d) ^ (c ->1 d)) v ((b_|_ ->1 d) ^ (c_|_ ->1 d)))))))) =< d

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

This theorem is referenced by:  4oa 1018

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