Theorem ud4lem1a 577

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 47	. . 3 (a ->4 b) = (((a ^ b) v (a' ^ b)) v ((a' v b) ^ b'))
2		df-i4 47	. . 3 (b ->4 a) = (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))
3	1, 2	2an 79	. 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 186	. . . . . . . . . 10 (a ^ b) C b
5	4	comcom 453	. . . . . . . . 9 b C (a ^ b)
6		coman2 186	. . . . . . . . . 10 (a' ^ b) C b
7	6	comcom 453	. . . . . . . . 9 b C (a' ^ b)
8	5, 7	com2or 483	. . . . . . . 8 b C ((a ^ b) v (a' ^ b))
9	8	comcom 453	. . . . . . 7 ((a ^ b) v (a' ^ b)) C b
10		coman1 185	. . . . . . . . . 10 (a ^ b) C a
11	10	comcom 453	. . . . . . . . 9 a C (a ^ b)
12		coman1 185	. . . . . . . . . . . 12 (a' ^ b) C a'
13	12	comcom 453	. . . . . . . . . . 11 a' C (a' ^ b)
14	13	comcom2 183	. . . . . . . . . 10 a' C (a' ^ b)'
15	14	comcom5 458	. . . . . . . . 9 a C (a' ^ b)
16	11, 15	com2or 483	. . . . . . . 8 a C ((a ^ b) v (a' ^ b))
17	16	comcom 453	. . . . . . 7 ((a ^ b) v (a' ^ b)) C a
18	9, 17	com2an 484	. . . . . 6 ((a ^ b) v (a' ^ b)) C (b ^ a)
19	5	comcom3 454	. . . . . . . . 9 b' C (a ^ b)
20	7	comcom3 454	. . . . . . . . 9 b' C (a' ^ b)
21	19, 20	com2or 483	. . . . . . . 8 b' C ((a ^ b) v (a' ^ b))
22	21	comcom 453	. . . . . . 7 ((a ^ b) v (a' ^ b)) C b'
23	22, 17	com2an 484	. . . . . 6 ((a ^ b) v (a' ^ b)) C (b' ^ a)
24	18, 23	com2or 483	. . . . 5 ((a ^ b) v (a' ^ b)) C ((b ^ a) v (b' ^ a))
25	22, 17	com2or 483	. . . . . 6 ((a ^ b) v (a' ^ b)) C (b' v a)
26	11	comcom3 454	. . . . . . . 8 a' C (a ^ b)
27	26, 13	com2or 483	. . . . . . 7 a' C ((a ^ b) v (a' ^ b))
28	27	comcom 453	. . . . . 6 ((a ^ b) v (a' ^ b)) C a'
29	25, 28	com2an 484	. . . . 5 ((a ^ b) v (a' ^ b)) C ((b' v a) ^ a')
30	24, 29	com2or 483	. . . 4 ((a ^ b) v (a' ^ b)) C (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))
31	28, 9	com2or 483	. . . . 5 ((a ^ b) v (a' ^ b)) C (a' v b)
32	9	comcom2 183	. . . . 5 ((a ^ b) v (a' ^ b)) C b'
33	31, 32	com2an 484	. . . 4 ((a ^ b) v (a' ^ b)) C ((a' v b) ^ b')
34	30, 33	fh2r 474	. . 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 74	. . . . . . . . 9 (b ^ a) = (a ^ b)
36		ancom 74	. . . . . . . . 9 (b' ^ a) = (a ^ b')
37	35, 36	2or 72	. . . . . . . 8 ((b ^ a) v (b' ^ a)) = ((a ^ b) v (a ^ b'))
38		ax-a2 31	. . . . . . . . 9 (b' v a) = (a v b')
39	38	ran 78	. . . . . . . 8 ((b' v a) ^ a') = ((a v b') ^ a')
40	37, 39	2or 72	. . . . . . 7 (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a')) = (((a ^ b) v (a ^ b')) v ((a v b') ^ a'))
41	40	lan 77	. . . . . 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 484	. . . . . . . . 9 ((a ^ b) v (a' ^ b)) C (a ^ b)
43	17, 22	com2an 484	. . . . . . . . 9 ((a ^ b) v (a' ^ b)) C (a ^ b')
44	42, 43	com2or 483	. . . . . . . 8 ((a ^ b) v (a' ^ b)) C ((a ^ b) v (a ^ b'))
45	17, 32	com2or 483	. . . . . . . . 9 ((a ^ b) v (a' ^ b)) C (a v b')
46	45, 28	com2an 484	. . . . . . . 8 ((a ^ b) v (a' ^ b)) C ((a v b') ^ a')
47	44, 46	fh1 469	. . . . . . 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 86	. . . . . . . . . . 11 ((a' ^ b) ^ (a ^ b')) = ((a' ^ a) ^ (b ^ b'))
49		dff 101	. . . . . . . . . . . . . 14 0 = (b ^ b')
50	49	ax-r1 35	. . . . . . . . . . . . 13 (b ^ b') = 0
51	50	lan 77	. . . . . . . . . . . 12 ((a' ^ a) ^ (b ^ b')) = ((a' ^ a) ^ 0)
52		an0 108	. . . . . . . . . . . 12 ((a' ^ a) ^ 0) = 0
53	51, 52	ax-r2 36	. . . . . . . . . . 11 ((a' ^ a) ^ (b ^ b')) = 0
54	48, 53	ax-r2 36	. . . . . . . . . 10 ((a' ^ b) ^ (a ^ b')) = 0
55	54	lor 70	. . . . . . . . 9 ((a ^ b) v ((a' ^ b) ^ (a ^ b'))) = ((a ^ b) v 0)
56	10	comcom2 183	. . . . . . . . . . 11 (a ^ b) C a'
57	56, 4	com2an 484	. . . . . . . . . 10 (a ^ b) C (a' ^ b)
58	4	comcom2 183	. . . . . . . . . . 11 (a ^ b) C b'
59	10, 58	com2an 484	. . . . . . . . . 10 (a ^ b) C (a ^ b')
60	57, 59	fh3 471	. . . . . . . . 9 ((a ^ b) v ((a' ^ b) ^ (a ^ b'))) = (((a ^ b) v (a' ^ b)) ^ ((a ^ b) v (a ^ b')))
61		or0 102	. . . . . . . . 9 ((a ^ b) v 0) = (a ^ b)
62	55, 60, 61	3tr2 64	. . . . . . . 8 (((a ^ b) v (a' ^ b)) ^ ((a ^ b) v (a ^ b'))) = (a ^ b)
63	10, 58	com2or 483	. . . . . . . . . . 11 (a ^ b) C (a v b')
64	63, 56	com2an 484	. . . . . . . . . 10 (a ^ b) C ((a v b') ^ a')
65	64, 57	fh2r 474	. . . . . . . . 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 81	. . . . . . . . . . . 12 ((a ^ b) ^ ((a v b') ^ a')) = ((a v b') ^ ((a ^ b) ^ a'))
67		an32 83	. . . . . . . . . . . . . . 15 ((a ^ b) ^ a') = ((a ^ a') ^ b)
68		ancom 74	. . . . . . . . . . . . . . . 16 ((a ^ a') ^ b) = (b ^ (a ^ a'))
69		dff 101	. . . . . . . . . . . . . . . . . . 19 0 = (a ^ a')
70	69	ax-r1 35	. . . . . . . . . . . . . . . . . 18 (a ^ a') = 0
71	70	lan 77	. . . . . . . . . . . . . . . . 17 (b ^ (a ^ a')) = (b ^ 0)
72		an0 108	. . . . . . . . . . . . . . . . 17 (b ^ 0) = 0
73	71, 72	ax-r2 36	. . . . . . . . . . . . . . . 16 (b ^ (a ^ a')) = 0
74	68, 73	ax-r2 36	. . . . . . . . . . . . . . 15 ((a ^ a') ^ b) = 0
75	67, 74	ax-r2 36	. . . . . . . . . . . . . 14 ((a ^ b) ^ a') = 0
76	75	lan 77	. . . . . . . . . . . . 13 ((a v b') ^ ((a ^ b) ^ a')) = ((a v b') ^ 0)
77		an0 108	. . . . . . . . . . . . 13 ((a v b') ^ 0) = 0
78	76, 77	ax-r2 36	. . . . . . . . . . . 12 ((a v b') ^ ((a ^ b) ^ a')) = 0
79	66, 78	ax-r2 36	. . . . . . . . . . 11 ((a ^ b) ^ ((a v b') ^ a')) = 0
80		ancom 74	. . . . . . . . . . . 12 (((a' ^ b) ^ (a v b')) ^ a') = (a' ^ ((a' ^ b) ^ (a v b')))
81		anass 76	. . . . . . . . . . . 12 (((a' ^ b) ^ (a v b')) ^ a') = ((a' ^ b) ^ ((a v b') ^ a'))
82		anor2 89	. . . . . . . . . . . . . . . . . 18 (a' ^ b) = (a v b')'
83	82