Theorem ud4lem1 563

Description: Lemma for unified disjunction.

Assertion

Ref	Expression
ud4lem1	((a ->4 b) ->4 (b ->4 a)) = (a v (a_|_ ^ b_|_))

Proof of Theorem ud4lem1

Step	Hyp	Ref	Expression
1		df-i4 46	. 2 ((a ->4 b) ->4 (b ->4 a)) = ((((a ->4 b) ^ (b ->4 a)) v ((a ->4 b)_|_ ^ (b ->4 a))) v (((a ->4 b)_|_ v (b ->4 a)) ^ (b ->4 a)_|_))
2		ud4lem1a 559	. . . . 5 ((a ->4 b) ^ (b ->4 a)) = ((a ^ b) v (a_|_ ^ b_|_))
3		ud4lem1b 560	. . . . 5 ((a ->4 b)_|_ ^ (b ->4 a)) = (a ^ b_|_)
4	2, 3	2or 67	. . . 4 (((a ->4 b) ^ (b ->4 a)) v ((a ->4 b)_|_ ^ (b ->4 a))) = (((a ^ b) v (a_|_ ^ b_|_)) v (a ^ b_|_))
5		ud4lem1d 562	. . . 4 (((a ->4 b)_|_ v (b ->4 a)) ^ (b ->4 a)_|_) = (((a_|_ v b_|_) ^ (a_|_ v b)) ^ a)
6	4, 5	2or 67	. . 3 ((((a ->4 b) ^ (b ->4 a)) v ((a ->4 b)_|_ ^ (b ->4 a))) v (((a ->4 b)_|_ v (b ->4 a)) ^ (b ->4 a)_|_)) = ((((a ^ b) v (a_|_ ^ b_|_)) v (a ^ b_|_)) v (((a_|_ v b_|_) ^ (a_|_ v b)) ^ a))
7		ancom 68	. . . . . 6 (((a_|_ v b_|_) ^ (a_|_ v b)) ^ a) = (a ^ ((a_|_ v b_|_) ^ (a_|_ v b)))
8	7	lor 66	. . . . 5 ((((a ^ b) v (a_|_ ^ b_|_)) v (a ^ b_|_)) v (((a_|_ v b_|_) ^ (a_|_ v b)) ^ a)) = ((((a ^ b) v (a_|_ ^ b_|_)) v (a ^ b_|_)) v (a ^ ((a_|_ v b_|_) ^ (a_|_ v b))))
9		coman1 177	. . . . . . . . . . . 12 (a ^ b) C a
10	9	comcom 435	. . . . . . . . . . 11 a C (a ^ b)
11	10	comcom3 436	. . . . . . . . . 10 a_|_ C (a ^ b)
12		coman1 177	. . . . . . . . . . 11 (a_|_ ^ b_|_) C a_|_
13	12	comcom 435	. . . . . . . . . 10 a_|_ C (a_|_ ^ b_|_)
14	11, 13	com2or 465	. . . . . . . . 9 a_|_ C ((a ^ b) v (a_|_ ^ b_|_))
15		coman1 177	. . . . . . . . . . 11 (a ^ b_|_) C a
16	15	comcom 435	. . . . . . . . . 10 a C (a ^ b_|_)
17	16	comcom3 436	. . . . . . . . 9 a_|_ C (a ^ b_|_)
18	14, 17	com2or 465	. . . . . . . 8 a_|_ C (((a ^ b) v (a_|_ ^ b_|_)) v (a ^ b_|_))
19	18	comcom2 175	. . . . . . 7 a_|_ C (((a ^ b) v (a_|_ ^ b_|_)) v (a ^ b_|_))_|_
20	19	comcom5 440	. . . . . 6 a C (((a ^ b) v (a_|_ ^ b_|_)) v (a ^ b_|_))
21		comorr 176	. . . . . . . . 9 a_|_ C (a_|_ v b_|_)
22		comorr 176	. . . . . . . . 9 a_|_ C (a_|_ v b)
23	21, 22	com2an 466	. . . . . . . 8 a_|_ C ((a_|_ v b_|_) ^ (a_|_ v b))
24	23	comcom2 175	. . . . . . 7 a_|_ C ((a_|_ v b_|_) ^ (a_|_ v b))_|_
25	24	comcom5 440	. . . . . 6 a C ((a_|_ v b_|_) ^ (a_|_ v b))
26	20, 25	fh4 454	. . . . 5 ((((a ^ b) v (a_|_ ^ b_|_)) v (a ^ b_|_)) v (a ^ ((a_|_ v b_|_) ^ (a_|_ v b)))) = (((((a ^ b) v (a_|_ ^ b_|_)) v (a ^ b_|_)) v a) ^ ((((a ^ b) v (a_|_ ^ b_|_)) v (a ^ b_|_)) v ((a_|_ v b_|_) ^ (a_|_ v b))))
27	8, 26	ax-r2 35	. . . 4 ((((a ^ b) v (a_|_ ^ b_|_)) v (a ^ b_|_)) v (((a_|_ v b_|_) ^ (a_|_ v b)) ^ a)) = (((((a ^ b) v (a_|_ ^ b_|_)) v (a ^ b_|_)) v a) ^ ((((a ^ b) v (a_|_ ^ b_|_)) v (a ^ b_|_)) v ((a_|_ v b_|_) ^ (a_|_ v b))))
28		ax-a3 31	. . . . . . . 8 ((((a ^ b) v (a_|_ ^ b_|_)) v (a ^ b_|_)) v a) = (((a ^ b) v (a_|_ ^ b_|_)) v ((a ^ b_|_) v a))
29		or4 77	. . . . . . . . 9 (((a ^ b) v (a_|_ ^ b_|_)) v ((a ^ b_|_) v a)) = (((a ^ b) v (a ^ b_|_)) v ((a_|_ ^ b_|_) v a))
30		lea 152	. . . . . . . . . . . 12 (a ^ b) =< a
31		lea 152	. . . . . . . . . . . 12 (a ^ b_|_) =< a
32	30, 31	lel2or 162	. . . . . . . . . . 11 ((a ^ b) v (a ^ b_|_)) =< a
33		leor 151	. . . . . . . . . . 11 a =< ((a_|_ ^ b_|_) v a)
34	32, 33	letr 129	. . . . . . . . . 10 ((a ^ b) v (a ^ b_|_)) =< ((a_|_ ^ b_|_) v a)
35	34	df-le2 123	. . . . . . . . 9 (((a ^ b) v (a ^ b_|_)) v ((a_|_ ^ b_|_) v a)) = ((a_|_ ^ b_|_) v a)
36	29, 35	ax-r2 35	. . . . . . . 8 (((a ^ b) v (a_|_ ^ b_|_)) v ((a ^ b_|_) v a)) = ((a_|_ ^ b_|_) v a)
37	28, 36	ax-r2 35	. . . . . . 7 ((((a ^ b) v (a_|_ ^ b_|_)) v (a ^ b_|_)) v a) = ((a_|_ ^ b_|_) v a)
38		ax-a2 30	. . . . . . 7 ((a_|_ ^ b_|_) v a) = (a v (a_|_ ^ b_|_))
39	37, 38	ax-r2 35	. . . . . 6 ((((a ^ b) v (a_|_ ^ b_|_)) v (a ^ b_|_)) v a) = (a v (a_|_ ^ b_|_))
40	9	comcom2 175	. . . . . . . . . . . . 13 (a ^ b) C a_|_
41		coman2 178	. . . . . . . . . . . . . 14 (a ^ b) C b
42	41	comcom2 175	. . . . . . . . . . . . 13 (a ^ b) C b_|_
43	40, 42	com2or 465	. . . . . . . . . . . 12 (a ^ b) C (a_|_ v b_|_)
44	43	comcom 435	. . . . . . . . . . 11 (a_|_ v b_|_) C (a ^ b)
45		comor1 443	. . . . . . . . . . . 12 (a_|_ v b_|_) C a_|_
46		comor2 444	. . . . . . . . . . . 12 (a_|_ v b_|_) C b_|_
47	45, 46	com2an 466	. . . . . . . . . . 11 (a_|_ v b_|_) C (a_|_ ^ b_|_)
48	44, 47	com2or 465	. . . . . . . . . 10 (a_|_ v b_|_) C ((a ^ b) v (a_|_ ^ b_|_))
49	45	comcom3 436	. . . . . . . . . . . 12 (a_|_ v b_|_)_|_ C a_|_
50	49	comcom5 440	. . . . . . . . . . 11 (a_|_ v b_|_) C a
51	50, 46	com2an 466	. . . . . . . . . 10 (a_|_ v b_|_) C (a ^ b_|_)
52	48, 51	com2or 465	. . . . . . . . 9 (a_|_ v b_|_) C (((a ^ b) v (a_|_ ^ b_|_)) v (a ^ b_|_))
53	46	comcom3 436	. . . . . . . . . . 11 (a_|_ v b_|_)_|_ C b_|_
54	53	comcom5 440	. . . . . . . . . 10 (a_|_ v b_|_) C b
55	45, 54	com2or 465	. . . . . . . . 9 (a_|_ v b_|_) C (a_|_ v b)
56	52, 55	fh4 454	. . . . . . . 8 ((((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)))
57		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_|_))
58		or32 75	. . . . . . . . . . . . 13 (((a ^ b) v (a_|_ ^ b_|_)) v (a_|_ v b_|_)) = (((a ^ b) v (a_|_ v b_|_)) v (a_|_ ^ b_|_))
59		df-a 39	. . . . . . . . . . . . . . . . . . 19 (a ^ b) = (a_|_ v b_|_)_|_
60	59	con2 64	. . . . . . . . . . . . . . . . . 18 (a ^ b)_|_ = (a_|_ v b_|_)
61	60	ax-r1 34	. . . . . . . . . . . . . . . . 17 (a_|_ v b_|_) = (a ^ b)_|_
62	61	lor 66	. . . . . . . . . . . . . . . 16 ((a ^ b) v (a_|_ v b_|_)) = ((a ^ b) v (a ^ b)_|_)
63		df-t 40	. . . . . . . . . . . . . . . . 17 1 = ((a ^ b) v (a ^ b)_|_)
64	63	ax-r1 34	. . . . . . . . . . . . . . . 16 ((a ^ b) v (a ^ b)_|_) = 1
65	62, 64	ax-r2 35	. . . . . . . . . . . . . . 15 ((a ^ b) v (a_|_ v b_|_)) = 1
66	65	ax-r5 37	. . . . . . . . . . . . . 14 (((a ^ b) v (a_|_ v b_|_)) v (a_|_ ^ b_|_)) = (1 v (a_|_ ^ b_|_))
67		ax-a2 30	. . . . . . . . . . . . . . 15 (1 v (a_|_ ^ b_|_)) = ((a_|_ ^ b_|_) v 1)
68		or1 96	. . . . . . . . . . . . . . 15 ((a_|_ ^ b_|_) v 1) = 1
69	67, 68	ax-r2 35	. . . . . . . . . . . . . 14 (1 v (a_|_ ^ b_|_)) = 1
70	66, 69	ax-r2 35	. . . . . . . . . . . . 13 (((a ^ b) v (a_|_ v b_|_)) v (a_|_ ^ b_|_)) = 1
71	58, 70	ax-r2 35	. . . . . . . . . . . 12 (((a ^ b) v (a_|_ ^ b_|_)) v (a_|_ v b_|_)) = 1
72	71	ax-r5 37	. . . . . . . . . . 11 ((((a ^ b) v (a