Theorem ud4lem1a 559

Description: Lemma for unified disjunction.

Assertion

Ref	Expression
ud4lem1a	((a ->4 b) ^ (b ->4 a)) = ((a ^ b) v (a_|_ ^ b_|_))

Proof of Theorem ud4lem1a

Step	Hyp	Ref	Expression
1		df-i4 46	. . 3 (a ->4 b) = (((a ^ b) v (a_|_ ^ b)) v ((a_|_ v b) ^ b_|_))
2		df-i4 46	. . 3 (b ->4 a) = (((b ^ a) v (b_|_ ^ a)) v ((b_|_ v a) ^ a_|_))
3	1, 2	2an 72	. 2 ((a ->4 b) ^ (b ->4 a)) = ((((a ^ b) v (a_|_ ^ b)) v ((a_|_ v b) ^ b_|_)) ^ (((b ^ a) v (b_|_ ^ a)) v ((b_|_ v a) ^ a_|_)))
4		coman2 178	. . . . . . . . . 10 (a ^ b) C b
5	4	comcom 435	. . . . . . . . 9 b C (a ^ b)
6		coman2 178	. . . . . . . . . 10 (a_|_ ^ b) C b
7	6	comcom 435	. . . . . . . . 9 b C (a_|_ ^ b)
8	5, 7	com2or 465	. . . . . . . 8 b C ((a ^ b) v (a_|_ ^ b))
9	8	comcom 435	. . . . . . 7 ((a ^ b) v (a_|_ ^ b)) C b
10		coman1 177	. . . . . . . . . 10 (a ^ b) C a
11	10	comcom 435	. . . . . . . . 9 a C (a ^ b)
12		coman1 177	. . . . . . . . . . . 12 (a_|_ ^ b) C a_|_
13	12	comcom 435	. . . . . . . . . . 11 a_|_ C (a_|_ ^ b)
14	13	comcom2 175	. . . . . . . . . 10 a_|_ C (a_|_ ^ b)_|_
15	14	comcom5 440	. . . . . . . . 9 a C (a_|_ ^ b)
16	11, 15	com2or 465	. . . . . . . 8 a C ((a ^ b) v (a_|_ ^ b))
17	16	comcom 435	. . . . . . 7 ((a ^ b) v (a_|_ ^ b)) C a
18	9, 17	com2an 466	. . . . . 6 ((a ^ b) v (a_|_ ^ b)) C (b ^ a)
19	5	comcom3 436	. . . . . . . . 9 b_|_ C (a ^ b)
20	7	comcom3 436	. . . . . . . . 9 b_|_ C (a_|_ ^ b)
21	19, 20	com2or 465	. . . . . . . 8 b_|_ C ((a ^ b) v (a_|_ ^ b))
22	21	comcom 435	. . . . . . 7 ((a ^ b) v (a_|_ ^ b)) C b_|_
23	22, 17	com2an 466	. . . . . 6 ((a ^ b) v (a_|_ ^ b)) C (b_|_ ^ a)
24	18, 23	com2or 465	. . . . 5 ((a ^ b) v (a_|_ ^ b)) C ((b ^ a) v (b_|_ ^ a))
25	22, 17	com2or 465	. . . . . 6 ((a ^ b) v (a_|_ ^ b)) C (b_|_ v a)
26	11	comcom3 436	. . . . . . . 8 a_|_ C (a ^ b)
27	26, 13	com2or 465	. . . . . . 7 a_|_ C ((a ^ b) v (a_|_ ^ b))
28	27	comcom 435	. . . . . 6 ((a ^ b) v (a_|_ ^ b)) C a_|_
29	25, 28	com2an 466	. . . . 5 ((a ^ b) v (a_|_ ^ b)) C ((b_|_ v a) ^ a_|_)
30	24, 29	com2or 465	. . . 4 ((a ^ b) v (a_|_ ^ b)) C (((b ^ a) v (b_|_ ^ a)) v ((b_|_ v a) ^ a_|_))
31	28, 9	com2or 465	. . . . 5 ((a ^ b) v (a_|_ ^ b)) C (a_|_ v b)
32	9	comcom2 175	. . . . 5 ((a ^ b) v (a_|_ ^ b)) C b_|_
33	31, 32	com2an 466	. . . 4 ((a ^ b) v (a_|_ ^ b)) C ((a_|_ v b) ^ b_|_)
34	30, 33	fh2r 456	. . 3 ((((a ^ b) v (a_|_ ^ b)) v ((a_|_ v b) ^ b_|_)) ^ (((b ^ a) v (b_|_ ^ a)) v ((b_|_ v a) ^ a_|_))) = ((((a ^ b) v (a_|_ ^ b)) ^ (((b ^ a) v (b_|_ ^ a)) v ((b_|_ v a) ^ a_|_))) v (((a_|_ v b) ^ b_|_) ^ (((b ^ a) v (b_|_ ^ a)) v ((b_|_ v a) ^ a_|_))))
35		ancom 68	. . . . . . . . 9 (b ^ a) = (a ^ b)
36		ancom 68	. . . . . . . . 9 (b_|_ ^ a) = (a ^ b_|_)
37	35, 36	2or 67	. . . . . . . 8 ((b ^ a) v (b_|_ ^ a)) = ((a ^ b) v (a ^ b_|_))
38		ax-a2 30	. . . . . . . . 9 (b_|_ v a) = (a v b_|_)
39	38	ran 71	. . . . . . . 8 ((b_|_ v a) ^ a_|_) = ((a v b_|_) ^ a_|_)
40	37, 39	2or 67	. . . . . . 7 (((b ^ a) v (b_|_ ^ a)) v ((b_|_ v a) ^ a_|_)) = (((a ^ b) v (a ^ b_|_)) v ((a v b_|_) ^ a_|_))
41	40	lan 70	. . . . . 6 (((a ^ b) v (a_|_ ^ b)) ^ (((b ^ a) v (b_|_ ^ a)) v ((b_|_ v a) ^ a_|_))) = (((a ^ b) v (a_|_ ^ b)) ^ (((a ^ b) v (a ^ b_|_)) v ((a v b_|_) ^ a_|_)))
42	17, 9	com2an 466	. . . . . . . . 9 ((a ^ b) v (a_|_ ^ b)) C (a ^ b)
43	17, 22	com2an 466	. . . . . . . . 9 ((a ^ b) v (a_|_ ^ b)) C (a ^ b_|_)
44	42, 43	com2or 465	. . . . . . . 8 ((a ^ b) v (a_|_ ^ b)) C ((a ^ b) v (a ^ b_|_))
45	17, 32	com2or 465	. . . . . . . . 9 ((a ^ b) v (a_|_ ^ b)) C (a v b_|_)
46	45, 28	com2an 466	. . . . . . . 8 ((a ^ b) v (a_|_ ^ b)) C ((a v b_|_) ^ a_|_)
47	44, 46	fh1 451	. . . . . . 7 (((a ^ b) v (a_|_ ^ b)) ^ (((a ^ b) v (a ^ b_|_)) v ((a v b_|_) ^ a_|_))) = ((((a ^ b) v (a_|_ ^ b)) ^ ((a ^ b) v (a ^ b_|_))) v (((a ^ b) v (a_|_ ^ b)) ^ ((a v b_|_) ^ a_|_)))
48		an4 78	. . . . . . . . . . 11 ((a_|_ ^ b) ^ (a ^ b_|_)) = ((a_|_ ^ a) ^ (b ^ b_|_))
49		dff 93	. . . . . . . . . . . . . 14 0 = (b ^ b_|_)
50	49	ax-r1 34	. . . . . . . . . . . . 13 (b ^ b_|_) = 0
51	50	lan 70	. . . . . . . . . . . 12 ((a_|_ ^ a) ^ (b ^ b_|_)) = ((a_|_ ^ a) ^ 0)
52		an0 100	. . . . . . . . . . . 12 ((a_|_ ^ a) ^ 0) = 0
53	51, 52	ax-r2 35	. . . . . . . . . . 11 ((a_|_ ^ a) ^ (b ^ b_|_)) = 0
54	48, 53	ax-r2 35	. . . . . . . . . 10 ((a_|_ ^ b) ^ (a ^ b_|_)) = 0
55	54	lor 66	. . . . . . . . 9 ((a ^ b) v ((a_|_ ^ b) ^ (a ^ b_|_))) = ((a ^ b) v 0)
56	10	comcom2 175	. . . . . . . . . . 11 (a ^ b) C a_|_
57	56, 4	com2an 466	. . . . . . . . . 10 (a ^ b) C (a_|_ ^ b)
58	4	comcom2 175	. . . . . . . . . . 11 (a ^ b) C b_|_
59	10, 58	com2an 466	. . . . . . . . . 10 (a ^ b) C (a ^ b_|_)
60	57, 59	fh3 453	. . . . . . . . 9 ((a ^ b) v ((a_|_ ^ b) ^ (a ^ b_|_))) = (((a ^ b) v (a_|_ ^ b)) ^ ((a ^ b) v (a ^ b_|_)))
61		or0 94	. . . . . . . . 9 ((a ^ b) v 0) = (a ^ b)
62	55, 60, 61	3tr2 61	. . . . . . . 8 (((a ^ b) v (a_|_ ^ b)) ^ ((a ^ b) v (a ^ b_|_))) = (a ^ b)
63	10, 58	com2or 465	. . . . . . . . . . 11 (a ^ b) C (a v b_|_)
64	63, 56	com2an 466	. . . . . . . . . 10 (a ^ b) C ((a v b_|_) ^ a_|_)
65	64, 57	fh2r 456	. . . . . . . . 9 (((a ^ b) v (a_|_ ^ b)) ^ ((a v b_|_) ^ a_|_)) = (((a ^ b) ^ ((a v b_|_) ^ a_|_)) v ((a_|_ ^ b) ^ ((a v b_|_) ^ a_|_)))
66		an12 74	. . . . . . . . . . . 12 ((a ^ b) ^ ((a v b_|_) ^ a_|_)) = ((a v b_|_) ^ ((a ^ b) ^ a_|_))
67		an32 76	. . . . . . . . . . . . . . 15 ((a ^ b) ^ a_|_) = ((a ^ a_|_) ^ b)
68		ancom 68	. . . . . . . . . . . . . . . 16 ((a ^ a_|_) ^ b) = (b ^ (a ^ a_|_))
69		dff 93	. . . . . . . . . . . . . . . . . . 19 0 = (a ^ a_|_)
70	69	ax-r1 34	. . . . . . . . . . . . . . . . . 18 (a ^ a_|_) = 0
71	70	lan 70	. . . . . . . . . . . . . . . . 17 (b ^ (a ^ a_|_)) = (b ^ 0)
72		an0 100	. . . . . . . . . . . . . . . . 17 (b ^ 0) = 0
73	71, 72	ax-r2 35	. . . . . . . . . . . . . . . 16 (b ^ (a ^ a_|_)) = 0
74	68, 73	ax-r2 35	. . . . . . . . . . . . . . 15 ((a ^ a_|_) ^ b) = 0
75	67, 74	ax-r2 35	. . . . . . . . . . . . . 14 ((a ^ b) ^ a_|_) = 0
76	75	lan 70	. . . . . . . . . . . . 13 ((a v b_|_) ^ ((a ^ b) ^ a_|_)) = ((a v b_|_) ^ 0)
77		an0 100	. . . . . . . . . . . . 13 ((a v b_|_) ^ 0) = 0
78	76, 77	ax-r2 35	. . . . . . . . . . . 12 ((a v b_|_) ^ ((a ^ b) ^ a_|_)) = 0
79	66, 78	ax-r2 35	. . . . . . . . . . 11 ((a ^ b) ^ ((a v b_|_) ^ a_|_)) = 0
80		ancom 68	. . . . . . . . . . . 12 (((a_|_ ^ b) ^ (a v b_|_)) ^ a_|_) = (a_|_ ^ ((a_|_ ^ b) ^ (a v b_|_)))
81		anass 69	. . . . . . . . . . . 12 (((a_|_ ^ b) ^ (a v b_|_)) ^ a_|_) = ((a_|_ ^ b) ^ ((a v b_|_) ^ a_|_))
82		anor2 81	. . . . . . . . . . . . . . . . . 18 (a_|_ ^ b) = (a v b_|_)_|_
83	82	ax-r1 34	. . . . . . . . . . . . . . . . 17 (a v b_|_)_|_ = (a_|_ ^ b)
84	83	con3 65	. . . . . . . . . . . . . . . 16 (a v b_|_) = (a_|_ ^ b)_|_
85	84	lan 70	. . . . . . . . . . . . . . 15 ((a_|_ ^ b) ^ (a v b_|_