Theorem ud4lem1b 560

Description: Lemma for unified disjunction.

Assertion

Ref	Expression
ud4lem1b	((a ->4 b)_|_ ^ (b ->4 a)) = (a ^ b_|_)

Proof of Theorem ud4lem1b

Step	Hyp	Ref	Expression
1		ud4lem0c 272	. . 3 (a ->4 b)_|_ = (((a_|_ v b_|_) ^ (a v b_|_)) ^ ((a ^ b_|_) v 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_|_ v b_|_) ^ (a v b_|_)) ^ ((a ^ b_|_) v b)) ^ (((b ^ a) v (b_|_ ^ a)) v ((b_|_ v a) ^ a_|_)))
4		coman2 178	. . . . . . . . . . 11 (b ^ a) C a
5	4	comcom2 175	. . . . . . . . . 10 (b ^ a) C a_|_
6		coman1 177	. . . . . . . . . . 11 (b ^ a) C b
7	6	comcom2 175	. . . . . . . . . 10 (b ^ a) C b_|_
8	5, 7	com2or 465	. . . . . . . . 9 (b ^ a) C (a_|_ v b_|_)
9	8	comcom 435	. . . . . . . 8 (a_|_ v b_|_) C (b ^ a)
10		coman2 178	. . . . . . . . . . 11 (b_|_ ^ a) C a
11	10	comcom2 175	. . . . . . . . . 10 (b_|_ ^ a) C a_|_
12		coman1 177	. . . . . . . . . 10 (b_|_ ^ a) C b_|_
13	11, 12	com2or 465	. . . . . . . . 9 (b_|_ ^ a) C (a_|_ v b_|_)
14	13	comcom 435	. . . . . . . 8 (a_|_ v b_|_) C (b_|_ ^ a)
15	9, 14	com2or 465	. . . . . . 7 (a_|_ v b_|_) C ((b ^ a) v (b_|_ ^ a))
16	15	comcom 435	. . . . . 6 ((b ^ a) v (b_|_ ^ a)) C (a_|_ v b_|_)
17	4, 7	com2or 465	. . . . . . . . 9 (b ^ a) C (a v b_|_)
18	17	comcom 435	. . . . . . . 8 (a v b_|_) C (b ^ a)
19		comor2 444	. . . . . . . . 9 (a v b_|_) C b_|_
20		comor1 443	. . . . . . . . 9 (a v b_|_) C a
21	19, 20	com2an 466	. . . . . . . 8 (a v b_|_) C (b_|_ ^ a)
22	18, 21	com2or 465	. . . . . . 7 (a v b_|_) C ((b ^ a) v (b_|_ ^ a))
23	22	comcom 435	. . . . . 6 ((b ^ a) v (b_|_ ^ a)) C (a v b_|_)
24	16, 23	com2an 466	. . . . 5 ((b ^ a) v (b_|_ ^ a)) C ((a_|_ v b_|_) ^ (a v b_|_))
25		coman2 178	. . . . . . . . . . 11 (a ^ b_|_) C b_|_
26	25	comcom3 436	. . . . . . . . . 10 (a ^ b_|_)_|_ C b_|_
27	26	comcom5 440	. . . . . . . . 9 (a ^ b_|_) C b
28		coman1 177	. . . . . . . . 9 (a ^ b_|_) C a
29	27, 28	com2an 466	. . . . . . . 8 (a ^ b_|_) C (b ^ a)
30	25, 28	com2an 466	. . . . . . . 8 (a ^ b_|_) C (b_|_ ^ a)
31	29, 30	com2or 465	. . . . . . 7 (a ^ b_|_) C ((b ^ a) v (b_|_ ^ a))
32	31	comcom 435	. . . . . 6 ((b ^ a) v (b_|_ ^ a)) C (a ^ b_|_)
33	6	comcom 435	. . . . . . . 8 b C (b ^ a)
34	12	comcom 435	. . . . . . . . . 10 b_|_ C (b_|_ ^ a)
35	34	comcom2 175	. . . . . . . . 9 b_|_ C (b_|_ ^ a)_|_
36	35	comcom5 440	. . . . . . . 8 b C (b_|_ ^ a)
37	33, 36	com2or 465	. . . . . . 7 b C ((b ^ a) v (b_|_ ^ a))
38	37	comcom 435	. . . . . 6 ((b ^ a) v (b_|_ ^ a)) C b
39	32, 38	com2or 465	. . . . 5 ((b ^ a) v (b_|_ ^ a)) C ((a ^ b_|_) v b)
40	24, 39	com2an 466	. . . 4 ((b ^ a) v (b_|_ ^ a)) C (((a_|_ v b_|_) ^ (a v b_|_)) ^ ((a ^ b_|_) v b))
41		comor1 443	. . . . . . . . . 10 (b_|_ v a) C b_|_
42	41	comcom3 436	. . . . . . . . 9 (b_|_ v a)_|_ C b_|_
43	42	comcom5 440	. . . . . . . 8 (b_|_ v a) C b
44		comor2 444	. . . . . . . 8 (b_|_ v a) C a
45	43, 44	com2an 466	. . . . . . 7 (b_|_ v a) C (b ^ a)
46	41, 44	com2an 466	. . . . . . 7 (b_|_ v a) C (b_|_ ^ a)
47	45, 46	com2or 465	. . . . . 6 (b_|_ v a) C ((b ^ a) v (b_|_ ^ a))
48	47	comcom 435	. . . . 5 ((b ^ a) v (b_|_ ^ a)) C (b_|_ v a)
49	4	comcom 435	. . . . . . . 8 a C (b ^ a)
50	10	comcom 435	. . . . . . . 8 a C (b_|_ ^ a)
51	49, 50	com2or 465	. . . . . . 7 a C ((b ^ a) v (b_|_ ^ a))
52	51	comcom 435	. . . . . 6 ((b ^ a) v (b_|_ ^ a)) C a
53	52	comcom2 175	. . . . 5 ((b ^ a) v (b_|_ ^ a)) C a_|_
54	48, 53	com2an 466	. . . 4 ((b ^ a) v (b_|_ ^ a)) C ((b_|_ v a) ^ a_|_)
55	40, 54	fh2 452	. . 3 ((((a_|_ v b_|_) ^ (a v b_|_)) ^ ((a ^ b_|_) v b)) ^ (((b ^ a) v (b_|_ ^ a)) v ((b_|_ v a) ^ a_|_))) = (((((a_|_ v b_|_) ^ (a v b_|_)) ^ ((a ^ b_|_) v b)) ^ ((b ^ a) v (b_|_ ^ a))) v ((((a_|_ v b_|_) ^ (a v b_|_)) ^ ((a ^ b_|_) v b)) ^ ((b_|_ v a) ^ a_|_)))
56	8, 17	com2an 466	. . . . . . . 8 (b ^ a) C ((a_|_ v b_|_) ^ (a v b_|_))
57	4, 7	com2an 466	. . . . . . . . 9 (b ^ a) C (a ^ b_|_)
58	57, 6	com2or 465	. . . . . . . 8 (b ^ a) C ((a ^ b_|_) v b)
59	56, 58	com2an 466	. . . . . . 7 (b ^ a) C (((a_|_ v b_|_) ^ (a v b_|_)) ^ ((a ^ b_|_) v b))
60	7, 4	com2an 466	. . . . . . 7 (b ^ a) C (b_|_ ^ a)
61	59, 60	fh2 452	. . . . . 6 ((((a_|_ v b_|_) ^ (a v b_|_)) ^ ((a ^ b_|_) v b)) ^ ((b ^ a) v (b_|_ ^ a))) = (((((a_|_ v b_|_) ^ (a v b_|_)) ^ ((a ^ b_|_) v b)) ^ (b ^ a)) v ((((a_|_ v b_|_) ^ (a v b_|_)) ^ ((a ^ b_|_) v b)) ^ (b_|_ ^ a)))
62		an32 76	. . . . . . . . . 10 ((((a_|_ v b_|_) ^ (a v b_|_)) ^ ((a ^ b_|_) v b)) ^ (b ^ a)) = ((((a_|_ v b_|_) ^ (a v b_|_)) ^ (b ^ a)) ^ ((a ^ b_|_) v b))
63		an32 76	. . . . . . . . . . . . 13 (((a_|_ v b_|_) ^ (a v b_|_)) ^ (b ^ a)) = (((a_|_ v b_|_) ^ (b ^ a)) ^ (a v b_|_))
64		ax-a2 30	. . . . . . . . . . . . . . . . 17 (a_|_ v b_|_) = (b_|_ v a_|_)
65		df-a 39	. . . . . . . . . . . . . . . . 17 (b ^ a) = (b_|_ v a_|_)_|_
66	64, 65	2an 72	. . . . . . . . . . . . . . . 16 ((a_|_ v b_|_) ^ (b ^ a)) = ((b_|_ v a_|_) ^ (b_|_ v a_|_)_|_)
67		dff 93	. . . . . . . . . . . . . . . . 17 0 = ((b_|_ v a_|_) ^ (b_|_ v a_|_)_|_)
68	67	ax-r1 34	. . . . . . . . . . . . . . . 16 ((b_|_ v a_|_) ^ (b_|_ v a_|_)_|_) = 0
69	66, 68	ax-r2 35	. . . . . . . . . . . . . . 15 ((a_|_ v b_|_) ^ (b ^ a)) = 0
70	69	ran 71	. . . . . . . . . . . . . 14 (((a_|_ v b_|_) ^ (b ^ a)) ^ (a v b_|_)) = (0 ^ (a v b_|_))
71		ancom 68	. . . . . . . . . . . . . . 15 (0 ^ (a v b_|_)) = ((a v b_|_) ^ 0)
72		an0 100	. . . . . . . . . . . . . . 15 ((a v b_|_) ^ 0) = 0
73	71, 72	ax-r2 35	. . . . . . . . . . . . . 14 (0 ^ (a v b_|_)) = 0
74	70, 73	ax-r2 35	. . . . . . . . . . . . 13 (((a_|_ v b_|_) ^ (b ^ a)) ^ (a v b_|_)) = 0
75	63, 74	ax-r2 35	. . . . . . . . . . . 12 (((a_|_ v b_|_) ^ (a v b_|_)) ^ (b ^ a)) = 0
76	75	ran 71	. . . . . . . . . . 11 ((((a_|_ v b_|_) ^ (a v b_|_)) ^ (b ^ a)) ^ ((a ^ b_|_) v b)) = (0 ^ ((a ^ b_|_) v b))
77		ancom 68	. . . . . . . . . . . 12 (0 ^ ((a ^ b_|_) v b)) = (((a ^ b_|_) v b) ^ 0)
78		an0 100	. . . . . . . . . . . 12 (((a ^ b_|_) v b) ^ 0) = 0
79	77, 78	ax-r2 35	. . . . . . . . . . 11 (0 ^ ((a ^ b_|_) v b)) = 0
80	76, 79	ax-r2 35	. . . . . . . . . 10 ((((a_|_ v b_|_) ^ (a v b_|_)) ^ (b ^ a)) ^ ((a ^ b_|_) v b)) = 0
81	62, 80	ax-r2 35	. . . . . . . . 9 ((((a_|_ v b_|_) ^ (a v b_|_)) ^ ((a ^ b_|_) v b)) ^ (b ^ a)) = 0
82		lea 152	. . . . . . . . . . . . . 14 (b_|_ ^ a) =< b_|_
83		leor 151	. . . . . . . . . . . . . 14 b_|_ =< (a_|_ v b_|_)
84	82, 83	letr 129	. . . . . . . . . . . . 13 (b_|_ ^ a) =< (a_|_ v b_|_)
85		lear 153	. . . . . . . . . . . . . 14 (b_|_ ^ a) =< a
86		leo 150	. . . . . . . . . . . . . 14 a =< (a v b_|_)
87	85, 86	letr 129	. . . . . . . . . . . . 13 (b_|_ ^ a) =< (a v b_|_)
88	84, 87	ler2an 165	. . . . . . . . . . . 12 (b_|_ ^ a) =< ((a_|_ v b_|_) ^ (a v b_|_))
89		ancom 68	. . . . . . . . . . . . 13 (b_|_ ^ a) = (a ^ b_|_)
90		leo 150	. . . . . . . . . . . . 13 (a ^ b_|_) =< ((a ^ b_|_) v b)
91	89, 90	bltr 130	. . . . . . . . . . . 12 (b_|_ ^ a) =< ((a ^ b_|_) v b)
92	88, 91	ler2an 165	. . . . . . . . . . 11 (b_|_ ^ a) =< (((a_|_ v b_|_) ^ (a v b_|_)) ^ ((a ^ b_|_) v b))
93	92	df2le2 128	. . . . . . . . . 10