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 112	. . . . . . . . . 10 (a' v ((a' ^ b) v (a' ^ b'))) = ((a' v (a' ^ b)) v (a' v (a' ^ b')))
61		a5b 120	. . . . . . . . . . . 12 (a' v (a' ^ b)) = a'
62		a5b 120	. . . . . . . . . . . 12 (a' v (a' ^ b')) = a'
63	61, 62	2or 72	. . . . . . . . . . 11 ((a' v (a' ^ b)) v (a' v (a' ^ b'))) = (a' v a')
64	63, 7	ax-r2 36	. . . . . . . . . 10 ((a' v (a' ^ b)) v (a' v (a' ^ b'))) = a'
65	60, 64	ax-r2 36	. . . . . . . . 9 (a' v ((a' ^ b) v (a' ^ b'))) = a'
66	65	ax-r5 38	. . . . . . . 8 ((a' v ((a' ^ b) v (a' ^ b'))) v (a ^ (a' v b))) = (a' v (a ^ (a' v b)))
67	59, 66	ax-r2 36	. . . . . . 7 (a' v (((a' ^ b) v (a' ^ b')) v (a ^ (a' v b)))) = (a' v (a ^ (a' v b)))
68	57, 67	ax-r2 36	. . . . . 6 (a' v (a ->3 b)) = (a' v (a ^ (a' v b)))
69		omln 446	. . . . . 6 (a' v (a ^ (a' v b))) = (a' v b)
70	68, 69	ax-r2 36	. . . . 5 (a' v (a ->3 b)) = (a' v b)
71	70	lan 77	. . . 4 (a ^ (a' v (a ->3 b))) = (a ^ (a' v b))
72	56, 71	2or 72	. . 3 (((a' ^ (a ->3 b)) v (a' ^ (a ->3 b)')) v (a ^ (a' v (a ->3 b)))) = (a' v (a ^ (a' v b)))
73	72, 69	ax-r2 36	. 2 (((a' ^ (a ->3 b)) v (a' ^ (a ->3 b)')) v (a ^ (a' v (a ->3 b)))) = (a' v b)
74	1, 73	ax-r2 36	1 (a ->3 (a ->3 b)) = (a' v b)

Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7  0wf 9   ->3 wi3 14

This theorem is referenced by:  i0i3 512  i3i0 513  ska14 514  i3abs1 522  i3abs3 524  i3th1 543  i3th2 544  i3th3 545  i3th5 547  i3th7 549  i3th8 550  u3lem4 758  u3lem12 788  u3lemax4 796  u3lemax5 797

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-r3 439

This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i3 46  df-le1 130  df-le2 131  df-c1 132  df-c2 133

Copyright terms: Public domain