Theorem ud5lem1 571

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 47	. 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 568	. . . . 5 ((a ->5 b) ^ (b ->5 a)) = ((a ^ b) v (a_|_ ^ b_|_))
3		ud5lem1b 569	. . . . 5 ((a ->5 b)_|_ ^ (b ->5 a)) = (a ^ b_|_)
4	2, 3	2or 67	. . . 4 (((a ->5 b) ^ (b ->5 a)) v ((a ->5 b)_|_ ^ (b ->5 a))) = (((a ^ b) v (a_|_ ^ b_|_)) v (a ^ b_|_))
5		ud5lem1c 570	. . . 4 ((a ->5 b)_|_ ^ (b ->5 a)_|_) = (((a v b) ^ (a v b_|_)) ^ ((a_|_ v b) ^ (a_|_ v b_|_)))
6	4, 5	2or 67	. . 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 177	. . . . . . . . . 10 (a ^ b) C a
8		coman2 178	. . . . . . . . . 10 (a ^ b) C b
9	7, 8	com2or 465	. . . . . . . . 9 (a ^ b) C (a v b)
10	8	comcom2 175	. . . . . . . . . 10 (a ^ b) C b_|_
11	7, 10	com2or 465	. . . . . . . . 9 (a ^ b) C (a v b_|_)
12	9, 11	com2an 466	. . . . . . . 8 (a ^ b) C ((a v b) ^ (a v b_|_))
13	12	comcom 435	. . . . . . 7 ((a v b) ^ (a v b_|_)) C (a ^ b)
14		coman1 177	. . . . . . . . . . 11 (a_|_ ^ b_|_) C a_|_
15	14	comcom7 442	. . . . . . . . . 10 (a_|_ ^ b_|_) C a
16		coman2 178	. . . . . . . . . . 11 (a_|_ ^ b_|_) C b_|_
17	16	comcom7 442	. . . . . . . . . 10 (a_|_ ^ b_|_) C b
18	15, 17	com2or 465	. . . . . . . . 9 (a_|_ ^ b_|_) C (a v b)
19	15, 16	com2or 465	. . . . . . . . 9 (a_|_ ^ b_|_) C (a v b_|_)
20	18, 19	com2an 466	. . . . . . . 8 (a_|_ ^ b_|_) C ((a v b) ^ (a v b_|_))
21	20	comcom 435	. . . . . . 7 ((a v b) ^ (a v b_|_)) C (a_|_ ^ b_|_)
22	13, 21	com2or 465	. . . . . 6 ((a v b) ^ (a v b_|_)) C ((a ^ b) v (a_|_ ^ b_|_))
23		coman1 177	. . . . . . . . 9 (a ^ b_|_) C a
24		coman2 178	. . . . . . . . . 10 (a ^ b_|_) C b_|_
25	24	comcom7 442	. . . . . . . . 9 (a ^ b_|_) C b
26	23, 25	com2or 465	. . . . . . . 8 (a ^ b_|_) C (a v b)
27	23, 24	com2or 465	. . . . . . . 8 (a ^ b_|_) C (a v b_|_)
28	26, 27	com2an 466	. . . . . . 7 (a ^ b_|_) C ((a v b) ^ (a v b_|_))
29	28	comcom 435	. . . . . 6 ((a v b) ^ (a v b_|_)) C (a ^ b_|_)
30	22, 29	com2or 465	. . . . 5 ((a v b) ^ (a v b_|_)) C (((a ^ b) v (a_|_ ^ b_|_)) v (a ^ b_|_))
31		comor1 443	. . . . . . . . . 10 (a_|_ v b) C a_|_
32	31	comcom7 442	. . . . . . . . 9 (a_|_ v b) C a
33		comor2 444	. . . . . . . . 9 (a_|_ v b) C b
34	32, 33	com2or 465	. . . . . . . 8 (a_|_ v b) C (a v b)
35	33	comcom2 175	. . . . . . . . 9 (a_|_ v b) C b_|_
36	32, 35	com2or 465	. . . . . . . 8 (a_|_ v b) C (a v b_|_)
37	34, 36	com2an 466	. . . . . . 7 (a_|_ v b) C ((a v b) ^ (a v b_|_))
38	37	comcom 435	. . . . . 6 ((a v b) ^ (a v b_|_)) C (a_|_ v b)
39		comor1 443	. . . . . . . . . 10 (a_|_ v b_|_) C a_|_
40	39	comcom7 442	. . . . . . . . 9 (a_|_ v b_|_) C a
41		comor2 444	. . . . . . . . . 10 (a_|_ v b_|_) C b_|_
42	41	comcom7 442	. . . . . . . . 9 (a_|_ v b_|_) C b
43	40, 42	com2or 465	. . . . . . . 8 (a_|_ v b_|_) C (a v b)
44	40, 41	com2or 465	. . . . . . . 8 (a_|_ v b_|_) C (a v b_|_)
45	43, 44	com2an 466	. . . . . . 7 (a_|_ v b_|_) C ((a v b) ^ (a v b_|_))
46	45	comcom 435	. . . . . 6 ((a v b) ^ (a v b_|_)) C (a_|_ v b_|_)
47	38, 46	com2an 466	. . . . 5 ((a v b) ^ (a v b_|_)) C ((a_|_ v b) ^ (a_|_ v b_|_))
48	30, 47	fh4 454	. . . 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 443	. . . . . . . . . . 11 (a v b) C a
50		comor2 444	. . . . . . . . . . 11 (a v b) C b
51	49, 50	com2an 466	. . . . . . . . . 10 (a v b) C (a ^ b)
52	49	comcom2 175	. . . . . . . . . . 11 (a v b) C a_|_
53	50	comcom2 175	. . . . . . . . . . 11 (a v b) C b_|_
54	52, 53	com2an 466	. . . . . . . . . 10 (a v b) C (a_|_ ^ b_|_)
55	51, 54	com2or 465	. . . . . . . . 9 (a v b) C ((a ^ b) v (a_|_ ^ b_|_))
56	49, 53	com2an 466	. . . . . . . . 9 (a v b) C (a ^ b_|_)
57	55, 56	com2or 465	. . . . . . . 8 (a v b) C (((a ^ b) v (a_|_ ^ b_|_)) v (a ^ b_|_))
58	49, 53	com2or 465	. . . . . . . 8 (a v b) C (a v b_|_)
59	57, 58	fh4 454	. . . . . . 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 75	. . . . . . . . . 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 31	. . . . . . . . . . . . 13 (((a ^ b) v (a_|_ ^ b_|_)) v (a v b)) = ((a ^ b) v ((a_|_ ^ b_|_) v (a v b)))
62		oran 79	. . . . . . . . . . . . . . . . 17 (a v b) = (a_|_ ^ b_|_)_|_
63	62	lor 66	. . . . . . . . . . . . . . . 16 ((a_|_ ^ b_|_) v (a v b)) = ((a_|_ ^ b_|_) v (a_|_ ^ b_|_)_|_)
64		df-t 40	. . . . . . . . . . . . . . . . 17 1 = ((a_|_ ^ b_|_) v (a_|_ ^ b_|_)_|_)
65	64	ax-r1 34	. . . . . . . . . . . . . . . 16 ((a_|_ ^ b_|_) v (a_|_ ^ b_|_)_|_) = 1
66	63, 65	ax-r2 35	. . . . . . . . . . . . . . 15 ((a_|_ ^ b_|_) v (a v b)) = 1
67	66	lor 66	. . . . . . . . . . . . . 14 ((a ^ b) v ((a_|_ ^ b_|_) v (a v b))) = ((a ^ b) v 1)
68		or1 96	. . . . . . . . . . . . . 14 ((a ^ b) v 1) = 1
69	67, 68	ax-r2 35	. . . . . . . . . . . . 13 ((a ^ b) v ((a_|_ ^ b_|_) v (a v b))) = 1
70	61, 69	ax-r2 35	. . . . . . . . . . . 12 (((a ^ b) v (a_|_ ^ b_|_)) v (a v b)) = 1
71	70	ax-r5 37	. . . . . . . . . . 11 ((((a ^ b) v (a_|_ ^ b_|_)) v (a v b)) v (a ^ b_|_)) = (1 v (a ^ b_|_))
72		or1r 97	. . . . . . . . . . 11 (1 v (a ^ b_|_)) = 1
73	71, 72	ax-r2 35	. . . . . . . . . 10 ((((a ^ b) v (a_|_ ^ b_|_)) v (a v b)) v (a ^ b_|_)) = 1
74	60, 73	ax-r2 35	. . . . . . . . 9 ((((a ^ b) v (a_|_ ^ b_|_)) v (a ^ b_|_)) v (a v b)) = 1
75		lea 152	. . . . . . . . . . . . 13 (a ^ b) =< a
76		leo 150	. . . . . . . . . . . . 13 a =< (a v b_|_)
77	75, 76	letr 129	. . . . . . . . . . . 12 (a ^ b) =< (a v b_|_)
78		lear 153	. . . . . . . . . . . . 13 (a_|_ ^ b_|_) =< b_|_
79		leor 151	. . . . . . . . . . . . 13 b_|_ =< (a v b_|_)
80	78, 79	letr 129	. . . . . . . . . . . 12 (a_|_ ^ b_|_) =< (a v b_|_)
81	77, 80	lel2or 162	. . . . . . . . . . 11 ((a ^ b) v (a_|_ ^ b_|_)) =< (a v b_|_)
82		lea 152	. . . . . . . . . . . 12 (a ^ b_|_) =< a
83	82, 76	letr 129	. . . . . . . . . . 11 (a ^ b_|_) =< (a v b_|_)
84	81, 83	lel2or 162	. . . . . . . . . 10 (((a ^ b) v (a_|_ ^ b_|_)) v (a ^ b_|_)) =< (a v b_|_)
85	84	df-le2 123	. . . . . . . . 9 ((((a ^ b) v (a_|_ ^ b_|_)) v (a ^ b_|_)) v (a v b_|_)) = (a v b_|_)
86	74, 85	2an 72	. . . . . . . 8 (((((a ^ b) v (a_|_ ^ b_|_)) v (a ^ b_|_)) v (a v b)) ^ ((((a ^ b) v (a_|_ ^ b_|_)) v (a ^ b_|_)) v (a v b_|_))) = (1 ^