Theorem oa3-2to2s 970

Description: Derivation of 3-OA variant from weaker version.

Hypotheses

Ref	Expression
oa3-2to2s.1	((a ->1 d) ^ (a v (b ^ ((a ^ b) v ((a ->1 d) ^ (b ->1 d)))))) =< d
oa3-2to2s.2	d = ((a ^ c) v (b ^ c))

Assertion

Ref	Expression
oa3-2to2s	((a ->1 c) ^ (a v (b ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c)))))) =< ((a ^ c) v (b ^ c))

Proof of Theorem oa3-2to2s

Step	Hyp	Ref	Expression
1		id 58	. . 3 (a ->1 c)_|_ = (a ->1 c)_|_
2		id 58	. . 3 (b ->1 c)_|_ = (b ->1 c)_|_
3		id 58	. . 3 (0 ->1 c)_|_ = (0 ->1 c)_|_
4		leo 150	. . . . 5 a_|_ =< (a_|_ v (a ^ c))
5		df-i1 43	. . . . . . 7 (a ->1 c) = (a_|_ v (a ^ c))
6	5	ax-r1 34	. . . . . 6 (a_|_ v (a ^ c)) = (a ->1 c)
7		ax-a1 29	. . . . . 6 (a ->1 c) = (a ->1 c)_|__|_
8	6, 7	ax-r2 35	. . . . 5 (a_|_ v (a ^ c)) = (a ->1 c)_|__|_
9	4, 8	lbtr 131	. . . 4 a_|_ =< (a ->1 c)_|__|_
10		leo 150	. . . . 5 b_|_ =< (b_|_ v (b ^ c))
11		df-i1 43	. . . . . . 7 (b ->1 c) = (b_|_ v (b ^ c))
12	11	ax-r1 34	. . . . . 6 (b_|_ v (b ^ c)) = (b ->1 c)
13		ax-a1 29	. . . . . 6 (b ->1 c) = (b ->1 c)_|__|_
14	12, 13	ax-r2 35	. . . . 5 (b_|_ v (b ^ c)) = (b ->1 c)_|__|_
15	10, 14	lbtr 131	. . . 4 b_|_ =< (b ->1 c)_|__|_
16		leo 150	. . . . 5 0_|_ =< (0_|_ v (0 ^ c))
17		df-i1 43	. . . . . . 7 (0 ->1 c) = (0_|_ v (0 ^ c))
18	17	ax-r1 34	. . . . . 6 (0_|_ v (0 ^ c)) = (0 ->1 c)
19		ax-a1 29	. . . . . 6 (0 ->1 c) = (0 ->1 c)_|__|_
20	18, 19	ax-r2 35	. . . . 5 (0_|_ v (0 ^ c)) = (0 ->1 c)_|__|_
21	16, 20	lbtr 131	. . . 4 0_|_ =< (0 ->1 c)_|__|_
22		or0 94	. . . . . 6 (d v 0) = d
23	22	ax-r1 34	. . . . 5 d = (d v 0)
24		oa3-2to2s.2	. . . . . . 7 d = ((a ^ c) v (b ^ c))
25	5	lan 70	. . . . . . . . . . 11 (a ^ (a ->1 c)) = (a ^ (a_|_ v (a ^ c)))
26		omla 429	. . . . . . . . . . 11 (a ^ (a_|_ v (a ^ c))) = (a ^ c)
27	25, 26	ax-r2 35	. . . . . . . . . 10 (a ^ (a ->1 c)) = (a ^ c)
28	27	ax-r1 34	. . . . . . . . 9 (a ^ c) = (a ^ (a ->1 c))
29		ax-a1 29	. . . . . . . . . 10 a = a_|__|_
30	29, 7	2an 72	. . . . . . . . 9 (a ^ (a ->1 c)) = (a_|__|_ ^ (a ->1 c)_|__|_)
31	28, 30	ax-r2 35	. . . . . . . 8 (a ^ c) = (a_|__|_ ^ (a ->1 c)_|__|_)
32	11	lan 70	. . . . . . . . . . 11 (b ^ (b ->1 c)) = (b ^ (b_|_ v (b ^ c)))
33		omla 429	. . . . . . . . . . 11 (b ^ (b_|_ v (b ^ c))) = (b ^ c)
34	32, 33	ax-r2 35	. . . . . . . . . 10 (b ^ (b ->1 c)) = (b ^ c)
35	34	ax-r1 34	. . . . . . . . 9 (b ^ c) = (b ^ (b ->1 c))
36		ax-a1 29	. . . . . . . . . 10 b = b_|__|_
37	36, 13	2an 72	. . . . . . . . 9 (b ^ (b ->1 c)) = (b_|__|_ ^ (b ->1 c)_|__|_)
38	35, 37	ax-r2 35	. . . . . . . 8 (b ^ c) = (b_|__|_ ^ (b ->1 c)_|__|_)
39	31, 38	2or 67	. . . . . . 7 ((a ^ c) v (b ^ c)) = ((a_|__|_ ^ (a ->1 c)_|__|_) v (b_|__|_ ^ (b ->1 c)_|__|_))
40	24, 39	ax-r2 35	. . . . . 6 d = ((a_|__|_ ^ (a ->1 c)_|__|_) v (b_|__|_ ^ (b ->1 c)_|__|_))
41		an1 98	. . . . . . . 8 (0 ^ 1) = 0
42	41	ax-r1 34	. . . . . . 7 0 = (0 ^ 1)
43		ax-a1 29	. . . . . . . 8 0 = 0_|__|_
44		0i1 265	. . . . . . . . . 10 (0 ->1 c) = 1
45	44	ax-r1 34	. . . . . . . . 9 1 = (0 ->1 c)
46	45, 19	ax-r2 35	. . . . . . . 8 1 = (0 ->1 c)_|__|_
47	43, 46	2an 72	. . . . . . 7 (0 ^ 1) = (0_|__|_ ^ (0 ->1 c)_|__|_)
48	42, 47	ax-r2 35	. . . . . 6 0 = (0_|__|_ ^ (0 ->1 c)_|__|_)
49	40, 48	2or 67	. . . . 5 (d v 0) = (((a_|__|_ ^ (a ->1 c)_|__|_) v (b_|__|_ ^ (b ->1 c)_|__|_)) v (0_|__|_ ^ (0 ->1 c)_|__|_))
50	23, 49	ax-r2 35	. . . 4 d = (((a_|__|_ ^ (a ->1 c)_|__|_) v (b_|__|_ ^ (b ->1 c)_|__|_)) v (0_|__|_ ^ (0 ->1 c)_|__|_))
51		oa3-2lema 958	. . . . 5 ((a ->1 d) ^ (a v (b ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v (((a ^ 0) v ((a ->1 d) ^ (0 ->1 d))) ^ ((b ^ 0) v ((b ->1 d) ^ (0 ->1 d)))))))) = ((a ->1 d) ^ (a v (b ^ ((a ^ b) v ((a ->1 d) ^ (b ->1 d))))))
52		oa3-2to2s.1	. . . . 5 ((a ->1 d) ^ (a v (b ^ ((a ^ b) v ((a ->1 d) ^ (b ->1 d)))))) =< d
53	51, 52	bltr 130	. . . 4 ((a ->1 d) ^ (a v (b ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v (((a ^ 0) v ((a ->1 d) ^ (0 ->1 d))) ^ ((b ^ 0) v ((b ->1 d) ^ (0 ->1 d)))))))) =< d
54	9, 15, 21, 50, 29, 36, 43, 53	oa4to6 945	. . 3 (((a_|_ v (a ->1 c)_|_) ^ (b_|_ v (b ->1 c)_|_)) ^ (0_|_ v (0 ->1 c)_|_)) =< ((a ->1 c)_|_ v (a_|_ ^ (b_|_ v (((a_|_ v b_|_) ^ ((a ->1 c)_|_ v (b ->1 c)_|_)) ^ (((a_|_ v 0_|_) ^ ((a ->1 c)_|_ v (0 ->1 c)_|_)) v ((b_|_ v 0_|_) ^ ((b ->1 c)_|_ v (0 ->1 c)_|_)))))))
55	1, 2, 3, 54	oa6to4 938	. 2 ((a ->1 c) ^ (a v (b ^ (((a ^ b) v ((a ->1 c) ^ (b ->1 c))) v (((a ^ 0) v ((a ->1 c) ^ (0 ->1 c))) ^ ((b ^ 0) v ((b ->1 c) ^ (0 ->1 c)))))))) =< (((a ^ c) v (b ^ c)) v (0 ^ c))
56		oa3-2lema 958	. 2 ((a ->1 c) ^ (a v (b ^ (((a ^ b) v ((a ->1 c) ^ (b ->1 c))) v (((a ^ 0) v ((a ->1 c) ^ (0 ->1 c))) ^ ((b ^ 0) v ((b ->1 c) ^ (0 ->1 c)))))))) = ((a ->1 c) ^ (a v (b ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c))))))
57		ancom 68	. . . . 5 (0 ^ c) = (c ^ 0)
58		an0 100	. . . . 5 (c ^ 0) = 0
59	57, 58	ax-r2 35	. . . 4 (0 ^ c) = 0
60	59	lor 66	. . 3 (((a ^ c) v (b ^ c)) v (0 ^ c)) = (((a ^ c) v (b ^ c)) v 0)
61		or0 94	. . 3 (((a ^ c) v (b ^ c)) v 0) = ((a ^ c) v (b ^ c))
62	60, 61	ax-r2 35	. 2 (((a ^ c) v (b ^ c)) v (0 ^ c)) = ((a ^ c) v (b ^ c))
63	55, 56, 62	le3tr2 133	1 ((a ->1 c) ^ (a v (b ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c)))))) =< ((a ^ c) v (b ^ c))

Syntax hints:   = wb 1   =< wle 2  _|_wn 4   v wo 6   ^ wa 7  1wt 9  0wf 10   ->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