Theorem ud4lem1c 561

Description: Lemma for unified disjunction.

Assertion

Ref	Expression
ud4lem1c	((a ->4 b)_|_ v (b ->4 a)) = (a v b_|_)

Proof of Theorem ud4lem1c

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	2or 67	. 2 ((a ->4 b)_|_ v (b ->4 a)) = ((((a_|_ v b_|_) ^ (a v b_|_)) ^ ((a ^ b_|_) v b)) v (((b ^ a) v (b_|_ ^ a)) v ((b_|_ v a) ^ a_|_)))
4		comor2 444	. . . . . . . . . . . 12 (a_|_ v b_|_) C b_|_
5	4	comcom3 436	. . . . . . . . . . 11 (a_|_ v b_|_)_|_ C b_|_
6	5	comcom5 440	. . . . . . . . . 10 (a_|_ v b_|_) C b
7		comor1 443	. . . . . . . . . . . 12 (a_|_ v b_|_) C a_|_
8	7	comcom3 436	. . . . . . . . . . 11 (a_|_ v b_|_)_|_ C a_|_
9	8	comcom5 440	. . . . . . . . . 10 (a_|_ v b_|_) C a
10	6, 9	com2an 466	. . . . . . . . 9 (a_|_ v b_|_) C (b ^ a)
11	4, 9	com2an 466	. . . . . . . . 9 (a_|_ v b_|_) C (b_|_ ^ a)
12	10, 11	com2or 465	. . . . . . . 8 (a_|_ v b_|_) C ((b ^ a) v (b_|_ ^ a))
13	12	comcom 435	. . . . . . 7 ((b ^ a) v (b_|_ ^ a)) C (a_|_ v b_|_)
14		comor2 444	. . . . . . . . . . . 12 (a v b_|_) C b_|_
15	14	comcom3 436	. . . . . . . . . . 11 (a v b_|_)_|_ C b_|_
16	15	comcom5 440	. . . . . . . . . 10 (a v b_|_) C b
17		comor1 443	. . . . . . . . . 10 (a v b_|_) C a
18	16, 17	com2an 466	. . . . . . . . 9 (a v b_|_) C (b ^ a)
19	14, 17	com2an 466	. . . . . . . . 9 (a v b_|_) C (b_|_ ^ a)
20	18, 19	com2or 465	. . . . . . . 8 (a v b_|_) C ((b ^ a) v (b_|_ ^ a))
21	20	comcom 435	. . . . . . 7 ((b ^ a) v (b_|_ ^ a)) C (a v b_|_)
22	13, 21	com2an 466	. . . . . 6 ((b ^ a) v (b_|_ ^ a)) C ((a_|_ v b_|_) ^ (a v b_|_))
23	22	comcom 435	. . . . 5 ((a_|_ v b_|_) ^ (a v b_|_)) C ((b ^ a) v (b_|_ ^ a))
24		comor2 444	. . . . . . . . . 10 (b_|_ v a) C a
25	24	comcom2 175	. . . . . . . . 9 (b_|_ v a) C a_|_
26		comor1 443	. . . . . . . . 9 (b_|_ v a) C b_|_
27	25, 26	com2or 465	. . . . . . . 8 (b_|_ v a) C (a_|_ v b_|_)
28	25	comcom3 436	. . . . . . . . . 10 (b_|_ v a)_|_ C a_|_
29	28	comcom5 440	. . . . . . . . 9 (b_|_ v a) C a
30	29, 26	com2or 465	. . . . . . . 8 (b_|_ v a) C (a v b_|_)
31	27, 30	com2an 466	. . . . . . 7 (b_|_ v a) C ((a_|_ v b_|_) ^ (a v b_|_))
32	31	comcom 435	. . . . . 6 ((a_|_ v b_|_) ^ (a v b_|_)) C (b_|_ v a)
33		comorr 176	. . . . . . . 8 a_|_ C (a_|_ v b_|_)
34		comorr 176	. . . . . . . . 9 a C (a v b_|_)
35	34	comcom3 436	. . . . . . . 8 a_|_ C (a v b_|_)
36	33, 35	com2an 466	. . . . . . 7 a_|_ C ((a_|_ v b_|_) ^ (a v b_|_))
37	36	comcom 435	. . . . . 6 ((a_|_ v b_|_) ^ (a v b_|_)) C a_|_
38	32, 37	com2an 466	. . . . 5 ((a_|_ v b_|_) ^ (a v b_|_)) C ((b_|_ v a) ^ a_|_)
39	23, 38	com2or 465	. . . 4 ((a_|_ v b_|_) ^ (a v b_|_)) C (((b ^ a) v (b_|_ ^ a)) v ((b_|_ v a) ^ a_|_))
40		coman1 177	. . . . . . . . 9 (a ^ b_|_) C a
41	40	comcom2 175	. . . . . . . 8 (a ^ b_|_) C a_|_
42		coman2 178	. . . . . . . 8 (a ^ b_|_) C b_|_
43	41, 42	com2or 465	. . . . . . 7 (a ^ b_|_) C (a_|_ v b_|_)
44	40, 42	com2or 465	. . . . . . 7 (a ^ b_|_) C (a v b_|_)
45	43, 44	com2an 466	. . . . . 6 (a ^ b_|_) C ((a_|_ v b_|_) ^ (a v b_|_))
46	45	comcom 435	. . . . 5 ((a_|_ v b_|_) ^ (a v b_|_)) C (a ^ b_|_)
47	4	comcom 435	. . . . . . . . 9 b_|_ C (a_|_ v b_|_)
48	14	comcom 435	. . . . . . . . 9 b_|_ C (a v b_|_)
49	47, 48	com2an 466	. . . . . . . 8 b_|_ C ((a_|_ v b_|_) ^ (a v b_|_))
50	49	comcom 435	. . . . . . 7 ((a_|_ v b_|_) ^ (a v b_|_)) C b_|_
51	50	comcom3 436	. . . . . 6 ((a_|_ v b_|_) ^ (a v b_|_))_|_ C b_|_
52	51	comcom5 440	. . . . 5 ((a_|_ v b_|_) ^ (a v b_|_)) C b
53	46, 52	com2or 465	. . . 4 ((a_|_ v b_|_) ^ (a v b_|_)) C ((a ^ b_|_) v b)
54	39, 53	fh4r 458	. . 3 ((((a_|_ v b_|_) ^ (a v b_|_)) ^ ((a ^ b_|_) v b)) v (((b ^ a) v (b_|_ ^ a)) v ((b_|_ v a) ^ a_|_))) = ((((a_|_ v b_|_) ^ (a v b_|_)) v (((b ^ a) v (b_|_ ^ a)) v ((b_|_ v a) ^ a_|_))) ^ (((a ^ b_|_) v b) v (((b ^ a) v (b_|_ ^ a)) v ((b_|_ v a) ^ a_|_))))
55		coman2 178	. . . . . . . . . . . 12 (b ^ a) C a
56	55	comcom2 175	. . . . . . . . . . 11 (b ^ a) C a_|_
57		coman1 177	. . . . . . . . . . . 12 (b ^ a) C b
58	57	comcom2 175	. . . . . . . . . . 11 (b ^ a) C b_|_
59	56, 58	com2or 465	. . . . . . . . . 10 (b ^ a) C (a_|_ v b_|_)
60	59	comcom 435	. . . . . . . . 9 (a_|_ v b_|_) C (b ^ a)
61		coman2 178	. . . . . . . . . . . 12 (b_|_ ^ a) C a
62	61	comcom2 175	. . . . . . . . . . 11 (b_|_ ^ a) C a_|_
63		coman1 177	. . . . . . . . . . 11 (b_|_ ^ a) C b_|_
64	62, 63	com2or 465	. . . . . . . . . 10 (b_|_ ^ a) C (a_|_ v b_|_)
65	64	comcom 435	. . . . . . . . 9 (a_|_ v b_|_) C (b_|_ ^ a)
66	60, 65	com2or 465	. . . . . . . 8 (a_|_ v b_|_) C ((b ^ a) v (b_|_ ^ a))
67	27	comcom 435	. . . . . . . . 9 (a_|_ v b_|_) C (b_|_ v a)
68	67, 7	com2an 466	. . . . . . . 8 (a_|_ v b_|_) C ((b_|_ v a) ^ a_|_)
69	66, 68	com2or 465	. . . . . . 7 (a_|_ v b_|_) C (((b ^ a) v (b_|_ ^ a)) v ((b_|_ v a) ^ a_|_))
70	17	comcom2 175	. . . . . . . . 9 (a v b_|_) C a_|_
71	70, 14	com2or 465	. . . . . . . 8 (a v b_|_) C (a_|_ v b_|_)
72	71	comcom 435	. . . . . . 7 (a_|_ v b_|_) C (a v b_|_)
73	69, 72	fh4r 458	. . . . . 6 (((a_|_ v b_|_) ^ (a v b_|_)) v (((b ^ a) v (b_|_ ^ a)) v ((b_|_ v a) ^ a_|_))) = (((a_|_ v b_|_) v (((b ^ a) v (b_|_ ^ a)) v ((b_|_ v a) ^ a_|_))) ^ ((a v b_|_) v (((b ^ a) v (b_|_ ^ a)) v ((b_|_ v a) ^ a_|_))))
74		ax-a2 30	. . . . . . . . . . 11 (((a_|_ v b_|_) v (b ^ a)) v (b_|_ ^ a)) = ((b_|_ ^ a) v ((a_|_ v b_|_) v (b ^ a)))
75		ax-a3 31	. . . . . . . . . . 11 (((a_|_ v b_|_) v (b ^ a)) v (b_|_ ^ a)) = ((a_|_ v b_|_) v ((b ^ a) v (b_|_ ^ a)))
76		ax-a2 30	. . . . . . . . . . . . . . 15 (a_|_ v b_|_) = (b_|_ v a_|_)
77		df-a 39	. . . . . . . . . . . . . . 15 (b ^ a) = (b_|_ v a_|_)_|_
78	76, 77	2or 67	. . . . . . . . . . . . . 14 ((a_|_ v b_|_) v (b ^ a)) = ((b_|_ v a_|_) v (b_|_ v a_|_)_|_)
79		df-t 40	. . . . . . . . . . . . . . 15 1 = ((b_|_ v a_|_) v (b_|_ v a_|_)_|_)
80	79	ax-r1 34	. . . . . . . . . . . . . 14 ((b_|_ v a_|_) v (b_|_ v a_|_)_|_) = 1
81	78, 80	ax-r2 35	. . . . . . . . . . . . 13 ((a_|_ v b_|_) v (b ^ a)) = 1
82	81	lor 66	. . . . . . . . . . . 12 ((b_|_ ^ a) v ((a_|_ v b_|_) v (b ^ a))) = ((b_|_ ^ a) v 1)
83		or1 96	. . . . . . . . . . . 12 ((b_|_ ^ a) v 1) = 1
84	82, 83	ax-r2 35	. . . . . . . . . . 11 ((b_|_ ^ a) v ((a_|_ v b_|_) v (b ^ a))) = 1
85	74, 75, 84	3tr2 61	. . . . . . . . . 10 ((a_|_ v b_|_) v ((b ^ a) v (b_|_ ^ a))) = 1
86	85	ax-r5 37	. . . . . . . . 9 (((a_|_ v b_|_) v ((b ^ a) v (b_|_ ^ a))) v ((b_|_ v a) ^ a_|_)) = (1 v ((b_|_ v a) ^ a_|_))
87		ax-a3 31	. . . . . . . . 9 (((a_|_ v b_|_) v ((b ^ a) v (b_|_ ^ a))) v ((b_|_ v a) ^ a_|_)) = ((a_|_ v b_|_) v (((b ^ a) v (b_|_ ^ a)) v ((b_|_ v a) ^ a_|_)))
88		ax-a2 30	. . . . . . . . . 10 (1 v ((b_|_ v a) ^ a_|_)) = (((b_|_ v a) ^ a_|_) v 1)
89		or1 96	. . . . . . . . . 10 (((b_|_ v a) ^ a_|_) v 1) = 1
90	88, 89	ax-r2 35	. . . . . . . . 9 (1 v ((b_|_ v a) ^ a_|_)) = 1
91	86, 87, 90	3tr2 61	. . . . . . . 8 ((a_|_ v b_|_) v (((b ^ a) v (b_|_ ^ a