Theorem oa3-u2lem 966

Description: Lemma for a "universal" 3-OA. Equivalence with substitution into 6-OA dual.

Assertion

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

Proof of Theorem oa3-u2lem

Step	Hyp	Ref	Expression
1		u1lemab 592	. . . . . . 7 ((a_|_ ->1 c) ^ c) = ((a_|_ ^ c) v (a_|__|_ ^ c))
2		an1 98	. . . . . . 7 ((a ->1 c) ^ 1) = (a ->1 c)
3	1, 2	2or 67	. . . . . 6 (((a_|_ ->1 c) ^ c) v ((a ->1 c) ^ 1)) = (((a_|_ ^ c) v (a_|__|_ ^ c)) v (a ->1 c))
4		lea 152	. . . . . . . . 9 (a_|_ ^ c) =< a_|_
5		ax-a1 29	. . . . . . . . . . . 12 a = a_|__|_
6	5	ax-r1 34	. . . . . . . . . . 11 a_|__|_ = a
7		leid 140	. . . . . . . . . . 11 a =< a
8	6, 7	bltr 130	. . . . . . . . . 10 a_|__|_ =< a
9	8	leran 145	. . . . . . . . 9 (a_|__|_ ^ c) =< (a ^ c)
10	4, 9	le2or 160	. . . . . . . 8 ((a_|_ ^ c) v (a_|__|_ ^ c)) =< (a_|_ v (a ^ c))
11		df-i1 43	. . . . . . . . 9 (a ->1 c) = (a_|_ v (a ^ c))
12	11	ax-r1 34	. . . . . . . 8 (a_|_ v (a ^ c)) = (a ->1 c)
13	10, 12	lbtr 131	. . . . . . 7 ((a_|_ ^ c) v (a_|__|_ ^ c)) =< (a ->1 c)
14	13	df-le2 123	. . . . . 6 (((a_|_ ^ c) v (a_|__|_ ^ c)) v (a ->1 c)) = (a ->1 c)
15	3, 14	ax-r2 35	. . . . 5 (((a_|_ ->1 c) ^ c) v ((a ->1 c) ^ 1)) = (a ->1 c)
16		ancom 68	. . . . . 6 ((((a_|_ ->1 c) ^ (b_|_ ->1 c)) v ((a ->1 c) ^ (b ->1 c))) ^ ((c ^ (b_|_ ->1 c)) v (1 ^ (b ->1 c)))) = (((c ^ (b_|_ ->1 c)) v (1 ^ (b ->1 c))) ^ (((a_|_ ->1 c) ^ (b_|_ ->1 c)) v ((a ->1 c) ^ (b ->1 c))))
17		ancom 68	. . . . . . . . . 10 (c ^ (b_|_ ->1 c)) = ((b_|_ ->1 c) ^ c)
18		u1lemab 592	. . . . . . . . . 10 ((b_|_ ->1 c) ^ c) = ((b_|_ ^ c) v (b_|__|_ ^ c))
19	17, 18	ax-r2 35	. . . . . . . . 9 (c ^ (b_|_ ->1 c)) = ((b_|_ ^ c) v (b_|__|_ ^ c))
20		ancom 68	. . . . . . . . . 10 (1 ^ (b ->1 c)) = ((b ->1 c) ^ 1)
21		an1 98	. . . . . . . . . 10 ((b ->1 c) ^ 1) = (b ->1 c)
22	20, 21	ax-r2 35	. . . . . . . . 9 (1 ^ (b ->1 c)) = (b ->1 c)
23	19, 22	2or 67	. . . . . . . 8 ((c ^ (b_|_ ->1 c)) v (1 ^ (b ->1 c))) = (((b_|_ ^ c) v (b_|__|_ ^ c)) v (b ->1 c))
24		lea 152	. . . . . . . . . . 11 (b_|_ ^ c) =< b_|_
25		ax-a1 29	. . . . . . . . . . . . . 14 b = b_|__|_
26	25	ax-r1 34	. . . . . . . . . . . . 13 b_|__|_ = b
27		leid 140	. . . . . . . . . . . . 13 b =< b
28	26, 27	bltr 130	. . . . . . . . . . . 12 b_|__|_ =< b
29	28	leran 145	. . . . . . . . . . 11 (b_|__|_ ^ c) =< (b ^ c)
30	24, 29	le2or 160	. . . . . . . . . 10 ((b_|_ ^ c) v (b_|__|_ ^ c)) =< (b_|_ v (b ^ c))
31		df-i1 43	. . . . . . . . . . 11 (b ->1 c) = (b_|_ v (b ^ c))
32	31	ax-r1 34	. . . . . . . . . 10 (b_|_ v (b ^ c)) = (b ->1 c)
33	30, 32	lbtr 131	. . . . . . . . 9 ((b_|_ ^ c) v (b_|__|_ ^ c)) =< (b ->1 c)
34	33	df-le2 123	. . . . . . . 8 (((b_|_ ^ c) v (b_|__|_ ^ c)) v (b ->1 c)) = (b ->1 c)
35	23, 34	ax-r2 35	. . . . . . 7 ((c ^ (b_|_ ->1 c)) v (1 ^ (b ->1 c))) = (b ->1 c)
36		ax-a2 30	. . . . . . 7 (((a_|_ ->1 c) ^ (b_|_ ->1 c)) v ((a ->1 c) ^ (b ->1 c))) = (((a ->1 c) ^ (b ->1 c)) v ((a_|_ ->1 c) ^ (b_|_ ->1 c)))
37	35, 36	2an 72	. . . . . 6 (((c ^ (b_|_ ->1 c)) v (1 ^ (b ->1 c))) ^ (((a_|_ ->1 c) ^ (b_|_ ->1 c)) v ((a ->1 c) ^ (b ->1 c)))) = ((b ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v ((a_|_ ->1 c) ^ (b_|_ ->1 c))))
38	16, 37	ax-r2 35	. . . . 5 ((((a_|_ ->1 c) ^ (b_|_ ->1 c)) v ((a ->1 c) ^ (b ->1 c))) ^ ((c ^ (b_|_ ->1 c)) v (1 ^ (b ->1 c)))) = ((b ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v ((a_|_ ->1 c) ^ (b_|_ ->1 c))))
39	15, 38	2or 67	. . . 4 ((((a_|_ ->1 c) ^ c) v ((a ->1 c) ^ 1)) v ((((a_|_ ->1 c) ^ (b_|_ ->1 c)) v ((a ->1 c) ^ (b ->1 c))) ^ ((c ^ (b_|_ ->1 c)) v (1 ^ (b ->1 c))))) = ((a ->1 c) v ((b ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v ((a_|_ ->1 c) ^ (b_|_ ->1 c)))))
40	39	lan 70	. . 3 (c ^ ((((a_|_ ->1 c) ^ c) v ((a ->1 c) ^ 1)) v ((((a_|_ ->1 c) ^ (b_|_ ->1 c)) v ((a ->1 c) ^ (b ->1 c))) ^ ((c ^ (b_|_ ->1 c)) v (1 ^ (b ->1 c)))))) = (c ^ ((a ->1 c) v ((b ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v ((a_|_ ->1 c) ^ (b_|_ ->1 c))))))
41	40	lor 66	. 2 ((a_|_ ->1 c) v (c ^ ((((a_|_ ->1 c) ^ c) v ((a ->1 c) ^ 1)) v ((((a_|_ ->1 c) ^ (b_|_ ->1 c)) v ((a ->1 c) ^ (b ->1 c))) ^ ((c ^ (b_|_ ->1 c)) v (1 ^ (b ->1 c))))))) = ((a_|_ ->1 c) v (c ^ ((a ->1 c) v ((b ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v ((a_|_ ->1 c) ^ (b_|_ ->1 c)))))))
42	41	lan 70	1 ((a ->1 c) ^ ((a_|_ ->1 c) v (c ^ ((((a_|_ ->1 c) ^ c) v ((a ->1 c) ^ 1)) v ((((a_|_ ->1 c) ^ (b_|_ ->1 c)) v ((a ->1 c) ^ (b ->1 c))) ^ ((c ^ (b_|_ ->1 c)) v (1 ^ (b ->1 c)))))))) = ((a ->1 c) ^ ((a_|_ ->1 c) v (c ^ ((a ->1 c) v ((b ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v ((a_|_ ->1 c) ^ (b_|_ ->1 c))))))))

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

This theorem is referenced by:  oa3-u2 972

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