Theorem mhcor1 870

Description: Corollary of Marsden-Herman Lemma.

Assertion

Ref	Expression
mhcor1	((((a ->1 b) ^ (b ->2 c)) ^ (c ->1 d)) ^ (d ->2 a)) = (((a == b) ^ (b == c)) ^ (c == d))

Proof of Theorem mhcor1

Step	Hyp	Ref	Expression
1		anass 69	. . 3 ((((b ->2 c) ^ (c ->1 d)) ^ (a ->1 b)) ^ (d ->2 a)) = (((b ->2 c) ^ (c ->1 d)) ^ ((a ->1 b) ^ (d ->2 a)))
2		imp3 823	. . . 4 ((b ->2 c) ^ (c ->1 d)) = ((b_|_ ^ c_|_) v (c ^ d))
3		ancom 68	. . . . 5 ((a ->1 b) ^ (d ->2 a)) = ((d ->2 a) ^ (a ->1 b))
4		imp3 823	. . . . 5 ((d ->2 a) ^ (a ->1 b)) = ((d_|_ ^ a_|_) v (a ^ b))
5	3, 4	ax-r2 35	. . . 4 ((a ->1 b) ^ (d ->2 a)) = ((d_|_ ^ a_|_) v (a ^ b))
6	2, 5	2an 72	. . 3 (((b ->2 c) ^ (c ->1 d)) ^ ((a ->1 b) ^ (d ->2 a))) = (((b_|_ ^ c_|_) v (c ^ d)) ^ ((d_|_ ^ a_|_) v (a ^ b)))
7		leao3 156	. . . . . . . . 9 (c ^ d) =< (b v c)
8		oran 79	. . . . . . . . 9 (b v c) = (b_|_ ^ c_|_)_|_
9	7, 8	lbtr 131	. . . . . . . 8 (c ^ d) =< (b_|_ ^ c_|_)_|_
10	9	lecom 172	. . . . . . 7 (c ^ d) C (b_|_ ^ c_|_)_|_
11	10	comcom7 442	. . . . . 6 (c ^ d) C (b_|_ ^ c_|_)
12	11	comcom 435	. . . . 5 (b_|_ ^ c_|_) C (c ^ d)
13		leao2 155	. . . . . . . 8 (c ^ d) =< (d v a)
14		oran 79	. . . . . . . 8 (d v a) = (d_|_ ^ a_|_)_|_
15	13, 14	lbtr 131	. . . . . . 7 (c ^ d) =< (d_|_ ^ a_|_)_|_
16	15	lecom 172	. . . . . 6 (c ^ d) C (d_|_ ^ a_|_)_|_
17	16	comcom7 442	. . . . 5 (c ^ d) C (d_|_ ^ a_|_)
18		leao3 156	. . . . . . . . 9 (a ^ b) =< (d v a)
19	18, 14	lbtr 131	. . . . . . . 8 (a ^ b) =< (d_|_ ^ a_|_)_|_
20	19	lecom 172	. . . . . . 7 (a ^ b) C (d_|_ ^ a_|_)_|_
21	20	comcom7 442	. . . . . 6 (a ^ b) C (d_|_ ^ a_|_)
22	21	comcom 435	. . . . 5 (d_|_ ^ a_|_) C (a ^ b)
23		leao2 155	. . . . . . . 8 (a ^ b) =< (b v c)
24	23, 8	lbtr 131	. . . . . . 7 (a ^ b) =< (b_|_ ^ c_|_)_|_
25	24	lecom 172	. . . . . 6 (a ^ b) C (b_|_ ^ c_|_)_|_
26	25	comcom7 442	. . . . 5 (a ^ b) C (b_|_ ^ c_|_)
27	12, 17, 22, 26	mh2 866	. . . 4 (((b_|_ ^ c_|_) v (c ^ d)) ^ ((d_|_ ^ a_|_) v (a ^ b))) = ((((b_|_ ^ c_|_) ^ (d_|_ ^ a_|_)) v ((b_|_ ^ c_|_) ^ (a ^ b))) v (((c ^ d) ^ (d_|_ ^ a_|_)) v ((c ^ d) ^ (a ^ b))))
28		ancom 68	. . . . . . . 8 ((c_|_ ^ d_|_) ^ (a_|_ ^ b_|_)) = ((a_|_ ^ b_|_) ^ (c_|_ ^ d_|_))
29		ancom 68	. . . . . . . . . 10 (b_|_ ^ c_|_) = (c_|_ ^ b_|_)
30	29	ran 71	. . . . . . . . 9 ((b_|_ ^ c_|_) ^ (d_|_ ^ a_|_)) = ((c_|_ ^ b_|_) ^ (d_|_ ^ a_|_))
31		an4 78	. . . . . . . . 9 ((c_|_ ^ b_|_) ^ (d_|_ ^ a_|_)) = ((c_|_ ^ d_|_) ^ (b_|_ ^ a_|_))
32		ancom 68	. . . . . . . . . 10 (b_|_ ^ a_|_) = (a_|_ ^ b_|_)
33	32	lan 70	. . . . . . . . 9 ((c_|_ ^ d_|_) ^ (b_|_ ^ a_|_)) = ((c_|_ ^ d_|_) ^ (a_|_ ^ b_|_))
34	30, 31, 33	3tr 62	. . . . . . . 8 ((b_|_ ^ c_|_) ^ (d_|_ ^ a_|_)) = ((c_|_ ^ d_|_) ^ (a_|_ ^ b_|_))
35		anass 69	. . . . . . . 8 (((a_|_ ^ b_|_) ^ c_|_) ^ d_|_) = ((a_|_ ^ b_|_) ^ (c_|_ ^ d_|_))
36	28, 34, 35	3tr1 60	. . . . . . 7 ((b_|_ ^ c_|_) ^ (d_|_ ^ a_|_)) = (((a_|_ ^ b_|_) ^ c_|_) ^ d_|_)
37		ancom 68	. . . . . . . 8 ((b_|_ ^ c_|_) ^ (a ^ b)) = ((a ^ b) ^ (b_|_ ^ c_|_))
38		anass 69	. . . . . . . 8 ((a ^ b) ^ (b_|_ ^ c_|_)) = (a ^ (b ^ (b_|_ ^ c_|_)))
39		dff 93	. . . . . . . . . . . . 13 0 = (b ^ b_|_)
40	39	ran 71	. . . . . . . . . . . 12 (0 ^ c_|_) = ((b ^ b_|_) ^ c_|_)
41	40	ax-r1 34	. . . . . . . . . . 11 ((b ^ b_|_) ^ c_|_) = (0 ^ c_|_)
42		anass 69	. . . . . . . . . . 11 ((b ^ b_|_) ^ c_|_) = (b ^ (b_|_ ^ c_|_))
43		an0r 101	. . . . . . . . . . 11 (0 ^ c_|_) = 0
44	41, 42, 43	3tr2 61	. . . . . . . . . 10 (b ^ (b_|_ ^ c_|_)) = 0
45	44	lan 70	. . . . . . . . 9 (a ^ (b ^ (b_|_ ^ c_|_))) = (a ^ 0)
46		an0 100	. . . . . . . . 9 (a ^ 0) = 0
47	45, 46	ax-r2 35	. . . . . . . 8 (a ^ (b ^ (b_|_ ^ c_|_))) = 0
48	37, 38, 47	3tr 62	. . . . . . 7 ((b_|_ ^ c_|_) ^ (a ^ b)) = 0
49	36, 48	2or 67	. . . . . 6 (((b_|_ ^ c_|_) ^ (d_|_ ^ a_|_)) v ((b_|_ ^ c_|_) ^ (a ^ b))) = ((((a_|_ ^ b_|_) ^ c_|_) ^ d_|_) v 0)
50		or0 94	. . . . . 6 ((((a_|_ ^ b_|_) ^ c_|_) ^ d_|_) v 0) = (((a_|_ ^ b_|_) ^ c_|_) ^ d_|_)
51	49, 50	ax-r2 35	. . . . 5 (((b_|_ ^ c_|_) ^ (d_|_ ^ a_|_)) v ((b_|_ ^ c_|_) ^ (a ^ b))) = (((a_|_ ^ b_|_) ^ c_|_) ^ d_|_)
52		anass 69	. . . . . . . 8 ((c ^ d) ^ (d_|_ ^ a_|_)) = (c ^ (d ^ (d_|_ ^ a_|_)))
53		anass 69	. . . . . . . . . . 11 ((d ^ d_|_) ^ a_|_) = (d ^ (d_|_ ^ a_|_))
54	53	ax-r1 34	. . . . . . . . . 10 (d ^ (d_|_ ^ a_|_)) = ((d ^ d_|_) ^ a_|_)
55		an0r 101	. . . . . . . . . . . . 13 (0 ^ a_|_) = 0
56	55	ax-r1 34	. . . . . . . . . . . 12 0 = (0 ^ a_|_)
57		dff 93	. . . . . . . . . . . . 13 0 = (d ^ d_|_)
58	57	ran 71	. . . . . . . . . . . 12 (0 ^ a_|_) = ((d ^ d_|_) ^ a_|_)
59	56, 58	ax-r2 35	. . . . . . . . . . 11 0 = ((d ^ d_|_) ^ a_|_)
60	59	ax-r1 34	. . . . . . . . . 10 ((d ^ d_|_) ^ a_|_) = 0
61	54, 60	ax-r2 35	. . . . . . . . 9 (d ^ (d_|_ ^ a_|_)) = 0
62	61	lan 70	. . . . . . . 8 (c ^ (d ^ (d_|_ ^ a_|_))) = (c ^ 0)
63		an0 100	. . . . . . . 8 (c ^ 0) = 0
64	52, 62, 63	3tr 62	. . . . . . 7 ((c ^ d) ^ (d_|_ ^ a_|_)) = 0
65		ancom 68	. . . . . . . 8 ((c ^ d) ^ (a ^ b)) = ((a ^ b) ^ (c ^ d))
66		anass 69	. . . . . . . . 9 (((a ^ b) ^ c) ^ d) = ((a ^ b) ^ (c ^ d))
67	66	ax-r1 34	. . . . . . . 8 ((a ^ b) ^ (c ^ d)) = (((a ^ b) ^ c) ^ d)
68	65, 67	ax-r2 35	. . . . . . 7 ((c ^ d) ^ (a ^ b)) = (((a ^ b) ^ c) ^ d)
69	64, 68	2or 67	. . . . . 6 (((c ^ d) ^ (d_|_ ^ a_|_)) v ((c ^ d) ^ (a ^ b))) = (0 v (((a ^ b) ^ c) ^ d))
70		or0r 95	. . . . . 6 (0 v (((a ^ b) ^ c) ^ d)) = (((a ^ b) ^ c) ^ d)
71	69, 70	ax-r2 35	. . . . 5 (((c ^ d) ^ (d_|_ ^ a_|_)) v ((c ^ d) ^ (a ^ b))) = (((a ^ b) ^ c) ^ d)
72	51, 71	2or 67	. . . 4 ((((b_|_ ^ c_|_) ^ (d_|_ ^ a_|_)) v ((b_|_ ^ c_|_) ^ (a ^ b))) v (((c ^ d) ^ (d_|_ ^ a_|_)) v ((c ^ d) ^ (a ^ b)))) = ((((a_|_ ^ b_|_) ^ c_|_) ^ d_|_) v (((a ^ b) ^ c) ^ d))
73		ax-a2 30	. . . 4 ((((a_|_ ^ b_|_) ^ c_|_) ^ d_|_) v (((a ^ b) ^ c) ^ d)) = ((((a ^ b) ^ c) ^ d) v (((a_|_ ^ b_|_) ^ c_|_) ^ d_|_))
74	27, 72, 73	3tr 62	. . 3 (((b_|_ ^ c_|_) v (c ^ d)) ^ ((d_|_ ^ a_|_) v (a ^ b))) = ((((a ^ b) ^ c) ^ d) v (((a_|_ ^ b_|_) ^ c_|_) ^ d_|_))
75	1, 6, 74	3tr 62	. 2 ((((b ->2 c) ^ (c ->1 d)) ^ (a ->1 b)) ^ (d ->2 a)) = ((((a ^ b) ^ c) ^ d) v (((a_|_ ^ b_|_) ^ c_|_) ^ d_|_))
76		anass 69	. . . 4 (((a ->1 b) ^ (b ->2 c)) ^ (c ->1 d)) = ((a