Theorem lem4 511

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 46	. 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 46	. . . . . . . 8 (a ->3 b) = (((a' ^ b) v (a' ^ b')) v (a ^ (a' v b)))
3	2	lan 77	. . . . . . 7 (a' ^ (a ->3 b)) = (a' ^ (((a' ^ b) v (a' ^ b')) v (a ^ (a' v b))))
4		lea 160	. . . . . . . . . . . . 13 (a' ^ b) =< a'
5		lea 160	. . . . . . . . . . . . 13 (a' ^ b') =< a'
6	4, 5	le2or 168	. . . . . . . . . . . 12 ((a' ^ b) v (a' ^ b')) =< (a' v a')
7		oridm 110	. . . . . . . . . . . 12 (a' v a') = a'
8	6, 7	lbtr 139	. . . . . . . . . . 11 ((a' ^ b) v (a' ^ b')) =< a'
9	8	lecom 180	. . . . . . . . . 10 ((a' ^ b) v (a' ^ b')) C a'
10	9	comcom 453	. . . . . . . . 9 a' C ((a' ^ b) v (a' ^ b'))
11		lea 160	. . . . . . . . . . . 12 (a ^ (a' v b)) =< a
12	11	lecom 180	. . . . . . . . . . 11 (a ^ (a' v b)) C a
13	12	comcom 453	. . . . . . . . . 10 a C (a ^ (a' v b))
14	13	comcom3 454	. . . . . . . . 9 a' C (a ^ (a' v b))
15	10, 14	fh1 469	. . . . . . . 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 74	. . . . . . . . . . 11 ((a' ^ a) ^ (a' v b)) = ((a' v b) ^ (a' ^ a))
17		anass 76	. . . . . . . . . . 11 ((a' ^ a) ^ (a' v b)) = (a' ^ (a ^ (a' v b)))
18		dff 101	. . . . . . . . . . . . . . 15 0 = (a ^ a')
19		ancom 74	. . . . . . . . . . . . . . 15 (a ^ a') = (a' ^ a)
20	18, 19	ax-r2 36	. . . . . . . . . . . . . 14 0 = (a' ^ a)
21	20	lan 77	. . . . . . . . . . . . 13 ((a' v b) ^ 0) = ((a' v b) ^ (a' ^ a))
22	21	ax-r1 35	. . . . . . . . . . . 12 ((a' v b) ^ (a' ^ a)) = ((a' v b) ^ 0)
23		an0 108	. . . . . . . . . . . 12 ((a' v b) ^ 0) = 0
24	22, 23	ax-r2 36	. . . . . . . . . . 11 ((a' v b) ^ (a' ^ a)) = 0
25	16, 17, 24	3tr2 64	. . . . . . . . . 10 (a' ^ (a ^ (a' v b))) = 0
26	25	lor 70	. . . . . . . . 9 ((a' ^ ((a' ^ b) v (a' ^ b'))) v (a' ^ (a ^ (a' v b)))) = ((a' ^ ((a' ^ b) v (a' ^ b'))) v 0)
27		or0 102	. . . . . . . . . 10 ((a' ^ ((a' ^ b) v (a' ^ b'))) v 0) = (a' ^ ((a' ^ b) v (a' ^ b')))
28		ancom 74	. . . . . . . . . . 11 (a' ^ ((a' ^ b) v (a' ^ b'))) = (((a' ^ b) v (a' ^ b')) ^ a')
29	8	df2le2 136	. . . . . . . . . . 11 (((a' ^ b) v (a' ^ b')) ^ a') = ((a' ^ b) v (a' ^ b'))
30	28, 29	ax-r2 36	. . . . . . . . . 10 (a' ^ ((a' ^ b) v (a' ^ b'))) = ((a' ^ b) v (a' ^ b'))
31	27, 30	ax-r2 36	. . . . . . . . 9 ((a' ^ ((a' ^ b) v (a' ^ b'))) v 0) = ((a' ^ b) v (a' ^ b'))
32	26, 31	ax-r2 36	. . . . . . . 8 ((a' ^ ((a' ^ b) v (a' ^ b'))) v (a' ^ (a ^ (a' v b)))) = ((a' ^ b) v (a' ^ b'))
33	15, 32	ax-r2 36	. . . . . . 7 (a' ^ (((a' ^ b) v (a' ^ b')) v (a ^ (a' v b)))) = ((a' ^ b) v (a' ^ b'))
34	3, 33	ax-r2 36	. . . . . 6 (a' ^ (a ->3 b)) = ((a' ^ b) v (a' ^ b'))
35	2	lor 70	. . . . . . . . 9 (a v (a ->3 b)) = (a v (((a' ^ b) v (a' ^ b')) v (a ^ (a' v b))))
36		orordi 112	. . . . . . . . . 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 120	. . . . . . . . . . . 12 (a v (a ^ (a' v b))) = a
38	37	lor 70	. . . . . . . . . . 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 82	. . . . . . . . . . . 12 ((a v ((a' ^ b) v (a' ^ b'))) v a) = ((a v a) v ((a' ^ b) v (a' ^ b')))
40		oridm 110	. . . . . . . . . . . . 13 (a v a) = a
41	40	ax-r5 38	. . . . . . . . . . . 12 ((a v a) v ((a' ^ b) v (a' ^ b'))) = (a v ((a' ^ b) v (a' ^ b')))
42	39, 41	ax-r2 36	. . . . . . . . . . 11 ((a v ((a' ^ b) v (a' ^ b'))) v a) = (a v ((a' ^ b) v (a' ^ b')))
43	38, 42	ax-r2 36	. . . . . . . . . 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 36	. . . . . . . . 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 36	. . . . . . . 8 (a v (a ->3 b)) = (a v ((a' ^ b) v (a' ^ b')))
46	45	ax-r4 37	. . . . . . 7 (a v (a ->3 b))' = (a v ((a' ^ b) v (a' ^ b')))'
47		oran 87	. . . . . . . 8 (a v (a ->3 b)) = (a' ^ (a ->3 b)')'
48	47	con2 67	. . . . . . 7 (a v (a ->3 b))' = (a' ^ (a ->3 b)')
49		oran 87	. . . . . . . . 9 (a v ((a' ^ b) v (a' ^ b'))) = (a' ^ ((a' ^ b) v (a' ^ b'))')'
50	49	con2 67	. . . . . . . 8 (a v ((a' ^ b) v (a' ^ b')))' = (a' ^ ((a' ^ b) v (a' ^ b'))')
51		ancom 74	. . . . . . . 8 (a' ^ ((a' ^ b) v (a' ^ b'))') = (((a' ^ b) v (a' ^ b'))' ^ a')
52	50, 51	ax-r2 36	. . . . . . 7 (a v ((a' ^ b) v (a' ^ b')))' = (((a' ^ b) v (a' ^ b'))' ^ a')
53	46, 48, 52	3tr2 64	. . . . . 6 (a' ^ (a ->3 b)') = (((a' ^ b) v (a' ^ b'))' ^ a')
54	34, 53	2or 72	. . . . 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 451	. . . . 5 (((a' ^ b) v (a' ^ b')) v (((a' ^ b) v (a' ^ b'))' ^ a')) = a'
56	54, 55	ax-r2 36	. . . 4 ((a' ^ (a ->3 b)) v (a' ^ (a ->3 b)')) = a'
57	2	lor 70	. . . . . . 7 (a' v (a ->3 b)) = (a' v (((a' ^ b) v (a' ^ b')) v (a ^ (a' v b))))
58		ax-a3 32	. . . . . . . . 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 35	. . . . . . . 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&