Theorem ud5lem3 576

Description: Lemma for unified disjunction.

Assertion

Ref	Expression
ud5lem3	((a ->5 b) ->5 (a v (a_|_ ^ b))) = (a v b)

Proof of Theorem ud5lem3

Step	Hyp	Ref	Expression
1		df-i5 47	. 2 ((a ->5 b) ->5 (a v (a_|_ ^ b))) = ((((a ->5 b) ^ (a v (a_|_ ^ b))) v ((a ->5 b)_|_ ^ (a v (a_|_ ^ b)))) v ((a ->5 b)_|_ ^ (a v (a_|_ ^ b))_|_))
2		ud5lem3a 573	. . . . 5 ((a ->5 b) ^ (a v (a_|_ ^ b))) = ((a ^ b) v (a_|_ ^ b))
3		ud5lem3b 574	. . . . 5 ((a ->5 b)_|_ ^ (a v (a_|_ ^ b))) = (a ^ (a_|_ v b_|_))
4	2, 3	2or 67	. . . 4 (((a ->5 b) ^ (a v (a_|_ ^ b))) v ((a ->5 b)_|_ ^ (a v (a_|_ ^ b)))) = (((a ^ b) v (a_|_ ^ b)) v (a ^ (a_|_ v b_|_)))
5		ud5lem3c 575	. . . 4 ((a ->5 b)_|_ ^ (a v (a_|_ ^ b))_|_) = (((a v b) ^ (a v b_|_)) ^ a_|_)
6	4, 5	2or 67	. . 3 ((((a ->5 b) ^ (a v (a_|_ ^ b))) v ((a ->5 b)_|_ ^ (a v (a_|_ ^ b)))) v ((a ->5 b)_|_ ^ (a v (a_|_ ^ b))_|_)) = ((((a ^ b) v (a_|_ ^ b)) v (a ^ (a_|_ v b_|_))) v (((a v b) ^ (a v b_|_)) ^ a_|_))
7		ax-a3 31	. . . 4 ((((a ^ b) v (a_|_ ^ b)) v (a ^ (a_|_ v b_|_))) v (((a v b) ^ (a v b_|_)) ^ a_|_)) = (((a ^ b) v (a_|_ ^ b)) v ((a ^ (a_|_ v b_|_)) v (((a v b) ^ (a v b_|_)) ^ a_|_)))
8		or4 77	. . . . 5 (((a ^ b) v (a_|_ ^ b)) v ((a ^ (a_|_ v b_|_)) v (((a v b) ^ (a v b_|_)) ^ a_|_))) = (((a ^ b) v (a ^ (a_|_ v b_|_))) v ((a_|_ ^ b) v (((a v b) ^ (a v b_|_)) ^ a_|_)))
9		comanr1 446	. . . . . . . . 9 a C (a ^ b)
10		comorr 176	. . . . . . . . . 10 a_|_ C (a_|_ v b_|_)
11	10	comcom6 441	. . . . . . . . 9 a C (a_|_ v b_|_)
12	9, 11	fh4 454	. . . . . . . 8 ((a ^ b) v (a ^ (a_|_ v b_|_))) = (((a ^ b) v a) ^ ((a ^ b) v (a_|_ v b_|_)))
13		ax-a2 30	. . . . . . . . . . 11 ((a ^ b) v a) = (a v (a ^ b))
14		a5b 112	. . . . . . . . . . 11 (a v (a ^ b)) = a
15	13, 14	ax-r2 35	. . . . . . . . . 10 ((a ^ b) v a) = a
16		df-a 39	. . . . . . . . . . . . . 14 (a ^ b) = (a_|_ v b_|_)_|_
17	16	ax-r1 34	. . . . . . . . . . . . 13 (a_|_ v b_|_)_|_ = (a ^ b)
18	17	con3 65	. . . . . . . . . . . 12 (a_|_ v b_|_) = (a ^ b)_|_
19	18	lor 66	. . . . . . . . . . 11 ((a ^ b) v (a_|_ v b_|_)) = ((a ^ b) v (a ^ b)_|_)
20		df-t 40	. . . . . . . . . . . 12 1 = ((a ^ b) v (a ^ b)_|_)
21	20	ax-r1 34	. . . . . . . . . . 11 ((a ^ b) v (a ^ b)_|_) = 1
22	19, 21	ax-r2 35	. . . . . . . . . 10 ((a ^ b) v (a_|_ v b_|_)) = 1
23	15, 22	2an 72	. . . . . . . . 9 (((a ^ b) v a) ^ ((a ^ b) v (a_|_ v b_|_))) = (a ^ 1)
24		an1 98	. . . . . . . . 9 (a ^ 1) = a
25	23, 24	ax-r2 35	. . . . . . . 8 (((a ^ b) v a) ^ ((a ^ b) v (a_|_ v b_|_))) = a
26	12, 25	ax-r2 35	. . . . . . 7 ((a ^ b) v (a ^ (a_|_ v b_|_))) = a
27		coman1 177	. . . . . . . . . . . 12 (a_|_ ^ b) C a_|_
28	27	comcom7 442	. . . . . . . . . . 11 (a_|_ ^ b) C a
29		coman2 178	. . . . . . . . . . 11 (a_|_ ^ b) C b
30	28, 29	com2or 465	. . . . . . . . . 10 (a_|_ ^ b) C (a v b)
31	29	comcom2 175	. . . . . . . . . . 11 (a_|_ ^ b) C b_|_
32	28, 31	com2or 465	. . . . . . . . . 10 (a_|_ ^ b) C (a v b_|_)
33	30, 32	com2an 466	. . . . . . . . 9 (a_|_ ^ b) C ((a v b) ^ (a v b_|_))
34	33, 27	fh3 453	. . . . . . . 8 ((a_|_ ^ b) v (((a v b) ^ (a v b_|_)) ^ a_|_)) = (((a_|_ ^ b) v ((a v b) ^ (a v b_|_))) ^ ((a_|_ ^ b) v a_|_))
35		comor1 443	. . . . . . . . . . . . . 14 (a v b) C a
36	35	comcom2 175	. . . . . . . . . . . . 13 (a v b) C a_|_
37		comor2 444	. . . . . . . . . . . . 13 (a v b) C b
38	36, 37	com2an 466	. . . . . . . . . . . 12 (a v b) C (a_|_ ^ b)
39	37	comcom2 175	. . . . . . . . . . . . 13 (a v b) C b_|_
40	35, 39	com2or 465	. . . . . . . . . . . 12 (a v b) C (a v b_|_)
41	38, 40	fh4 454	. . . . . . . . . . 11 ((a_|_ ^ b) v ((a v b) ^ (a v b_|_))) = (((a_|_ ^ b) v (a v b)) ^ ((a_|_ ^ b) v (a v b_|_)))
42	36, 37	fh3r 457	. . . . . . . . . . . . . 14 ((a_|_ ^ b) v (a v b)) = ((a_|_ v (a v b)) ^ (b v (a v b)))
43		ax-a2 30	. . . . . . . . . . . . . . . 16 (a_|_ v (a v b)) = ((a v b) v a_|_)
44		or12 73	. . . . . . . . . . . . . . . . 17 (b v (a v b)) = (a v (b v b))
45		oridm 102	. . . . . . . . . . . . . . . . . 18 (b v b) = b
46	45	lor 66	. . . . . . . . . . . . . . . . 17 (a v (b v b)) = (a v b)
47	44, 46	ax-r2 35	. . . . . . . . . . . . . . . 16 (b v (a v b)) = (a v b)
48	43, 47	2an 72	. . . . . . . . . . . . . . 15 ((a_|_ v (a v b)) ^ (b v (a v b))) = (((a v b) v a_|_) ^ (a v b))
49		ancom 68	. . . . . . . . . . . . . . . 16 (((a v b) v a_|_) ^ (a v b)) = ((a v b) ^ ((a v b) v a_|_))
50		a5c 113	. . . . . . . . . . . . . . . 16 ((a v b) ^ ((a v b) v a_|_)) = (a v b)
51	49, 50	ax-r2 35	. . . . . . . . . . . . . . 15 (((a v b) v a_|_) ^ (a v b)) = (a v b)
52	48, 51	ax-r2 35	. . . . . . . . . . . . . 14 ((a_|_ v (a v b)) ^ (b v (a v b))) = (a v b)
53	42, 52	ax-r2 35	. . . . . . . . . . . . 13 ((a_|_ ^ b) v (a v b)) = (a v b)
54		anor2 81	. . . . . . . . . . . . . . . . 17 (a_|_ ^ b) = (a v b_|_)_|_
55	54	ax-r1 34	. . . . . . . . . . . . . . . 16 (a v b_|_)_|_ = (a_|_ ^ b)
56	55	con3 65	. . . . . . . . . . . . . . 15 (a v b_|_) = (a_|_ ^ b)_|_
57	56	lor 66	. . . . . . . . . . . . . 14 ((a_|_ ^ b) v (a v b_|_)) = ((a_|_ ^ b) v (a_|_ ^ b)_|_)
58		df-t 40	. . . . . . . . . . . . . . 15 1 = ((a_|_ ^ b) v (a_|_ ^ b)_|_)
59	58	ax-r1 34	. . . . . . . . . . . . . 14 ((a_|_ ^ b) v (a_|_ ^ b)_|_) = 1
60	57, 59	ax-r2 35	. . . . . . . . . . . . 13 ((a_|_ ^ b) v (a v b_|_)) = 1
61	53, 60	2an 72	. . . . . . . . . . . 12 (((a_|_ ^ b) v (a v b)) ^ ((a_|_ ^ b) v (a v b_|_))) = ((a v b) ^ 1)
62		an1 98	. . . . . . . . . . . 12 ((a v b) ^ 1) = (a v b)
63	61, 62	ax-r2 35	. . . . . . . . . . 11 (((a_|_ ^ b) v (a v b)) ^ ((a_|_ ^ b) v (a v b_|_))) = (a v b)
64	41, 63	ax-r2 35	. . . . . . . . . 10 ((a_|_ ^ b) v ((a v b) ^ (a v b_|_))) = (a v b)
65		ax-a2 30	. . . . . . . . . . 11 ((a_|_ ^ b) v a_|_) = (a_|_ v (a_|_ ^ b))
66		a5b 112	. . . . . . . . . . 11 (a_|_ v (a_|_ ^ b)) = a_|_
67	65, 66	ax-r2 35	. . . . . . . . . 10 ((a_|_ ^ b) v a_|_) = a_|_
68	64, 67	2an 72	. . . . . . . . 9 (((a_|_ ^ b) v ((a v b) ^ (a v b_|_))) ^ ((a_|_ ^ b) v a_|_)) = ((a v b) ^ a_|_)
69		ancom 68	. . . . . . . . 9 ((a v b) ^ a_|_) = (a_|_ ^ (a v b))
70	68, 69	ax-r2 35	. . . . . . . 8 (((a_|_ ^ b) v ((a v b) ^ (a v b_|_))) ^ ((a_|_ ^ b) v a_|_)) = (a_|_ ^ (a v b))
71	34, 70	ax-r2 35	. . . . . . 7 ((a_|_ ^ b) v (((a v b) ^ (a v b_|_)) ^ a_|_)) = (a_|_ ^ (a v b))
72	26, 71	2or 67	. . . . . 6 (((a ^ b) v (a ^ (a_|_ v b_|_))) v ((a_|_ ^ b) v (((a v b) ^ (a v b_|_)) ^ a_|_))) = (a v (a_|_ ^ (a v b)))
73		oml 427	. . . . . 6 (a v (a_|_ ^ (a v b))) = (a v b)
74	72, 73	ax-r2 35	. . . . 5 (((a ^ b) v (a ^ (a_|_ v b_|_))) v ((a_|_ ^ b) v (((a v b) ^ (a v b_|_)) ^ a