Theorem lem4 493

Description: Lemma 4 of Kalmbach p. 240.

Assertion

Ref	Expression
lem4	(a ->3 (a ->3 b)) = (a_|_ v b)

Proof of Theorem lem4

Step	Hyp	Ref	Expression
1		df-i3 45	. 2 (a ->3 (a ->3 b)) = (((a_|_ ^ (a ->3 b)) v (a_|_ ^ (a ->3 b)_|_)) v (a ^ (a_|_ v (a ->3 b))))
2		df-i3 45	. . . . . . . 8 (a ->3 b) = (((a_|_ ^ b) v (a_|_ ^ b_|_)) v (a ^ (a_|_ v b)))
3	2	lan 70	. . . . . . 7 (a_|_ ^ (a ->3 b)) = (a_|_ ^ (((a_|_ ^ b) v (a_|_ ^ b_|_)) v (a ^ (a_|_ v b))))
4		lea 152	. . . . . . . . . . . . 13 (a_|_ ^ b) =< a_|_
5		lea 152	. . . . . . . . . . . . 13 (a_|_ ^ b_|_) =< a_|_
6	4, 5	le2or 160	. . . . . . . . . . . 12 ((a_|_ ^ b) v (a_|_ ^ b_|_)) =< (a_|_ v a_|_)
7		oridm 102	. . . . . . . . . . . 12 (a_|_ v a_|_) = a_|_
8	6, 7	lbtr 131	. . . . . . . . . . 11 ((a_|_ ^ b) v (a_|_ ^ b_|_)) =< a_|_
9	8	lecom 172	. . . . . . . . . 10 ((a_|_ ^ b) v (a_|_ ^ b_|_)) C a_|_
10	9	comcom 435	. . . . . . . . 9 a_|_ C ((a_|_ ^ b) v (a_|_ ^ b_|_))
11		lea 152	. . . . . . . . . . . 12 (a ^ (a_|_ v b)) =< a
12	11	lecom 172	. . . . . . . . . . 11 (a ^ (a_|_ v b)) C a
13	12	comcom 435	. . . . . . . . . 10 a C (a ^ (a_|_ v b))
14	13	comcom3 436	. . . . . . . . 9 a_|_ C (a ^ (a_|_ v b))
15	10, 14	fh1 451	. . . . . . . 8 (a_|_ ^ (((a_|_ ^ b) v (a_|_ ^ b_|_)) v (a ^ (a_|_ v b)))) = ((a_|_ ^ ((a_|_ ^ b) v (a_|_ ^ b_|_))) v (a_|_ ^ (a ^ (a_|_ v b))))
16		ancom 68	. . . . . . . . . . 11 ((a_|_ ^ a) ^ (a_|_ v b)) = ((a_|_ v b) ^ (a_|_ ^ a))
17		anass 69	. . . . . . . . . . 11 ((a_|_ ^ a) ^ (a_|_ v b)) = (a_|_ ^ (a ^ (a_|_ v b)))
18		dff 93	. . . . . . . . . . . . . . 15 0 = (a ^ a_|_)
19		ancom 68	. . . . . . . . . . . . . . 15 (a ^ a_|_) = (a_|_ ^ a)
20	18, 19	ax-r2 35	. . . . . . . . . . . . . 14 0 = (a_|_ ^ a)
21	20	lan 70	. . . . . . . . . . . . 13 ((a_|_ v b) ^ 0) = ((a_|_ v b) ^ (a_|_ ^ a))
22	21	ax-r1 34	. . . . . . . . . . . 12 ((a_|_ v b) ^ (a_|_ ^ a)) = ((a_|_ v b) ^ 0)
23		an0 100	. . . . . . . . . . . 12 ((a_|_ v b) ^ 0) = 0
24	22, 23	ax-r2 35	. . . . . . . . . . 11 ((a_|_ v b) ^ (a_|_ ^ a)) = 0
25	16, 17, 24	3tr2 61	. . . . . . . . . 10 (a_|_ ^ (a ^ (a_|_ v b))) = 0
26	25	lor 66	. . . . . . . . 9 ((a_|_ ^ ((a_|_ ^ b) v (a_|_ ^ b_|_))) v (a_|_ ^ (a ^ (a_|_ v b)))) = ((a_|_ ^ ((a_|_ ^ b) v (a_|_ ^ b_|_))) v 0)
27		or0 94	. . . . . . . . . 10 ((a_|_ ^ ((a_|_ ^ b) v (a_|_ ^ b_|_))) v 0) = (a_|_ ^ ((a_|_ ^ b) v (a_|_ ^ b_|_)))
28		ancom 68	. . . . . . . . . . 11 (a_|_ ^ ((a_|_ ^ b) v (a_|_ ^ b_|_))) = (((a_|_ ^ b) v (a_|_ ^ b_|_)) ^ a_|_)
29	8	df2le2 128	. . . . . . . . . . 11 (((a_|_ ^ b) v (a_|_ ^ b_|_)) ^ a_|_) = ((a_|_ ^ b) v (a_|_ ^ b_|_))
30	28, 29	ax-r2 35	. . . . . . . . . 10 (a_|_ ^ ((a_|_ ^ b) v (a_|_ ^ b_|_))) = ((a_|_ ^ b) v (a_|_ ^ b_|_))
31	27, 30	ax-r2 35	. . . . . . . . 9 ((a_|_ ^ ((a_|_ ^ b) v (a_|_ ^ b_|_))) v 0) = ((a_|_ ^ b) v (a_|_ ^ b_|_))
32	26, 31	ax-r2 35	. . . . . . . 8 ((a_|_ ^ ((a_|_ ^ b) v (a_|_ ^ b_|_))) v (a_|_ ^ (a ^ (a_|_ v b)))) = ((a_|_ ^ b) v (a_|_ ^ b_|_))
33	15, 32	ax-r2 35	. . . . . . 7 (a_|_ ^ (((a_|_ ^ b) v (a_|_ ^ b_|_)) v (a ^ (a_|_ v b)))) = ((a_|_ ^ b) v (a_|_ ^ b_|_))
34	3, 33	ax-r2 35	. . . . . 6 (a_|_ ^ (a ->3 b)) = ((a_|_ ^ b) v (a_|_ ^ b_|_))
35	2	lor 66	. . . . . . . . 9 (a v (a ->3 b)) = (a v (((a_|_ ^ b) v (a_|_ ^ b_|_)) v (a ^ (a_|_ v b))))
36		orordi 104	. . . . . . . . . 10 (a v (((a_|_ ^ b) v (a_|_ ^ b_|_)) v (a ^ (a_|_ v b)))) = ((a v ((a_|_ ^ b) v (a_|_ ^ b_|_))) v (a v (a ^ (a_|_ v b))))
37		a5b 112	. . . . . . . . . . . 12 (a v (a ^ (a_|_ v b))) = a
38	37	lor 66	. . . . . . . . . . 11 ((a v ((a_|_ ^ b) v (a_|_ ^ b_|_))) v (a v (a ^ (a_|_ v b)))) = ((a v ((a_|_ ^ b) v (a_|_ ^ b_|_))) v a)
39		or32 75	. . . . . . . . . . . 12 ((a v ((a_|_ ^ b) v (a_|_ ^ b_|_))) v a) = ((a v a) v ((a_|_ ^ b) v (a_|_ ^ b_|_)))
40		oridm 102	. . . . . . . . . . . . 13 (a v a) = a
41	40	ax-r5 37	. . . . . . . . . . . 12 ((a v a) v ((a_|_ ^ b) v (a_|_ ^ b_|_))) = (a v ((a_|_ ^ b) v (a_|_ ^ b_|_)))
42	39, 41	ax-r2 35	. . . . . . . . . . 11 ((a v ((a_|_ ^ b) v (a_|_ ^ b_|_))) v a) = (a v ((a_|_ ^ b) v (a_|_ ^ b_|_)))
43	38, 42	ax-r2 35	. . . . . . . . . 10 ((a v ((a_|_ ^ b) v (a_|_ ^ b_|_))) v (a v (a ^ (a_|_ v b)))) = (a v ((a_|_ ^ b) v (a_|_ ^ b_|_)))
44	36, 43	ax-r2 35	. . . . . . . . 9 (a v (((a_|_ ^ b) v (a_|_ ^ b_|_)) v (a ^ (a_|_ v b)))) = (a v ((a_|_ ^ b) v (a_|_ ^ b_|_)))
45	35, 44	ax-r2 35	. . . . . . . 8 (a v (a ->3 b)) = (a v ((a_|_ ^ b) v (a_|_ ^ b_|_)))
46	45	ax-r4 36	. . . . . . 7 (a v (a ->3 b))_|_ = (a v ((a_|_ ^ b) v (a_|_ ^ b_|_)))_|_
47		oran 79	. . . . . . . 8 (a v (a ->3 b)) = (a_|_ ^ (a ->3 b)_|_)_|_
48	47	con2 64	. . . . . . 7 (a v (a ->3 b))_|_ = (a_|_ ^ (a ->3 b)_|_)
49		oran 79	. . . . . . . . 9 (a v ((a_|_ ^ b) v (a_|_ ^ b_|_))) = (a_|_ ^ ((a_|_ ^ b) v (a_|_ ^ b_|_))_|_)_|_
50	49	con2 64	. . . . . . . 8 (a v ((a_|_ ^ b) v (a_|_ ^ b_|_)))_|_ = (a_|_ ^ ((a_|_ ^ b) v (a_|_ ^ b_|_))_|_)
51		ancom 68	. . . . . . . 8 (a_|_ ^ ((a_|_ ^ b) v (a_|_ ^ b_|_))_|_) = (((a_|_ ^ b) v (a_|_ ^ b_|_))_|_ ^ a_|_)
52	50, 51	ax-r2 35	. . . . . . 7 (a v ((a_|_ ^ b) v (a_|_ ^ b_|_)))_|_ = (((a_|_ ^ b) v (a_|_ ^ b_|_))_|_ ^ a_|_)
53	46, 48, 52	3tr2 61	. . . . . 6 (a_|_ ^ (a ->3 b)_|_) = (((a_|_ ^ b) v (a_|_ ^ b_|_))_|_ ^ a_|_)
54	34, 53	2or 67	. . . . 5 ((a_|_ ^ (a ->3 b)) v (a_|_ ^ (a ->3 b)_|_)) = (((a_|_ ^ b) v (a_|_ ^ b_|_)) v (((a_|_ ^ b) v (a_|_ ^ b_|_))_|_ ^ a_|_))
55	8	oml2 433	. . . . 5 (((a_|_ ^ b) v (a_|_ ^ b_|_)) v (((a_|_ ^ b) v (a_|_ ^ b_|_))_|_ ^ a_|_)) = a_|_
56	54, 55	ax-r2 35	. . . 4 ((a_|_ ^ (a ->3 b)) v (a_|_ ^ (a ->3 b)_|_)) = a_|_
57	2	lor 66	. . . . . . 7 (a_|_ v (a ->3 b)) = (a_|_ v (((a_|_ ^ b) v (a_|_ ^ b_|_)) v (a ^ (a_|_ v b))))
58		ax-a3 31	. . . . . . . . 9 ((a_|_ v ((a_|_ ^ b) v (a_|_ ^ b_|_))) v (a ^ (a_|_ v b))) = (a_|_ v (((a_|_ ^ b) v (a_|_ ^ b_|_)) v (a ^ (a_|_ v b))))
59	58	ax-r1 34	. . . . . . . 8 (a_|_ v (((a_|_ ^ b) v (a_|_ ^ b_|_)) v (a ^ (a_|_ v b)))) = ((a_|_ v ((a_|_ ^ b) v (a_|_ ^ b_|_))) v (a ^ (a_|_ v b)))
60		orordi 104	. . . . . . . . . 10 (a_|_ v ((a_|_ ^ b) v (a_|_ ^ b_|_))) = ((a_|_ v (a