Theorem ud5lem1 589

Description: Lemma for unified disjunction.

Assertion

Ref	Expression
ud5lem1	((a ->5 b) ->5 (b ->5 a)) = (a v b')

Proof of Theorem ud5lem1

Step	Hyp	Ref	Expression
1		df-i5 48	. 2 ((a ->5 b) ->5 (b ->5 a)) = ((((a ->5 b) ^ (b ->5 a)) v ((a ->5 b)' ^ (b ->5 a))) v ((a ->5 b)' ^ (b ->5 a)'))
2		ud5lem1a 586	. . . . 5 ((a ->5 b) ^ (b ->5 a)) = ((a ^ b) v (a' ^ b'))
3		ud5lem1b 587	. . . . 5 ((a ->5 b)' ^ (b ->5 a)) = (a ^ b')
4	2, 3	2or 72	. . . 4 (((a ->5 b) ^ (b ->5 a)) v ((a ->5 b)' ^ (b ->5 a))) = (((a ^ b) v (a' ^ b')) v (a ^ b'))
5		ud5lem1c 588	. . . 4 ((a ->5 b)' ^ (b ->5 a)') = (((a v b) ^ (a v b')) ^ ((a' v b) ^ (a' v b')))
6	4, 5	2or 72	. . 3 ((((a ->5 b) ^ (b ->5 a)) v ((a ->5 b)' ^ (b ->5 a))) v ((a ->5 b)' ^ (b ->5 a)')) = ((((a ^ b) v (a' ^ b')) v (a ^ b')) v (((a v b) ^ (a v b')) ^ ((a' v b) ^ (a' v b'))))
7		coman1 185	. . . . . . . . . 10 (a ^ b) C a
8		coman2 186	. . . . . . . . . 10 (a ^ b) C b
9	7, 8	com2or 483	. . . . . . . . 9 (a ^ b) C (a v b)
10	8	comcom2 183	. . . . . . . . . 10 (a ^ b) C b'
11	7, 10	com2or 483	. . . . . . . . 9 (a ^ b) C (a v b')
12	9, 11	com2an 484	. . . . . . . 8 (a ^ b) C ((a v b) ^ (a v b'))
13	12	comcom 453	. . . . . . 7 ((a v b) ^ (a v b')) C (a ^ b)
14		coman1 185	. . . . . . . . . . 11 (a' ^ b') C a'
15	14	comcom7 460	. . . . . . . . . 10 (a' ^ b') C a
16		coman2 186	. . . . . . . . . . 11 (a' ^ b') C b'
17	16	comcom7 460	. . . . . . . . . 10 (a' ^ b') C b
18	15, 17	com2or 483	. . . . . . . . 9 (a' ^ b') C (a v b)
19	15, 16	com2or 483	. . . . . . . . 9 (a' ^ b') C (a v b')
20	18, 19	com2an 484	. . . . . . . 8 (a' ^ b') C ((a v b) ^ (a v b'))
21	20	comcom 453	. . . . . . 7 ((a v b) ^ (a v b')) C (a' ^ b')
22	13, 21	com2or 483	. . . . . 6 ((a v b) ^ (a v b')) C ((a ^ b) v (a' ^ b'))
23		coman1 185	. . . . . . . . 9 (a ^ b') C a
24		coman2 186	. . . . . . . . . 10 (a ^ b') C b'
25	24	comcom7 460	. . . . . . . . 9 (a ^ b') C b
26	23, 25	com2or 483	. . . . . . . 8 (a ^ b') C (a v b)
27	23, 24	com2or 483	. . . . . . . 8 (a ^ b') C (a v b')
28	26, 27	com2an 484	. . . . . . 7 (a ^ b') C ((a v b) ^ (a v b'))
29	28	comcom 453	. . . . . 6 ((a v b) ^ (a v b')) C (a ^ b')
30	22, 29	com2or 483	. . . . 5 ((a v b) ^ (a v b')) C (((a ^ b) v (a' ^ b')) v (a ^ b'))
31		comor1 461	. . . . . . . . . 10 (a' v b) C a'
32	31	comcom7 460	. . . . . . . . 9 (a' v b) C a
33		comor2 462	. . . . . . . . 9 (a' v b) C b
34	32, 33	com2or 483	. . . . . . . 8 (a' v b) C (a v b)
35	33	comcom2 183	. . . . . . . . 9 (a' v b) C b'
36	32, 35	com2or 483	. . . . . . . 8 (a' v b) C (a v b')
37	34, 36	com2an 484	. . . . . . 7 (a' v b) C ((a v b) ^ (a v b'))
38	37	comcom 453	. . . . . 6 ((a v b) ^ (a v b')) C (a' v b)
39		comor1 461	. . . . . . . . . 10 (a' v b') C a'
40	39	comcom7 460	. . . . . . . . 9 (a' v b') C a
41		comor2 462	. . . . . . . . . 10 (a' v b') C b'
42	41	comcom7 460	. . . . . . . . 9 (a' v b') C b
43	40, 42	com2or 483	. . . . . . . 8 (a' v b') C (a v b)
44	40, 41	com2or 483	. . . . . . . 8 (a' v b') C (a v b')
45	43, 44	com2an 484	. . . . . . 7 (a' v b') C ((a v b) ^ (a v b'))
46	45	comcom 453	. . . . . 6 ((a v b) ^ (a v b')) C (a' v b')
47	38, 46	com2an 484	. . . . 5 ((a v b) ^ (a v b')) C ((a' v b) ^ (a' v b'))
48	30, 47	fh4 472	. . . 4 ((((a ^ b) v (a' ^ b')) v (a ^ b')) v (((a v b) ^ (a v b')) ^ ((a' v b) ^ (a' v b')))) = (((((a ^ b) v (a' ^ b')) v (a ^ b')) v ((a v b) ^ (a v b'))) ^ ((((a ^ b) v (a' ^ b')) v (a ^ b')) v ((a' v b) ^ (a' v b'))))
49		comor1 461	. . . . . . . . . . 11 (a v b) C a
50		comor2 462	. . . . . . . . . . 11 (a v b) C b
51	49, 50	com2an 484	. . . . . . . . . 10 (a v b) C (a ^ b)
52	49	comcom2 183	. . . . . . . . . . 11 (a v b) C a'
53	50	comcom2 183	. . . . . . . . . . 11 (a v b) C b'
54	52, 53	com2an 484	. . . . . . . . . 10 (a v b) C (a' ^ b')
55	51, 54	com2or 483	. . . . . . . . 9 (a v b) C ((a ^ b) v (a' ^ b'))
56	49, 53	com2an 484	. . . . . . . . 9 (a v b) C (a ^ b')
57	55, 56	com2or 483	. . . . . . . 8 (a v b) C (((a ^ b) v (a' ^ b')) v (a ^ b'))
58	49, 53	com2or 483	. . . . . . . 8 (a v b) C (a v b')
59	57, 58	fh4 472	. . . . . . 7 ((((a ^ b) v (a' ^ b')) v (a ^ b')) v ((a v b) ^ (a v b'))) = (((((a ^ b) v (a' ^ b')) v (a ^ b')) v (a v b)) ^ ((((a ^ b) v (a' ^ b')) v (a ^ b')) v (a v b')))
60		or32 82	. . . . . . . . . 10 ((((a ^ b) v (a' ^ b')) v (a ^ b')) v (a v b)) = ((((a ^ b) v (a' ^ b')) v (a v b)) v (a ^ b'))
61		ax-a3 32	. . . . . . . . . . . . 13 (((a ^ b) v (a' ^ b')) v (a v b)) = ((a ^ b) v ((a' ^ b') v (a v b)))
62		oran 87	. . . . . . . . . . . . . . . . 17 (a v b) = (a' ^ b')'
63	62	lor 70	. . . . . . . . . . . . . . . 16 ((a' ^ b') v (a v b)) = ((a' ^ b') v (a' ^ b')')
64		df-t 41	. . . . . . . . . . . . . . . . 17 1 = ((a' ^ b') v (a' ^ b')')
65	64	ax-r1 35	. . . . . . . . . . . . . . . 16 ((a' ^ b') v (a' ^ b')') = 1
66	63, 65	ax-r2 36	. . . . . . . . . . . . . . 15 ((a' ^ b') v (a v b)) = 1
67	66	lor 70	. . . . . . . . . . . . . 14 ((a ^ b) v ((a' ^ b') v (a v b))) = ((a ^ b) v 1)
68		or1 104	. . . . . . . . . . . . . 14 ((a ^ b) v 1) = 1
69	67, 68	ax-r2 36	. . . . . . . . . . . . 13 ((a ^ b) v ((a' ^ b') v (a v b))) = 1
70	61, 69	ax-r2 36	. . . . . . . . . . . 12 (((a ^ b) v (a' ^ b')) v (a v b)) = 1
71	70	ax-r5 38	. . . . . . . . . . 11 ((((a ^ b) v (a' ^ b')) v (a v b)) v (a ^ b')) = (1 v (a ^ b'))
72		or1r 105	. . . . . . . . . . 11 (1 v (a ^ b')) = 1
73	71, 72	ax-r2 36	. . . . . . . . . 10 ((((a ^ b) v (a' ^ b')) v (a v b)) v (a ^ b')) = 1
74	60, 73	ax-r2 36	. . . . . . . . 9 ((((a ^ b) v (a' ^ b')) v (a ^ b')) v (a v b)) = 1
75		lea 160	. . . . . . . . . . . . 13 (a ^ b) =< a
76		leo 158	. . . . . . . . . . . . 13 a =< (a v b')
77	75, 76	letr 137	. . . . . . . . . . . 12 (a ^ b) =< (a v b')
78		lear 161	. . . . . . . . . . . . 13 (a' ^ b') =< b'
79		leor 159	. . . . . . . . . . . . 13 b' =< (a v b')
80	78, 79	letr 137	. . . . . . . . . . . 12 (a' ^ b') =< (a v b')
81	77, 80	lel2or 170	. . . . . . . . . . 11 ((a ^ b) v (a' ^ b')) =< (a v b')
82		lea 160	. . . . . . . . . . . 12 (a ^ b') =< a
83	82, 76	letr 137	. . . . . . . . . . 11 (a ^ b') =< (a v b')
84	81, 83	lel2or 170	. . . . . . . . . 10 (((a ^ b) v (a' ^ b')) v (a ^ b')) =< (a v b')
85	84	df-le2 131	. . . . . . . . 9 ((((a ^ b) v (a' ^ b')) v (a ^ b')) v (a v b')) = (a v b')
86	74, 85	2an 79	. . . . . . . 8 (((((a ^ b) v (a' ^ b')) v (a