Theorem oa3-u1 971

Description: Derivation of a "universal" 3-OA. The hypothesis is a substitution instance of the proper 4-OA.

Hypothesis

Ref	Expression
oa3-u1.1	((c ->1 c) ^ (c v ((a_|_ ->1 c) ^ (((c ^ (a_|_ ->1 c)) v ((c ->1 c) ^ ((a_|_ ->1 c) ->1 c))) v (((c ^ (b_|_ ->1 c)) v ((c ->1 c) ^ ((b_|_ ->1 c) ->1 c))) ^ (((a_|_ ->1 c) ^ (b_|_ ->1 c)) v (((a_|_ ->1 c) ->1 c) ^ ((b_|_ ->1 c) ->1 c)))))))) =< c

Assertion

Ref	Expression
oa3-u1	(c v ((a_|_ ->1 c) ^ ((a ->1 c) v ((b ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v ((a_|_ ->1 c) ^ (b_|_ ->1 c))))))) =< c

Proof of Theorem oa3-u1

Step	Hyp	Ref	Expression
1		oa3-u1lem 965	. . 3 (1 ^ (c v ((a_|_ ->1 c) ^ (((c ^ (a_|_ ->1 c)) v (1 ^ (a ->1 c))) v (((c ^ (b_|_ ->1 c)) v (1 ^ (b ->1 c))) ^ (((a_|_ ->1 c) ^ (b_|_ ->1 c)) v ((a ->1 c) ^ (b ->1 c)))))))) = (c v ((a_|_ ->1 c) ^ ((a ->1 c) v ((b ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v ((a_|_ ->1 c) ^ (b_|_ ->1 c)))))))
2	1	ax-r1 34	. 2 (c v ((a_|_ ->1 c) ^ ((a ->1 c) v ((b ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v ((a_|_ ->1 c) ^ (b_|_ ->1 c))))))) = (1 ^ (c v ((a_|_ ->1 c) ^ (((c ^ (a_|_ ->1 c)) v (1 ^ (a ->1 c))) v (((c ^ (b_|_ ->1 c)) v (1 ^ (b ->1 c))) ^ (((a_|_ ->1 c) ^ (b_|_ ->1 c)) v ((a ->1 c) ^ (b ->1 c))))))))
3		le1 138	. . . 4 c_|_ =< 1
4		u1lem9ab 761	. . . 4 (a_|_ ->1 c)_|_ =< (a ->1 c)
5		u1lem9ab 761	. . . 4 (b_|_ ->1 c)_|_ =< (b ->1 c)
6		ax-a2 30	. . . . . . 7 (c v ((b ^ c) v (b_|_ ^ c))) = (((b ^ c) v (b_|_ ^ c)) v c)
7		lear 153	. . . . . . . . 9 (b ^ c) =< c
8		lear 153	. . . . . . . . 9 (b_|_ ^ c) =< c
9	7, 8	lel2or 162	. . . . . . . 8 ((b ^ c) v (b_|_ ^ c)) =< c
10	9	df-le2 123	. . . . . . 7 (((b ^ c) v (b_|_ ^ c)) v c) = c
11	6, 10	ax-r2 35	. . . . . 6 (c v ((b ^ c) v (b_|_ ^ c))) = c
12	11	ax-r1 34	. . . . 5 c = (c v ((b ^ c) v (b_|_ ^ c)))
13		an1 98	. . . . . . . . 9 (c ^ 1) = c
14		ancom 68	. . . . . . . . . 10 ((a_|_ ->1 c) ^ (a ->1 c)) = ((a ->1 c) ^ (a_|_ ->1 c))
15		u1lem8 758	. . . . . . . . . 10 ((a ->1 c) ^ (a_|_ ->1 c)) = ((a ^ c) v (a_|_ ^ c))
16	14, 15	ax-r2 35	. . . . . . . . 9 ((a_|_ ->1 c) ^ (a ->1 c)) = ((a ^ c) v (a_|_ ^ c))
17	13, 16	2or 67	. . . . . . . 8 ((c ^ 1) v ((a_|_ ->1 c) ^ (a ->1 c))) = (c v ((a ^ c) v (a_|_ ^ c)))
18		ax-a2 30	. . . . . . . 8 (c v ((a ^ c) v (a_|_ ^ c))) = (((a ^ c) v (a_|_ ^ c)) v c)
19		lear 153	. . . . . . . . . 10 (a ^ c) =< c
20		lear 153	. . . . . . . . . 10 (a_|_ ^ c) =< c
21	19, 20	lel2or 162	. . . . . . . . 9 ((a ^ c) v (a_|_ ^ c)) =< c
22	21	df-le2 123	. . . . . . . 8 (((a ^ c) v (a_|_ ^ c)) v c) = c
23	17, 18, 22	3tr 62	. . . . . . 7 ((c ^ 1) v ((a_|_ ->1 c) ^ (a ->1 c))) = c
24		ancom 68	. . . . . . . 8 ((b_|_ ->1 c) ^ (b ->1 c)) = ((b ->1 c) ^ (b_|_ ->1 c))
25		u1lem8 758	. . . . . . . 8 ((b ->1 c) ^ (b_|_ ->1 c)) = ((b ^ c) v (b_|_ ^ c))
26	24, 25	ax-r2 35	. . . . . . 7 ((b_|_ ->1 c) ^ (b ->1 c)) = ((b ^ c) v (b_|_ ^ c))
27	23, 26	2or 67	. . . . . 6 (((c ^ 1) v ((a_|_ ->1 c) ^ (a ->1 c))) v ((b_|_ ->1 c) ^ (b ->1 c))) = (c v ((b ^ c) v (b_|_ ^ c)))
28	27	ax-r1 34	. . . . 5 (c v ((b ^ c) v (b_|_ ^ c))) = (((c ^ 1) v ((a_|_ ->1 c) ^ (a ->1 c))) v ((b_|_ ->1 c) ^ (b ->1 c)))
29	12, 28	ax-r2 35	. . . 4 c = (((c ^ 1) v ((a_|_ ->1 c) ^ (a ->1 c))) v ((b_|_ ->1 c) ^ (b ->1 c)))
30		oa3-u1.1	. . . 4 ((c ->1 c) ^ (c v ((a_|_ ->1 c) ^ (((c ^ (a_|_ ->1 c)) v ((c ->1 c) ^ ((a_|_ ->1 c) ->1 c))) v (((c ^ (b_|_ ->1 c)) v ((c ->1 c) ^ ((b_|_ ->1 c) ->1 c))) ^ (((a_|_ ->1 c) ^ (b_|_ ->1 c)) v (((a_|_ ->1 c) ->1 c) ^ ((b_|_ ->1 c) ->1 c)))))))) =< c
31	3, 4, 5, 29, 30	oa4to6dual 944	. . 3 (1 ^ (c v ((a_|_ ->1 c) ^ (((c ^ (a_|_ ->1 c)) v (1 ^ (a ->1 c))) v (((c ^ (b_|_ ->1 c)) v (1 ^ (b ->1 c))) ^ (((a_|_ ->1 c) ^ (b_|_ ->1 c)) v ((a ->1 c) ^ (b ->1 c)))))))) =< c
32		leid 140	. . 3 c =< c
33	31, 32	letr 129	. 2 (1 ^ (c v ((a_|_ ->1 c) ^ (((c ^ (a_|_ ->1 c)) v (1 ^ (a ->1 c))) v (((c ^ (b_|_ ->1 c)) v (1 ^ (b ->1 c))) ^ (((a_|_ ->1 c) ^ (b_|_ ->1 c)) v ((a ->1 c) ^ (b ->1 c)))))))) =< c
34	2, 33	bltr 130	1 (c v ((a_|_ ->1 c) ^ ((a ->1 c) v ((b ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v ((a_|_ ->1 c) ^ (b_|_ ->1 c))))))) =< c

Syntax hints:   =< 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-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