Theorem mlaconj4 826

Description: For 4GO proof of Mladen's conjecture, that it follows from Eq. (3.30) in OA-GO paper.

Hypotheses

Ref	Expression
mlaconj4.1	((d == e) ^ ((e_|_ ^ c_|_) v (d ^ c))) =< (d == c)
mlaconj4.2	d = (a v b)
mlaconj4.3	e = (a ^ b)

Assertion

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

Proof of Theorem mlaconj4

Step	Hyp	Ref	Expression
1		biao 781	. . . . 5 (a == b) = ((a ^ b) == (a v b))
2		bicom 88	. . . . 5 ((a ^ b) == (a v b)) = ((a v b) == (a ^ b))
3	1, 2	ax-r2 35	. . . 4 (a == b) = ((a v b) == (a ^ b))
4	3	bile 134	. . 3 (a == b) =< ((a v b) == (a ^ b))
5		orbile 825	. . . 4 ((a == c) v (b == c)) =< (((a ^ b) ->2 c) ^ (c ->1 (a v b)))
6		imp3 823	. . . 4 (((a ^ b) ->2 c) ^ (c ->1 (a v b))) = (((a ^ b)_|_ ^ c_|_) v (c ^ (a v b)))
7	5, 6	lbtr 131	. . 3 ((a == c) v (b == c)) =< (((a ^ b)_|_ ^ c_|_) v (c ^ (a v b)))
8	4, 7	le2an 161	. 2 ((a == b) ^ ((a == c) v (b == c))) =< (((a v b) == (a ^ b)) ^ (((a ^ b)_|_ ^ c_|_) v (c ^ (a v b))))
9		mlaconj4.2	. . . . . 6 d = (a v b)
10		mlaconj4.3	. . . . . 6 e = (a ^ b)
11	9, 10	2bi 91	. . . . 5 (d == e) = ((a v b) == (a ^ b))
12	10	ax-r4 36	. . . . . . 7 e_|_ = (a ^ b)_|_
13	12	ran 71	. . . . . 6 (e_|_ ^ c_|_) = ((a ^ b)_|_ ^ c_|_)
14		ancom 68	. . . . . . 7 (d ^ c) = (c ^ d)
15	9	lan 70	. . . . . . 7 (c ^ d) = (c ^ (a v b))
16	14, 15	ax-r2 35	. . . . . 6 (d ^ c) = (c ^ (a v b))
17	13, 16	2or 67	. . . . 5 ((e_|_ ^ c_|_) v (d ^ c)) = (((a ^ b)_|_ ^ c_|_) v (c ^ (a v b)))
18	11, 17	2an 72	. . . 4 ((d == e) ^ ((e_|_ ^ c_|_) v (d ^ c))) = (((a v b) == (a ^ b)) ^ (((a ^ b)_|_ ^ c_|_) v (c ^ (a v b))))
19	18	ax-r1 34	. . 3 (((a v b) == (a ^ b)) ^ (((a ^ b)_|_ ^ c_|_) v (c ^ (a v b)))) = ((d == e) ^ ((e_|_ ^ c_|_) v (d ^ c)))
20		lea 152	. . . . . 6 ((d == e) ^ ((e_|_ ^ c_|_) v (d ^ c))) =< (d == e)
21		bicom 88	. . . . . . 7 ((a v b) == (a ^ b)) = ((a ^ b) == (a v b))
22	21, 11, 1	3tr1 60	. . . . . 6 (d == e) = (a == b)
23	20, 22	lbtr 131	. . . . 5 ((d == e) ^ ((e_|_ ^ c_|_) v (d ^ c))) =< (a == b)
24		mlaconj4.1	. . . . . 6 ((d == e) ^ ((e_|_ ^ c_|_) v (d ^ c))) =< (d == c)
25	9	rbi 90	. . . . . 6 (d == c) = ((a v b) == c)
26	24, 25	lbtr 131	. . . . 5 ((d == e) ^ ((e_|_ ^ c_|_) v (d ^ c))) =< ((a v b) == c)
27	23, 26	ler2an 165	. . . 4 ((d == e) ^ ((e_|_ ^ c_|_) v (d ^ c))) =< ((a == b) ^ ((a v b) == c))
28		anass 69	. . . . . . . . . . 11 ((a_|_ ^ b_|_) ^ c_|_) = (a_|_ ^ (b_|_ ^ c_|_))
29		coman1 177	. . . . . . . . . . . 12 (a_|_ ^ (b_|_ ^ c_|_)) C a_|_
30	29	comcom7 442	. . . . . . . . . . 11 (a_|_ ^ (b_|_ ^ c_|_)) C a
31	28, 30	bctr 173	. . . . . . . . . 10 ((a_|_ ^ b_|_) ^ c_|_) C a
32		an32 76	. . . . . . . . . . 11 ((a_|_ ^ b_|_) ^ c_|_) = ((a_|_ ^ c_|_) ^ b_|_)
33		coman2 178	. . . . . . . . . . . 12 ((a_|_ ^ c_|_) ^ b_|_) C b_|_
34	33	comcom7 442	. . . . . . . . . . 11 ((a_|_ ^ c_|_) ^ b_|_) C b
35	32, 34	bctr 173	. . . . . . . . . 10 ((a_|_ ^ b_|_) ^ c_|_) C b
36	31, 35	com2an 466	. . . . . . . . 9 ((a_|_ ^ b_|_) ^ c_|_) C (a ^ b)
37		coman1 177	. . . . . . . . 9 ((a_|_ ^ b_|_) ^ c_|_) C (a_|_ ^ b_|_)
38	36, 37	com2or 465	. . . . . . . 8 ((a_|_ ^ b_|_) ^ c_|_) C ((a ^ b) v (a_|_ ^ b_|_))
39	31, 35	com2or 465	. . . . . . . . 9 ((a_|_ ^ b_|_) ^ c_|_) C (a v b)
40		coman2 178	. . . . . . . . . 10 ((a_|_ ^ b_|_) ^ c_|_) C c_|_
41	40	comcom7 442	. . . . . . . . 9 ((a_|_ ^ b_|_) ^ c_|_) C c
42	39, 41	com2an 466	. . . . . . . 8 ((a_|_ ^ b_|_) ^ c_|_) C ((a v b) ^ c)
43	38, 42	fh2c 459	. . . . . . 7 (((a ^ b) v (a_|_ ^ b_|_)) ^ (((a v b) ^ c) v ((a_|_ ^ b_|_) ^ c_|_))) = ((((a ^ b) v (a_|_ ^ b_|_)) ^ ((a v b) ^ c)) v (((a ^ b) v (a_|_ ^ b_|_)) ^ ((a_|_ ^ b_|_) ^ c_|_)))
44		anor3 82	. . . . . . . . . . 11 (a_|_ ^ b_|_) = (a v b)_|_
45		comanr1 446	. . . . . . . . . . . 12 (a v b) C ((a v b) ^ c)
46	45	comcom3 436	. . . . . . . . . . 11 (a v b)_|_ C ((a v b) ^ c)
47	44, 46	bctr 173	. . . . . . . . . 10 (a_|_ ^ b_|_) C ((a v b) ^ c)
48		coman1 177	. . . . . . . . . . . 12 (a_|_ ^ b_|_) C a_|_
49	48	comcom7 442	. . . . . . . . . . 11 (a_|_ ^ b_|_) C a
50		coman2 178	. . . . . . . . . . . 12 (a_|_ ^ b_|_) C b_|_
51	50	comcom7 442	. . . . . . . . . . 11 (a_|_ ^ b_|_) C b
52	49, 51	com2an 466	. . . . . . . . . 10 (a_|_ ^ b_|_) C (a ^ b)
53	47, 52	fh2rc 462	. . . . . . . . 9 (((a ^ b) v (a_|_ ^ b_|_)) ^ ((a v b) ^ c)) = (((a ^ b) ^ ((a v b) ^ c)) v ((a_|_ ^ b_|_) ^ ((a v b) ^ c)))
54		anass 69	. . . . . . . . . . . 12 (((a ^ b) ^ (a v b)) ^ c) = ((a ^ b) ^ ((a v b) ^ c))
55	54	ax-r1 34	. . . . . . . . . . 11 ((a ^ b) ^ ((a v b) ^ c)) = (((a ^ b) ^ (a v b)) ^ c)
56		leao1 154	. . . . . . . . . . . . 13 (a ^ b) =< (a v b)
57	56	df2le2 128	. . . . . . . . . . . 12 ((a ^ b) ^ (a v b)) = (a ^ b)
58	57	ran 71	. . . . . . . . . . 11 (((a ^ b) ^ (a v b)) ^ c) = ((a ^ b) ^ c)
59	55, 58	ax-r2 35	. . . . . . . . . 10 ((a ^ b) ^ ((a v b) ^ c)) = ((a ^ b) ^ c)
60		dff 93	. . . . . . . . . . . . . 14 0 = ((a_|_ ^ b_|_) ^ (a_|_ ^ b_|_)_|_)
61		oran 79	. . . . . . . . . . . . . . . 16 (a v b) = (a_|_ ^ b_|_)_|_
62	61	lan 70	. . . . . . . . . . . . . . 15 ((a_|_ ^ b_|_) ^ (a v b)) = ((a_|_ ^ b_|_) ^ (a_|_ ^ b_|_)_|_)
63	62	ax-r1 34	. . . . . . . . . . . . . 14 ((a_|_ ^ b_|_) ^ (a_|_ ^ b_|_)_|_) = ((a_|_ ^ b_|_) ^ (a v b))
64	60, 63	ax-r2 35	. . . . . . . . . . . . 13 0 = ((a_|_ ^ b_|_) ^ (a v b))
65	64	ran 71	. . . . . . . . . . . 12 (0 ^ c) = (((a_|_ ^ b_|_) ^ (a v b)) ^ c)
66	65	ax-r1 34	. . . . . . . . . . 11 (((a_|_ ^ b_|_) ^ (a v b)) ^ c) = (0 ^ c)
67		anass 69	. . . . . . . . . . 11 (((a_|_ ^ b_|_) ^ (a v b)) ^ c) = ((a_|_ ^ b_|_) ^ ((a v b) ^ c))
68		an0r 101	. . . . . . . . . . 11 (0 ^ c) = 0
69	66, 67, 68	3tr2 61	. . . . . . . . . 10 ((a_|_ ^ b_|_) ^ ((a v b) ^ c)) = 0
70	59, 69	2or 67	. . . . . . . . 9 (((a ^ b) ^ ((a v b) ^ c)) v ((a_|_ ^ b_|_) ^ ((a v b) ^ c))) = (((a ^ b) ^ c) v 0)
71		or0 94	. . . . . . . . 9 (((a ^ b) ^ c) v 0) = ((a ^ b) ^ c)
72	53, 70, 71	3tr 62	. . . . . . . 8 (((a ^ b) v (a_|_ ^ b_|_)) ^ ((a v b) ^ c)) = ((a ^ b) ^ c)
73		comanr1 446	. . . . . . . . . 10 (a_|_ ^ b_|_) C ((a_|_ ^ b_|_) ^ c_|_)
74	73, 52	fh2rc 462	. . . . . . . . 9 (((a ^ b) v (a_|_ ^ b_|_)) ^ ((a_|_ ^ b_|_) ^ c_|_)) = (((a ^ b) ^ ((a_|_ ^ b_|_) ^ c_|_)) v ((a_|_ ^ b_|_) ^ ((a_|_ ^ b_|_) ^ c_|_)))
75		an4 78	. . . . . . . . . . 11 ((a ^ b) ^ ((a_|_ ^ b_|_) ^ c_|_)) = ((a ^ (a_|_ ^ b_|_)) ^ (b ^ c_|_))
76		dff 93	. . . . . . . . . . . . . . 15 0 = (a ^ a_|_)
77	76	ran 71	. . . . . . . . . . . . . 14 (0 ^ b_|_) = ((a ^ a_|_) ^ b_|_)
78		an0r 101	. . . . . . . . . . . . . 14 (0 ^ b_|_) =