Theorem ud4lem1b 578

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 280	. . 3 (a ->4 b)' = (((a' v b') ^ (a v b')) ^ ((a ^ b') v 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' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a')))
4		coman2 186	. . . . . . . . . . 11 (b ^ a) C a
5	4	comcom2 183	. . . . . . . . . 10 (b ^ a) C a'
6		coman1 185	. . . . . . . . . . 11 (b ^ a) C b
7	6	comcom2 183	. . . . . . . . . 10 (b ^ a) C b'
8	5, 7	com2or 483	. . . . . . . . 9 (b ^ a) C (a' v b')
9	8	comcom 453	. . . . . . . 8 (a' v b') C (b ^ a)
10		coman2 186	. . . . . . . . . . 11 (b' ^ a) C a
11	10	comcom2 183	. . . . . . . . . 10 (b' ^ a) C a'
12		coman1 185	. . . . . . . . . 10 (b' ^ a) C b'
13	11, 12	com2or 483	. . . . . . . . 9 (b' ^ a) C (a' v b')
14	13	comcom 453	. . . . . . . 8 (a' v b') C (b' ^ a)
15	9, 14	com2or 483	. . . . . . 7 (a' v b') C ((b ^ a) v (b' ^ a))
16	15	comcom 453	. . . . . 6 ((b ^ a) v (b' ^ a)) C (a' v b')
17	4, 7	com2or 483	. . . . . . . . 9 (b ^ a) C (a v b')
18	17	comcom 453	. . . . . . . 8 (a v b') C (b ^ a)
19		comor2 462	. . . . . . . . 9 (a v b') C b'
20		comor1 461	. . . . . . . . 9 (a v b') C a
21	19, 20	com2an 484	. . . . . . . 8 (a v b') C (b' ^ a)
22	18, 21	com2or 483	. . . . . . 7 (a v b') C ((b ^ a) v (b' ^ a))
23	22	comcom 453	. . . . . 6 ((b ^ a) v (b' ^ a)) C (a v b')
24	16, 23	com2an 484	. . . . 5 ((b ^ a) v (b' ^ a)) C ((a' v b') ^ (a v b'))
25		coman2 186	. . . . . . . . . . 11 (a ^ b') C b'
26	25	comcom3 454	. . . . . . . . . 10 (a ^ b')' C b'
27	26	comcom5 458	. . . . . . . . 9 (a ^ b') C b
28		coman1 185	. . . . . . . . 9 (a ^ b') C a
29	27, 28	com2an 484	. . . . . . . 8 (a ^ b') C (b ^ a)
30	25, 28	com2an 484	. . . . . . . 8 (a ^ b') C (b' ^ a)
31	29, 30	com2or 483	. . . . . . 7 (a ^ b') C ((b ^ a) v (b' ^ a))
32	31	comcom 453	. . . . . 6 ((b ^ a) v (b' ^ a)) C (a ^ b')
33	6	comcom 453	. . . . . . . 8 b C (b ^ a)
34	12	comcom 453	. . . . . . . . . 10 b' C (b' ^ a)
35	34	comcom2 183	. . . . . . . . 9 b' C (b' ^ a)'
36	35	comcom5 458	. . . . . . . 8 b C (b' ^ a)
37	33, 36	com2or 483	. . . . . . 7 b C ((b ^ a) v (b' ^ a))
38	37	comcom 453	. . . . . 6 ((b ^ a) v (b' ^ a)) C b
39	32, 38	com2or 483	. . . . 5 ((b ^ a) v (b' ^ a)) C ((a ^ b') v b)
40	24, 39	com2an 484	. . . 4 ((b ^ a) v (b' ^ a)) C (((a' v b') ^ (a v b')) ^ ((a ^ b') v b))
41		comor1 461	. . . . . . . . . 10 (b' v a) C b'
42	41	comcom3 454	. . . . . . . . 9 (b' v a)' C b'
43	42	comcom5 458	. . . . . . . 8 (b' v a) C b
44		comor2 462	. . . . . . . 8 (b' v a) C a
45	43, 44	com2an 484	. . . . . . 7 (b' v a) C (b ^ a)
46	41, 44	com2an 484	. . . . . . 7 (b' v a) C (b' ^ a)
47	45, 46	com2or 483	. . . . . 6 (b' v a) C ((b ^ a) v (b' ^ a))
48	47	comcom 453	. . . . 5 ((b ^ a) v (b' ^ a)) C (b' v a)
49	4	comcom 453	. . . . . . . 8 a C (b ^ a)
50	10	comcom 453	. . . . . . . 8 a C (b' ^ a)
51	49, 50	com2or 483	. . . . . . 7 a C ((b ^ a) v (b' ^ a))
52	51	comcom 453	. . . . . 6 ((b ^ a) v (b' ^ a)) C a
53	52	comcom2 183	. . . . 5 ((b ^ a) v (b' ^ a)) C a'
54	48, 53	com2an 484	. . . 4 ((b ^ a) v (b' ^ a)) C ((b' v a) ^ a')
55	40, 54	fh2 470	. . 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 484	. . . . . . . 8 (b ^ a) C ((a' v b') ^ (a v b'))
57	4, 7	com2an 484	. . . . . . . . 9 (b ^ a) C (a ^ b')
58	57, 6	com2or 483	. . . . . . . 8 (b ^ a) C ((a ^ b') v b)
59	56, 58	com2an 484	. . . . . . 7 (b ^ a) C (((a' v b') ^ (a v b')) ^ ((a ^ b') v b))
60	7, 4	com2an 484	. . . . . . 7 (b ^ a) C (b' ^ a)
61	59, 60	fh2 470	. . . . . 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 83	. . . . . . . . . 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 83	. . . . . . . . . . . . 13 (((a' v b') ^ (a v b')) ^ (b ^ a)) = (((a' v b') ^ (b ^ a)) ^ (a v b'))
64		ax-a2 31	. . . . . . . . . . . . . . . . 17 (a' v b') = (b' v a')
65		df-a 40	. . . . . . . . . . . . . . . . 17 (b ^ a) = (b' v a')'
66	64, 65	2an 79	. . . . . . . . . . . . . . . 16 ((a' v b') ^ (b ^ a)) = ((b' v a') ^ (b' v a')')
67		dff 101	. . . . . . . . . . . . . . . . 17 0 = ((b' v a') ^ (b' v a')')
68	67	ax-r1 35	. . . . . . . . . . . . . . . 16 ((b' v a') ^ (b' v a')') = 0
69	66, 68	ax-r2 36	. . . . . . . . . . . . . . 15 ((a' v b') ^ (b ^ a)) = 0
70	69	ran 78	. . . . . . . . . . . . . 14 (((a' v b') ^ (b ^ a)) ^ (a v b')) = (0 ^ (a v b'))
71		ancom 74	. . . . . . . . . . . . . . 15 (0 ^ (a v b')) = ((a v b') ^ 0)
72		an0 108	. . . . . . . . . . . . . . 15 ((a v b') ^ 0) = 0
73	71, 72	ax-r2 36	. . . . . . . . . . . . . 14 (0 ^ (a v b')) = 0
74	70, 73	ax-r2 36	. . . . . . . . . . . . 13 (((a' v b') ^ (b ^ a)) ^ (a v b')) = 0
75	63, 74	ax-r2 36	. . . . . . . . . . . 12 (((a' v b') ^ (a v b')) ^ (b ^ a)) = 0
76	75	ran 78	. . . . . . . . . . 11 ((((a' v b') ^ (a v b')) ^ (b ^ a)) ^ ((a ^ b') v b)) = (0 ^ ((a ^ b') v b))
77		ancom 74	. . . . . . . . . . . 12 (0 ^ ((a ^ b') v b)) = (((a ^ b') v b) ^ 0)
78		an0 108	. . . . . . . . . . . 12 (((a ^ b') v b) ^ 0) = 0
79	77, 78	ax-r2 36	. . . . . . . . . . 11 (0 ^ ((a ^ b') v b)) = 0
80	76, 79	ax-r2 36	. . . . . . . . . 10 ((((a' v b') ^ (a v b')) ^ (b ^ a)) ^ ((a ^ b') v b)) = 0
81	62, 80	ax-r2 36	. . . . . . . . 9 ((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ (b ^ a)) = 0
82		lea 160	. . . . . . . . . . . . . 14 (b' ^ a) =< b'
83		leor 159	. . . . . . . . . . . . . 14 b' =< (a' v b')
84	82, 83	letr 137	. . . . . . . . . . . . 13 (b' ^ a) =< (a' v b')
85		lear 161	. . . . . . . . . . . . . 14 (b' ^ a) =< a
86		leo 158	. . . . . . . . . . . . . 14 a =< (a v b')
87	85, 86	letr 137	. . . . . . . . . . . . 13 (b' ^ a) =< (a v b')
88	84, 87	ler2an 173	. . . . . . . . . . . 12 (b' ^ a) =< ((a' v b') ^ (a v b'))
89		ancom 74	. . . . . . . . . . . . 13 (b' ^ a) = (a ^ b')
90		leo 158	. . . . . . . . . . . . 13 (a ^ b') =< ((a ^ b') v b)
91	89, 90	bltr 138	. . . . . . . . . . . 12 (b' ^ a