Theorem ud5lem1a 568

Description: Lemma for unified disjunction.

Assertion

Ref	Expression
ud5lem1a	((a ->5 b) ^ (b ->5 a)) = ((a ^ b) v (a_|_ ^ b_|_))

Proof of Theorem ud5lem1a

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