Theorem u1lem4 757

Description: Lemma for unified implication study. (Contributed by NM, 11-Jan-1998.)

Assertion

Ref	Expression
u1lem4	(a →1 (a →1 (b →1 a))) = (a →1 (b →1 a))

Proof of Theorem u1lem4

Step	Hyp	Ref	Expression
1		df-i1 44	. 2 (a →1 (a →1 (b →1 a))) = (a⊥ ∪ (a ∩ (a →1 (b →1 a))))
2		comid 187	. . . . 5 a C a
3	2	comcom2 183	. . . 4 a C a⊥
4		u1lemc1 680	. . . 4 a C (a →1 (b →1 a))
5	3, 4	fh4 472	. . 3 (a⊥ ∪ (a ∩ (a →1 (b →1 a)))) = ((a⊥ ∪ a) ∩ (a⊥ ∪ (a →1 (b →1 a))))
6		ax-a2 31	. . . . . 6 (a⊥ ∪ a) = (a ∪ a⊥ )
7		df-t 41	. . . . . . 7 1 = (a ∪ a⊥ )
8	7	ax-r1 35	. . . . . 6 (a ∪ a⊥ ) = 1
9	6, 8	ax-r2 36	. . . . 5 (a⊥ ∪ a) = 1
10		ax-a2 31	. . . . . 6 (a⊥ ∪ (a →1 (b →1 a))) = ((a →1 (b →1 a)) ∪ a⊥ )
11		u1lemona 625	. . . . . . 7 ((a →1 (b →1 a)) ∪ a⊥ ) = (a⊥ ∪ (a ∩ (b →1 a)))
12		df-i1 44	. . . . . . . . . . 11 (b →1 a) = (b⊥ ∪ (b ∩ a))
13		ancom 74	. . . . . . . . . . . 12 (b ∩ a) = (a ∩ b)
14	13	lor 70	. . . . . . . . . . 11 (b⊥ ∪ (b ∩ a)) = (b⊥ ∪ (a ∩ b))
15	12, 14	ax-r2 36	. . . . . . . . . 10 (b →1 a) = (b⊥ ∪ (a ∩ b))
16	15	lan 77	. . . . . . . . 9 (a ∩ (b →1 a)) = (a ∩ (b⊥ ∪ (a ∩ b)))
17	16	lor 70	. . . . . . . 8 (a⊥ ∪ (a ∩ (b →1 a))) = (a⊥ ∪ (a ∩ (b⊥ ∪ (a ∩ b))))
18		u1lem3 749	. . . . . . . . . 10 (a →1 (b →1 a)) = (a⊥ ∪ ((a ∩ b) ∪ (a ∩ b⊥ )))
19		ax-a2 31	. . . . . . . . . . . . . 14 (b⊥ ∪ (a ∩ b)) = ((a ∩ b) ∪ b⊥ )
20	19	lan 77	. . . . . . . . . . . . 13 (a ∩ (b⊥ ∪ (a ∩ b))) = (a ∩ ((a ∩ b) ∪ b⊥ ))
21		coman1 185	. . . . . . . . . . . . . . 15 (a ∩ b) C a
22		coman2 186	. . . . . . . . . . . . . . . 16 (a ∩ b) C b
23	22	comcom2 183	. . . . . . . . . . . . . . 15 (a ∩ b) C b⊥
24	21, 23	fh2 470	. . . . . . . . . . . . . 14 (a ∩ ((a ∩ b) ∪ b⊥ )) = ((a ∩ (a ∩ b)) ∪ (a ∩ b⊥ ))
25		anass 76	. . . . . . . . . . . . . . . . 17 ((a ∩ a) ∩ b) = (a ∩ (a ∩ b))
26	25	ax-r1 35	. . . . . . . . . . . . . . . 16 (a ∩ (a ∩ b)) = ((a ∩ a) ∩ b)
27		anidm 111	. . . . . . . . . . . . . . . . 17 (a ∩ a) = a
28	27	ran 78	. . . . . . . . . . . . . . . 16 ((a ∩ a) ∩ b) = (a ∩ b)
29	26, 28	ax-r2 36	. . . . . . . . . . . . . . 15 (a ∩ (a ∩ b)) = (a ∩ b)
30	29	ax-r5 38	. . . . . . . . . . . . . 14 ((a ∩ (a ∩ b)) ∪ (a ∩ b⊥ )) = ((a ∩ b) ∪ (a ∩ b⊥ ))
31	24, 30	ax-r2 36	. . . . . . . . . . . . 13 (a ∩ ((a ∩ b) ∪ b⊥ )) = ((a ∩ b) ∪ (a ∩ b⊥ ))
32	20, 31	ax-r2 36	. . . . . . . . . . . 12 (a ∩ (b⊥ ∪ (a ∩ b))) = ((a ∩ b) ∪ (a ∩ b⊥ ))
33	32	ax-r1 35	. . . . . . . . . . 11 ((a ∩ b) ∪ (a ∩ b⊥ )) = (a ∩ (b⊥ ∪ (a ∩ b)))
34	33	lor 70	. . . . . . . . . 10 (a⊥ ∪ ((a ∩ b) ∪ (a ∩ b⊥ ))) = (a⊥ ∪ (a ∩ (b⊥ ∪ (a ∩ b))))
35	18, 34	ax-r2 36	. . . . . . . . 9 (a →1 (b →1 a)) = (a⊥ ∪ (a ∩ (b⊥ ∪ (a ∩ b))))
36	35	ax-r1 35	. . . . . . . 8 (a⊥ ∪ (a ∩ (b⊥ ∪ (a ∩ b)))) = (a →1 (b →1 a))
37	17, 36	ax-r2 36	. . . . . . 7 (a⊥ ∪ (a ∩ (b →1 a))) = (a →1 (b →1 a))
38	11, 37	ax-r2 36	. . . . . 6 ((a →1 (b →1 a)) ∪ a⊥ ) = (a →1 (b →1 a))
39	10, 38	ax-r2 36	. . . . 5 (a⊥ ∪ (a →1 (b →1 a))) = (a →1 (b →1 a))
40	9, 39	2an 79	. . . 4 ((a⊥ ∪ a) ∩ (a⊥ ∪ (a →1 (b →1 a)))) = (1 ∩ (a →1 (b →1 a)))
41		ancom 74	. . . . 5 (1 ∩ (a →1 (b →1 a))) = ((a →1 (b →1 a)) ∩ 1)
42		an1 106	. . . . 5 ((a →1 (b →1 a)) ∩ 1) = (a →1 (b →1 a))
43	41, 42	ax-r2 36	. . . 4 (1 ∩ (a →1 (b →1 a))) = (a →1 (b →1 a))
44	40, 43	ax-r2 36	. . 3 ((a⊥ ∪ a) ∩ (a⊥ ∪ (a →1 (b →1 a)))) = (a →1 (b →1 a))
45	5, 44	ax-r2 36	. 2 (a⊥ ∪ (a ∩ (a →1 (b →1 a)))) = (a →1 (b →1 a))
46	1, 45	ax-r2 36	1 (a →1 (a →1 (b →1 a))) = (a →1 (b →1 a))

Syntax hints:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8   →₁ wi1 12

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-i1 44  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is referenced by: (None)