Theorem ud3lem3 558

Description: Lemma for unified disjunction.

Assertion

Ref	Expression
ud3lem3	((a ->3 b) ->3 (a v b)) = (a v b)

Proof of Theorem ud3lem3

Step	Hyp	Ref	Expression
1		df-i3 45	. 2 ((a ->3 b) ->3 (a v b)) = ((((a ->3 b)_|_ ^ (a v b)) v ((a ->3 b)_|_ ^ (a v b)_|_)) v ((a ->3 b) ^ ((a ->3 b)_|_ v (a v b))))
2		ud3lem3a 554	. . . . . . 7 ((a ->3 b)_|_ ^ (a v b)) = (a ->3 b)_|_
3		ud3lem0c 271	. . . . . . 7 (a ->3 b)_|_ = (((a v b_|_) ^ (a v b)) ^ (a_|_ v (a ^ b_|_)))
4	2, 3	ax-r2 35	. . . . . 6 ((a ->3 b)_|_ ^ (a v b)) = (((a v b_|_) ^ (a v b)) ^ (a_|_ v (a ^ b_|_)))
5		ud3lem3b 555	. . . . . 6 ((a ->3 b)_|_ ^ (a v b)_|_) = 0
6	4, 5	2or 67	. . . . 5 (((a ->3 b)_|_ ^ (a v b)) v ((a ->3 b)_|_ ^ (a v b)_|_)) = ((((a v b_|_) ^ (a v b)) ^ (a_|_ v (a ^ b_|_))) v 0)
7		or0 94	. . . . 5 ((((a v b_|_) ^ (a v b)) ^ (a_|_ v (a ^ b_|_))) v 0) = (((a v b_|_) ^ (a v b)) ^ (a_|_ v (a ^ b_|_)))
8	6, 7	ax-r2 35	. . . 4 (((a ->3 b)_|_ ^ (a v b)) v ((a ->3 b)_|_ ^ (a v b)_|_)) = (((a v b_|_) ^ (a v b)) ^ (a_|_ v (a ^ b_|_)))
9		ud3lem3d 557	. . . 4 ((a ->3 b) ^ ((a ->3 b)_|_ v (a v b))) = ((a_|_ ^ b) v (a ^ (a_|_ v b)))
10	8, 9	2or 67	. . 3 ((((a ->3 b)_|_ ^ (a v b)) v ((a ->3 b)_|_ ^ (a v b)_|_)) v ((a ->3 b) ^ ((a ->3 b)_|_ v (a v b)))) = ((((a v b_|_) ^ (a v b)) ^ (a_|_ v (a ^ b_|_))) v ((a_|_ ^ b) v (a ^ (a_|_ v b))))
11		coman1 177	. . . . . . . . . 10 (a_|_ ^ b) C a_|_
12	11	comcom7 442	. . . . . . . . 9 (a_|_ ^ b) C a
13		coman2 178	. . . . . . . . . 10 (a_|_ ^ b) C b
14	13	comcom2 175	. . . . . . . . 9 (a_|_ ^ b) C b_|_
15	12, 14	com2or 465	. . . . . . . 8 (a_|_ ^ b) C (a v b_|_)
16	12, 13	com2or 465	. . . . . . . 8 (a_|_ ^ b) C (a v b)
17	15, 16	com2an 466	. . . . . . 7 (a_|_ ^ b) C ((a v b_|_) ^ (a v b))
18	17	comcom 435	. . . . . 6 ((a v b_|_) ^ (a v b)) C (a_|_ ^ b)
19		comorr 176	. . . . . . . . 9 a C (a v b_|_)
20		comorr 176	. . . . . . . . 9 a C (a v b)
21	19, 20	com2an 466	. . . . . . . 8 a C ((a v b_|_) ^ (a v b))
22	21	comcom 435	. . . . . . 7 ((a v b_|_) ^ (a v b)) C a
23		comor1 443	. . . . . . . . . . 11 (a_|_ v b) C a_|_
24	23	comcom7 442	. . . . . . . . . 10 (a_|_ v b) C a
25		comor2 444	. . . . . . . . . . 11 (a_|_ v b) C b
26	25	comcom2 175	. . . . . . . . . 10 (a_|_ v b) C b_|_
27	24, 26	com2or 465	. . . . . . . . 9 (a_|_ v b) C (a v b_|_)
28	24, 25	com2or 465	. . . . . . . . 9 (a_|_ v b) C (a v b)
29	27, 28	com2an 466	. . . . . . . 8 (a_|_ v b) C ((a v b_|_) ^ (a v b))
30	29	comcom 435	. . . . . . 7 ((a v b_|_) ^ (a v b)) C (a_|_ v b)
31	22, 30	com2an 466	. . . . . 6 ((a v b_|_) ^ (a v b)) C (a ^ (a_|_ v b))
32	18, 31	com2or 465	. . . . 5 ((a v b_|_) ^ (a v b)) C ((a_|_ ^ b) v (a ^ (a_|_ v b)))
33	19	comcom3 436	. . . . . . . 8 a_|_ C (a v b_|_)
34	20	comcom3 436	. . . . . . . 8 a_|_ C (a v b)
35	33, 34	com2an 466	. . . . . . 7 a_|_ C ((a v b_|_) ^ (a v b))
36	35	comcom 435	. . . . . 6 ((a v b_|_) ^ (a v b)) C a_|_
37		coman1 177	. . . . . . . . 9 (a ^ b_|_) C a
38		coman2 178	. . . . . . . . 9 (a ^ b_|_) C b_|_
39	37, 38	com2or 465	. . . . . . . 8 (a ^ b_|_) C (a v b_|_)
40	38	comcom7 442	. . . . . . . . 9 (a ^ b_|_) C b
41	37, 40	com2or 465	. . . . . . . 8 (a ^ b_|_) C (a v b)
42	39, 41	com2an 466	. . . . . . 7 (a ^ b_|_) C ((a v b_|_) ^ (a v b))
43	42	comcom 435	. . . . . 6 ((a v b_|_) ^ (a v b)) C (a ^ b_|_)
44	36, 43	com2or 465	. . . . 5 ((a v b_|_) ^ (a v b)) C (a_|_ v (a ^ b_|_))
45	32, 44	fh4r 458	. . . 4 ((((a v b_|_) ^ (a v b)) ^ (a_|_ v (a ^ b_|_))) v ((a_|_ ^ b) v (a ^ (a_|_ v b)))) = ((((a v b_|_) ^ (a v b)) v ((a_|_ ^ b) v (a ^ (a_|_ v b)))) ^ ((a_|_ v (a ^ b_|_)) v ((a_|_ ^ b) v (a ^ (a_|_ v b)))))
46		comor1 443	. . . . . . . . . . 11 (a v b_|_) C a
47	46	comcom2 175	. . . . . . . . . 10 (a v b_|_) C a_|_
48		comor2 444	. . . . . . . . . . 11 (a v b_|_) C b_|_
49	48	comcom7 442	. . . . . . . . . 10 (a v b_|_) C b
50	47, 49	com2an 466	. . . . . . . . 9 (a v b_|_) C (a_|_ ^ b)
51	47, 49	com2or 465	. . . . . . . . . 10 (a v b_|_) C (a_|_ v b)
52	46, 51	com2an 466	. . . . . . . . 9 (a v b_|_) C (a ^ (a_|_ v b))
53	50, 52	com2or 465	. . . . . . . 8 (a v b_|_) C ((a_|_ ^ b) v (a ^ (a_|_ v b)))
54	46, 49	com2or 465	. . . . . . . 8 (a v b_|_) C (a v b)
55	53, 54	fh4r 458	. . . . . . 7 (((a v b_|_) ^ (a v b)) v ((a_|_ ^ b) v (a ^ (a_|_ v b)))) = (((a v b_|_) v ((a_|_ ^ b) v (a ^ (a_|_ v b)))) ^ ((a v b) v ((a_|_ ^ b) v (a ^ (a_|_ v b)))))
56		ax-a3 31	. . . . . . . . . . 11 (((a v b_|_) v (a_|_ ^ b)) v (a ^ (a_|_ v b))) = ((a v b_|_) v ((a_|_ ^ b) v (a ^ (a_|_ v b))))
57	56	ax-r1 34	. . . . . . . . . 10 ((a v b_|_) v ((a_|_ ^ b) v (a ^ (a_|_ v b)))) = (((a v b_|_) v (a_|_ ^ b)) v (a ^ (a_|_ v b)))
58		anor2 81	. . . . . . . . . . . . . 14 (a_|_ ^ b) = (a v b_|_)_|_
59	58	lor 66	. . . . . . . . . . . . 13 ((a v b_|_) v (a_|_ ^ b)) = ((a v b_|_) v (a v b_|_)_|_)
60		df-t 40	. . . . . . . . . . . . . 14 1 = ((a v b_|_) v (a v b_|_)_|_)
61	60	ax-r1 34	. . . . . . . . . . . . 13 ((a v b_|_) v (a v b_|_)_|_) = 1
62	59, 61	ax-r2 35	. . . . . . . . . . . 12 ((a v b_|_) v (a_|_ ^ b)) = 1
63	62	ax-r5 37	. . . . . . . . . . 11 (((a v b_|_) v (a_|_ ^ b)) v (a ^ (a_|_ v b))) = (1 v (a ^ (a_|_ v b)))
64		or1r 97	. . . . . . . . . . 11 (1 v (a ^ (a_|_ v b))) = 1
65	63, 64	ax-r2 35	. . . . . . . . . 10 (((a v b_|_) v (a_|_ ^ b)) v (a ^ (a_|_ v b))) = 1
66	57, 65	ax-r2 35	. . . . . . . . 9 ((a v b_|_) v ((a_|_ ^ b) v (a ^ (a_|_ v b)))) = 1
67		ax-a2 30	. . . . . . . . . 10 ((a v b) v ((a_|_ ^ b) v (a ^ (a_|_ v b)))) = (((a_|_ ^ b) v (a ^ (a_|_ v b))) v (a v b))
68		lear 153	. . . . . . . . . . . . 13 (a_|_ ^ b) =< b
69		leor 151	. . . . . . . . . . . . 13 b =< (a v b)
70	68, 69	letr 129	. . . . . . . . . . . 12 (a_|_ ^ b) =< (a v b)
71		lea 152	. . . . . . . . . . . . 13 (a ^ (a_|_ v b)) =< a
72		leo 150	. . . . . . . . . . . . 13 a =< (a v b)
73	71, 72	letr 129	. . . . . . . . . . . 12 (a ^ (a_|_ v b)) =< (a v b)
74	70, 73	lel2or 162	. . . . . . . . . . 11 ((a_|_ ^ b) v (a ^ (a_|_ v b))) =< (a v b)
75	74	df-le2 123	. . . . . . . . . 10 (((a_|_ ^ b) v (a ^ (a_|_ v b))) v (a v b)) = (a v b)
76	67, 75	ax-r2 35	. . . . . . . . 9 ((a v b) v ((a_|_ ^ b) v (a ^ (a_|_ v b)))) = (a v b)
77	66, 76	2an 72	. . . . . . . 8 (((a v b_|_) v ((a_|_ ^ b) v (a ^ (a_|_ v b)))) ^ ((a v b) v ((a_|_ ^ b) v (a ^ (a_|_ v b))))) = (1 ^ (a v b))
78		an1r 99	. . . . . . . 8 (1 ^ (a v b)) = (a v b)
79	77, 78	ax-r2 35	. . . . . . 7 (((a v b_|_) v ((a_|_ ^ b) v (a ^ (a_|_ v b)))) ^ ((a v b) v ((a_|_ ^ b) v (a ^ (a_|_ v b))))) = (a v