Theorem u4lem5 746

Description: Lemma for unified implication study.

Assertion

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

Proof of Theorem u4lem5

Step	Hyp	Ref	Expression
1		df-i4 46	. 2 (a ->4 (a ->4 b)) = (((a ^ (a ->4 b)) v (a_|_ ^ (a ->4 b))) v ((a_|_ v (a ->4 b)) ^ (a ->4 b)_|_))
2		ancom 68	. . . . . . 7 (a ^ (a ->4 b)) = ((a ->4 b) ^ a)
3		u4lemaa 585	. . . . . . 7 ((a ->4 b) ^ a) = (a ^ b)
4	2, 3	ax-r2 35	. . . . . 6 (a ^ (a ->4 b)) = (a ^ b)
5		ancom 68	. . . . . . 7 (a_|_ ^ (a ->4 b)) = ((a ->4 b) ^ a_|_)
6		u4lemana 590	. . . . . . 7 ((a ->4 b) ^ a_|_) = ((a_|_ ^ b) v (a_|_ ^ b_|_))
7	5, 6	ax-r2 35	. . . . . 6 (a_|_ ^ (a ->4 b)) = ((a_|_ ^ b) v (a_|_ ^ b_|_))
8	4, 7	2or 67	. . . . 5 ((a ^ (a ->4 b)) v (a_|_ ^ (a ->4 b))) = ((a ^ b) v ((a_|_ ^ b) v (a_|_ ^ b_|_)))
9		ax-a3 31	. . . . . 6 (((a ^ b) v (a_|_ ^ b)) v (a_|_ ^ b_|_)) = ((a ^ b) v ((a_|_ ^ b) v (a_|_ ^ b_|_)))
10	9	ax-r1 34	. . . . 5 ((a ^ b) v ((a_|_ ^ b) v (a_|_ ^ b_|_))) = (((a ^ b) v (a_|_ ^ b)) v (a_|_ ^ b_|_))
11	8, 10	ax-r2 35	. . . 4 ((a ^ (a ->4 b)) v (a_|_ ^ (a ->4 b))) = (((a ^ b) v (a_|_ ^ b)) v (a_|_ ^ b_|_))
12		ax-a2 30	. . . . . . 7 (a_|_ v (a ->4 b)) = ((a ->4 b) v a_|_)
13		u4lemona 610	. . . . . . 7 ((a ->4 b) v a_|_) = (a_|_ v b)
14	12, 13	ax-r2 35	. . . . . 6 (a_|_ v (a ->4 b)) = (a_|_ v b)
15		ud4lem0c 272	. . . . . 6 (a ->4 b)_|_ = (((a_|_ v b_|_) ^ (a v b_|_)) ^ ((a ^ b_|_) v b))
16	14, 15	2an 72	. . . . 5 ((a_|_ v (a ->4 b)) ^ (a ->4 b)_|_) = ((a_|_ v b) ^ (((a_|_ v b_|_) ^ (a v b_|_)) ^ ((a ^ b_|_) v b)))
17		ancom 68	. . . . . 6 ((a_|_ v b) ^ (((a_|_ v b_|_) ^ (a v b_|_)) ^ ((a ^ b_|_) v b))) = ((((a_|_ v b_|_) ^ (a v b_|_)) ^ ((a ^ b_|_) v b)) ^ (a_|_ v b))
18		anass 69	. . . . . . 7 ((((a_|_ v b_|_) ^ (a v b_|_)) ^ ((a ^ b_|_) v b)) ^ (a_|_ v b)) = (((a_|_ v b_|_) ^ (a v b_|_)) ^ (((a ^ b_|_) v b) ^ (a_|_ v b)))
19		comor1 443	. . . . . . . . . . . . 13 (a_|_ v b) C a_|_
20	19	comcom7 442	. . . . . . . . . . . 12 (a_|_ v b) C a
21		comor2 444	. . . . . . . . . . . . 13 (a_|_ v b) C b
22	21	comcom2 175	. . . . . . . . . . . 12 (a_|_ v b) C b_|_
23	20, 22	com2an 466	. . . . . . . . . . 11 (a_|_ v b) C (a ^ b_|_)
24	23, 21	fh1r 455	. . . . . . . . . 10 (((a ^ b_|_) v b) ^ (a_|_ v b)) = (((a ^ b_|_) ^ (a_|_ v b)) v (b ^ (a_|_ v b)))
25		ax-a2 30	. . . . . . . . . . 11 (((a ^ b_|_) ^ (a_|_ v b)) v (b ^ (a_|_ v b))) = ((b ^ (a_|_ v b)) v ((a ^ b_|_) ^ (a_|_ v b)))
26		leor 151	. . . . . . . . . . . . . 14 b =< (a_|_ v b)
27	26	df2le2 128	. . . . . . . . . . . . 13 (b ^ (a_|_ v b)) = b
28		oran2 84	. . . . . . . . . . . . . . 15 (a_|_ v b) = (a ^ b_|_)_|_
29	28	lan 70	. . . . . . . . . . . . . 14 ((a ^ b_|_) ^ (a_|_ v b)) = ((a ^ b_|_) ^ (a ^ b_|_)_|_)
30		dff 93	. . . . . . . . . . . . . . 15 0 = ((a ^ b_|_) ^ (a ^ b_|_)_|_)
31	30	ax-r1 34	. . . . . . . . . . . . . 14 ((a ^ b_|_) ^ (a ^ b_|_)_|_) = 0
32	29, 31	ax-r2 35	. . . . . . . . . . . . 13 ((a ^ b_|_) ^ (a_|_ v b)) = 0
33	27, 32	2or 67	. . . . . . . . . . . 12 ((b ^ (a_|_ v b)) v ((a ^ b_|_) ^ (a_|_ v b))) = (b v 0)
34		or0 94	. . . . . . . . . . . 12 (b v 0) = b
35	33, 34	ax-r2 35	. . . . . . . . . . 11 ((b ^ (a_|_ v b)) v ((a ^ b_|_) ^ (a_|_ v b))) = b
36	25, 35	ax-r2 35	. . . . . . . . . 10 (((a ^ b_|_) ^ (a_|_ v b)) v (b ^ (a_|_ v b))) = b
37	24, 36	ax-r2 35	. . . . . . . . 9 (((a ^ b_|_) v b) ^ (a_|_ v b)) = b
38	37	lan 70	. . . . . . . 8 (((a_|_ v b_|_) ^ (a v b_|_)) ^ (((a ^ b_|_) v b) ^ (a_|_ v b))) = (((a_|_ v b_|_) ^ (a v b_|_)) ^ b)
39		ancom 68	. . . . . . . 8 (((a_|_ v b_|_) ^ (a v b_|_)) ^ b) = (b ^ ((a_|_ v b_|_) ^ (a v b_|_)))
40	38, 39	ax-r2 35	. . . . . . 7 (((a_|_ v b_|_) ^ (a v b_|_)) ^ (((a ^ b_|_) v b) ^ (a_|_ v b))) = (b ^ ((a_|_ v b_|_) ^ (a v b_|_)))
41	18, 40	ax-r2 35	. . . . . 6 ((((a_|_ v b_|_) ^ (a v b_|_)) ^ ((a ^ b_|_) v b)) ^ (a_|_ v b)) = (b ^ ((a_|_ v b_|_) ^ (a v b_|_)))
42	17, 41	ax-r2 35	. . . . 5 ((a_|_ v b) ^ (((a_|_ v b_|_) ^ (a v b_|_)) ^ ((a ^ b_|_) v b))) = (b ^ ((a_|_ v b_|_) ^ (a v b_|_)))
43	16, 42	ax-r2 35	. . . 4 ((a_|_ v (a ->4 b)) ^ (a ->4 b)_|_) = (b ^ ((a_|_ v b_|_) ^ (a v b_|_)))
44	11, 43	2or 67	. . 3 (((a ^ (a ->4 b)) v (a_|_ ^ (a ->4 b))) v ((a_|_ v (a ->4 b)) ^ (a ->4 b)_|_)) = ((((a ^ b) v (a_|_ ^ b)) v (a_|_ ^ b_|_)) v (b ^ ((a_|_ v b_|_) ^ (a v b_|_))))
45		comanr2 447	. . . . . . 7 b C (a ^ b)
46		comanr2 447	. . . . . . 7 b C (a_|_ ^ b)
47	45, 46	com2or 465	. . . . . 6 b C ((a ^ b) v (a_|_ ^ b))
48		comanr2 447	. . . . . . 7 b_|_ C (a_|_ ^ b_|_)
49	48	comcom6 441	. . . . . 6 b C (a_|_ ^ b_|_)
50	47, 49	com2or 465	. . . . 5 b C (((a ^ b) v (a_|_ ^ b)) v (a_|_ ^ b_|_))
51		comorr2 445	. . . . . . 7 b_|_ C (a_|_ v b_|_)
52		comorr2 445	. . . . . . 7 b_|_ C (a v b_|_)
53	51, 52	com2an 466	. . . . . 6 b_|_ C ((a_|_ v b_|_) ^ (a v b_|_))
54	53	comcom6 441	. . . . 5 b C ((a_|_ v b_|_) ^ (a v b_|_))
55	50, 54	fh4 454	. . . 4 ((((a ^ b) v (a_|_ ^ b)) v (a_|_ ^ b_|_)) v (b ^ ((a_|_ v b_|_) ^ (a v b_|_)))) = (((((a ^ b) v (a_|_ ^ b)) v (a_|_ ^ b_|_)) v b) ^ ((((a ^ b) v (a_|_ ^ b)) v (a_|_ ^ b_|_)) v ((a_|_ v b_|_) ^ (a v b_|_))))
56		or32 75	. . . . . . 7 ((((a ^ b) v (a_|_ ^ b)) v (a_|_ ^ b_|_)) v b) = ((((a ^ b) v (a_|_ ^ b)) v b) v (a_|_ ^ b_|_))
57		lear 153	. . . . . . . . . 10 (a ^ b) =< b
58		lear 153	. . . . . . . . . 10 (a_|_ ^ b) =< b
59	57, 58	lel2or 162	. . . . . . . . 9 ((a ^ b) v (a_|_ ^ b)) =< b
60	59	df-le2 123	. . . . . . . 8 (((a ^ b) v (a_|_ ^ b)) v b) = b
61	60	ax-r5 37	. . . . . . 7 ((((a ^ b) v (a_|_ ^ b)) v b) v (a_|_ ^ b_|_)) = (b v (a_|_ ^ b_|_))
62	56, 61	ax-r2 35	. . . . . 6 ((((a ^ b) v (a_|_ ^ b)) v (a_|_ ^ b_|_)) v b) = (b v (a_|_ ^ b_|_))
63		comor1 443	. . . . . . . . . . . 12 (a_|_ v b_|_) C a_|_
64	63	comcom7 442	. . . . . . . . . . 11 (a_|_ v b_|_) C a
65		comor2 444	. . . . . . . . . . . 12 (a_|_ v b_|_) C b_|_
66	65	comcom7 442	. . . . . . . . . . 11 (a_|_ v b_|_) C b
67	64, 66	com2an 466	. . . . . . . . . 10 (a_|_ v b_|_) C (a ^ b)
68	63, 66	com2an 466	. . . . . . . . . 10 (a_|_ v b_|_) C (a_|_ ^ b)
69	67, 68	com2or 465	. . . . . . . . 9 (a_|_ v b_|_) C ((a ^ b) v (a_|_ ^ b))
70	63, 65	com2an 466	. . . . . . . . 9 (a_|_ v b_|_) C (a_|_ ^ b_|_)
71	69, 70	com2or 465	. . . . . . . 8 (a_|_ v b_|_) C (((a ^ b) v (a_|_ ^