Theorem u1lem4 739

Description: Lemma for unified implication study.

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 43	. 2 (a →1 (a →1 (b →1 a))) = (a⊥ ∪ (a ∩ (a →1 (b →1 a))))
2		comid 179	. . . . 5 a C a
3	2	comcom2 175	. . . 4 a C a⊥
4		u1lemc1 662	. . . 4 a C (a →1 (b →1 a))
5	3, 4	fh4 454	. . 3 (a⊥ ∪ (a ∩ (a →1 (b →1 a)))) = ((a⊥ ∪ a) ∩ (a⊥ ∪ (a →1 (b →1 a))))
6		ax-a2 30	. . . . . 6 (a⊥ ∪ a) = (a ∪ a⊥ )
7		df-t 40	. . . . . . 7 1 = (a ∪ a⊥ )
8	7	ax-r1 34	. . . . . 6 (a ∪ a⊥ ) = 1
9	6, 8	ax-r2 35	. . . . 5 (a⊥ ∪ a) = 1
10		ax-a2 30	. . . . . 6 (a⊥ ∪ (a →1 (b →1 a))) = ((a →1 (b →1 a)) ∪ a⊥ )
11		u1lemona 607	. . . . . . 7 ((a →1 (b →1 a)) ∪ a⊥ ) = (a⊥ ∪ (a ∩ (b →1 a)))
12		df-i1 43	. . . . . . . . . . 11 (b →1 a) = (b⊥ ∪ (b ∩ a))
13		ancom 68	. . . . . . . . . . . 12 (b ∩ a) = (a ∩ b)
14	13	lor 66	. . . . . . . . . . 11 (b⊥ ∪ (b ∩ a)) = (b⊥ ∪ (a ∩ b))
15	12, 14	ax-r2 35	. . . . . . . . . 10 (b →1 a) = (b⊥ ∪ (a ∩ b))
16	15	lan 70	. . . . . . . . 9 (a ∩ (b →1 a)) = (a ∩ (b⊥ ∪ (a ∩ b)))
17	16	lor 66	. . . . . . . 8 (a⊥ ∪ (a ∩ (b →1 a))) = (a⊥ ∪ (a ∩ (b⊥ ∪ (a ∩ b))))
18		u1lem3 731	. . . . . . . . . 10 (a →1 (b →1 a)) = (a⊥ ∪ ((a ∩ b) ∪ (a ∩ b⊥ )))
19		ax-a2 30	. . . . . . . . . . . . . 14 (b⊥ ∪ (a ∩ b)) = ((a ∩ b) ∪ b⊥ )
20	19	lan 70	. . . . . . . . . . . . 13 (a ∩ (b⊥ ∪ (a ∩ b))) = (a ∩ ((a ∩ b) ∪ b⊥ ))
21		coman1 177	. . . . . . . . . . . . . . 15 (a ∩ b) C a
22		coman2 178	. . . . . . . . . . . . . . . 16 (a ∩ b) C b
23	22	comcom2 175	. . . . . . . . . . . . . . 15 (a ∩ b) C b⊥
24	21, 23	fh2 452	. . . . . . . . . . . . . 14 (a ∩ ((a ∩ b) ∪ b⊥ )) = ((a ∩ (a ∩ b)) ∪ (a ∩ b⊥ ))
25		anass 69	. . . . . . . . . . . . . . . . 17 ((a ∩ a) ∩ b) = (a ∩ (a ∩ b))
26	25	ax-r1 34	. . . . . . . . . . . . . . . 16 (a ∩ (a ∩ b)) = ((a ∩ a) ∩ b)
27		anidm 103	. . . . . . . . . . . . . . . . 17 (a ∩ a) = a
28	27	ran 71	. . . . . . . . . . . . . . . 16 ((a ∩ a) ∩ b) = (a ∩ b)
29	26, 28	ax-r2 35	. . . . . . . . . . . . . . 15 (a ∩ (a ∩ b)) = (a ∩ b)
30	29	ax-r5 37	. . . . . . . . . . . . . 14 ((a ∩ (a ∩ b)) ∪ (a ∩ b⊥ )) = ((a ∩ b) ∪ (a ∩ b⊥ ))
31	24, 30	ax-r2 35	. . . . . . . . . . . . 13 (a ∩ ((a ∩ b) ∪ b⊥ )) = ((a ∩ b) ∪ (a ∩ b⊥ ))
32	20, 31	ax-r2 35	. . . . . . . . . . . 12 (a ∩ (b⊥ ∪ (a ∩ b))) = ((a ∩ b) ∪ (a ∩ b⊥ ))
33	32	ax-r1 34	. . . . . . . . . . 11 ((a ∩ b) ∪ (a ∩ b⊥ )) = (a ∩ (b⊥ ∪ (a ∩ b)))
34	33	lor 66	. . . . . . . . . 10 (a⊥ ∪ ((a ∩ b) ∪ (a ∩ b⊥ ))) = (a⊥ ∪ (a ∩ (b⊥ ∪ (a ∩ b))))
35	18, 34	ax-r2 35	. . . . . . . . 9 (a →1 (b →1 a)) = (a⊥ ∪ (a ∩ (b⊥ ∪ (a ∩ b))))
36	35	ax-r1 34	. . . . . . . 8 (a⊥ ∪ (a ∩ (b⊥ ∪ (a ∩ b)))) = (a →1 (b →1 a))
37	17, 36	ax-r2 35	. . . . . . 7 (a⊥ ∪ (a ∩ (b →1 a))) = (a →1 (b →1 a))
38	11, 37	ax-r2 35	. . . . . 6 ((a →1 (b →1 a)) ∪ a⊥ ) = (a →1 (b →1 a))
39	10, 38	ax-r2 35	. . . . 5 (a⊥ ∪ (a →1 (b →1 a))) = (a →1 (b →1 a))
40	9, 39	2an 72	. . . 4 ((a⊥ ∪ a) ∩ (a⊥ ∪ (a →1 (b →1 a)))) = (1 ∩ (a →1 (b →1 a)))
41		ancom 68	. . . . 5 (1 ∩ (a →1 (b →1 a))) = ((a →1 (b →1 a)) ∩ 1)
42		an1 98	. . . . 5 ((a →1 (b →1 a)) ∩ 1) = (a →1 (b →1 a))
43	41, 42	ax-r2 35	. . . 4 (1 ∩ (a →1 (b →1 a))) = (a →1 (b →1 a))
44	40, 43	ax-r2 35	. . 3 ((a⊥ ∪ a) ∩ (a⊥ ∪ (a →1 (b →1 a)))) = (a →1 (b →1 a))
45	5, 44	ax-r2 35	. 2 (a⊥ ∪ (a ∩ (a →1 (b →1 a)))) = (a →1 (b →1 a))
46	1, 45	ax-r2 35	1 (a →1 (a →1 (b →1 a))) = (a →1 (b →1 a))

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

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

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-i1 43  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org