Theorem u3lem13a 771

Description: Lemma for unified implication study.

Assertion

Ref	Expression
u3lem13a	(a →3 (a →3 b⊥ )⊥ ) = (a →1 b)

Proof of Theorem u3lem13a

Step	Hyp	Ref	Expression
1		df-i3 45	. 2 (a →3 (a →3 b⊥ )⊥ ) = (((a⊥ ∩ (a →3 b⊥ )⊥ ) ∪ (a⊥ ∩ (a →3 b⊥ )⊥ ⊥ )) ∪ (a ∩ (a⊥ ∪ (a →3 b⊥ )⊥ )))
2		ancom 68	. . . . . . 7 (a⊥ ∩ (a →3 b⊥ )⊥ ) = ((a →3 b⊥ )⊥ ∩ a⊥ )
3		u3lemnana 629	. . . . . . 7 ((a →3 b⊥ )⊥ ∩ a⊥ ) = (a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )))
4	2, 3	ax-r2 35	. . . . . 6 (a⊥ ∩ (a →3 b⊥ )⊥ ) = (a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )))
5		ax-a1 29	. . . . . . . . 9 (a →3 b⊥ ) = (a →3 b⊥ )⊥ ⊥
6	5	ax-r1 34	. . . . . . . 8 (a →3 b⊥ )⊥ ⊥ = (a →3 b⊥ )
7	6	lan 70	. . . . . . 7 (a⊥ ∩ (a →3 b⊥ )⊥ ⊥ ) = (a⊥ ∩ (a →3 b⊥ ))
8		ancom 68	. . . . . . . 8 (a⊥ ∩ (a →3 b⊥ )) = ((a →3 b⊥ ) ∩ a⊥ )
9		u3lemana 589	. . . . . . . 8 ((a →3 b⊥ ) ∩ a⊥ ) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))
10	8, 9	ax-r2 35	. . . . . . 7 (a⊥ ∩ (a →3 b⊥ )) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))
11	7, 10	ax-r2 35	. . . . . 6 (a⊥ ∩ (a →3 b⊥ )⊥ ⊥ ) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))
12	4, 11	2or 67	. . . . 5 ((a⊥ ∩ (a →3 b⊥ )⊥ ) ∪ (a⊥ ∩ (a →3 b⊥ )⊥ ⊥ )) = ((a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )))
13		comanr1 446	. . . . . . . 8 a⊥ C (a⊥ ∩ b⊥ )
14		comanr1 446	. . . . . . . 8 a⊥ C (a⊥ ∩ b⊥ ⊥ )
15	13, 14	com2or 465	. . . . . . 7 a⊥ C ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))
16		comorr 176	. . . . . . . . 9 a C (a ∪ b⊥ )
17		comorr 176	. . . . . . . . 9 a C (a ∪ b⊥ ⊥ )
18	16, 17	com2an 466	. . . . . . . 8 a C ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))
19	18	comcom3 436	. . . . . . 7 a⊥ C ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))
20	15, 19	fh4r 458	. . . . . 6 ((a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) = ((a⊥ ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) ∩ (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))))
21		ax-a2 30	. . . . . . . . 9 (a⊥ ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) = (((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) ∪ a⊥ )
22		lea 152	. . . . . . . . . . 11 (a⊥ ∩ b⊥ ) ≤ a⊥
23		lea 152	. . . . . . . . . . 11 (a⊥ ∩ b⊥ ⊥ ) ≤ a⊥
24	22, 23	lel2or 162	. . . . . . . . . 10 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) ≤ a⊥
25	24	df-le2 123	. . . . . . . . 9 (((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) ∪ a⊥ ) = a⊥
26	21, 25	ax-r2 35	. . . . . . . 8 (a⊥ ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) = a⊥
27		anor2 81	. . . . . . . . . . . . 13 (a⊥ ∩ b⊥ ) = (a ∪ b⊥ ⊥ )⊥
28		anor3 82	. . . . . . . . . . . . 13 (a⊥ ∩ b⊥ ⊥ ) = (a ∪ b⊥ )⊥
29	27, 28	2or 67	. . . . . . . . . . . 12 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) = ((a ∪ b⊥ ⊥ )⊥ ∪ (a ∪ b⊥ )⊥ )
30		ax-a2 30	. . . . . . . . . . . 12 ((a ∪ b⊥ ⊥ )⊥ ∪ (a ∪ b⊥ )⊥ ) = ((a ∪ b⊥ )⊥ ∪ (a ∪ b⊥ ⊥ )⊥ )
31	29, 30	ax-r2 35	. . . . . . . . . . 11 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) = ((a ∪ b⊥ )⊥ ∪ (a ∪ b⊥ ⊥ )⊥ )
32		oran3 85	. . . . . . . . . . 11 ((a ∪ b⊥ )⊥ ∪ (a ∪ b⊥ ⊥ )⊥ ) = ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))⊥
33	31, 32	ax-r2 35	. . . . . . . . . 10 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) = ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))⊥
34	33	lor 66	. . . . . . . . 9 (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) = (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))⊥ )
35		df-t 40	. . . . . . . . . 10 1 = (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))⊥ )
36	35	ax-r1 34	. . . . . . . . 9 (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))⊥ ) = 1
37	34, 36	ax-r2 35	. . . . . . . 8 (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) = 1
38	26, 37	2an 72	. . . . . . 7 ((a⊥ ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) ∩ (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )))) = (a⊥ ∩ 1)
39		an1 98	. . . . . . 7 (a⊥ ∩ 1) = a⊥
40	38, 39	ax-r2 35	. . . . . 6 ((a⊥ ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) ∩ (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )))) = a⊥
41	20, 40	ax-r2 35	. . . . 5 ((a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) = a⊥
42	12, 41	ax-r2 35	. . . 4 ((a⊥ ∩ (a →3 b⊥ )⊥ ) ∪ (a⊥ ∩ (a →3 b⊥ )⊥ ⊥ )) = a⊥
43		comid 179	. . . . . . 7 a C a
44	43	comcom2 175	. . . . . 6 a C a⊥
45		comi31 490	. . . . . . 7 a C (a →3 b⊥ )
46	45	comcom2 175	. . . . . 6 a C (a →3 b⊥ )⊥
47	44, 46	fh1 451	. . . . 5 (a ∩ (a⊥ ∪ (a →3 b⊥ )⊥ )) = ((a ∩ a⊥ ) ∪ (a ∩ (a →3 b⊥ )⊥ ))
48		dff 93	. . . . . . . 8 0 = (a ∩ a⊥ )
49	48	ax-r1 34	. . . . . . 7 (a ∩ a⊥ ) = 0
50		ancom 68	. . . . . . . 8 (a ∩ (a →3 b⊥ )⊥ ) = ((a →3 b⊥ )⊥ ∩ a)
51		u3lemnaa 624	. . . . . . . 8 ((a →3 b⊥ )⊥ ∩ a) = (a ∩ b⊥ ⊥ )
52	50, 51	ax-r2 35	. . . . . . 7 (a ∩ (a →3 b⊥ )⊥ ) = (a ∩ b⊥ ⊥ )
53	49, 52	2or 67	. . . . . 6 ((a ∩ a⊥ ) ∪ (a ∩ (a →3 b⊥ )⊥ )) = (0 ∪ (a ∩ b⊥ ⊥ ))
54		ax-a2 30	. . . . . . 7 (0 ∪ (a ∩ b⊥ ⊥ )) = ((a ∩ b⊥ ⊥ ) ∪ 0)
55		or0 94	. . . . . . 7 ((a ∩ b⊥ ⊥ ) ∪ 0) = (a ∩ b⊥ ⊥ )
56	54, 55	ax-r2 35	. . . . . 6 (0 ∪ (a ∩ b⊥ ⊥ )) = (a ∩ b⊥ ⊥ )
57	53, 56	ax-r2 35	. . . . 5 ((a ∩ a⊥ ) ∪ (a ∩ (a →3 b⊥ )⊥ )) = (a ∩ b⊥ ⊥ )
58	47, 57	ax-r2 35	. . . 4 (a ∩ (a⊥ ∪ (a →3 b⊥ )⊥ )) = (a ∩ b⊥ ⊥ )
59	42, 58	2or 67	. . 3 (((a⊥ ∩ (a →3 b⊥ )⊥ ) ∪ (a⊥ ∩ (a →3 b⊥ )⊥ ⊥ )) ∪ (a ∩ (a⊥ ∪ (a →3 b⊥ )⊥ ))) = (a⊥ ∪ (a ∩ b⊥ ⊥ ))
60		ax-a1 29	. . . . . . 7 b = b⊥ ⊥
61	60	ax-r1 34	. . . . . 6 b⊥ ⊥ = b
62	61	lan 70	. . . . 5 (a ∩ b⊥ ⊥ ) = (a ∩ b)
63	62	lor 66	. . . 4 (a⊥ ∪ (a ∩ b⊥ ⊥ )) = (a⊥ ∪ (a ∩ b))
64		df-i1 43	. . . . 5 (a →1 b) = (a⊥ ∪ (a ∩ b))
65	64	ax-r1 34	. . . 4 (a⊥ ∪ (a ∩ b)) = (a →1 b)
66	63, 65	ax-r2 35	. . 3 (a⊥ ∪ (a ∩ b⊥ ⊥ )) = (a →1 b)
67	59, 66	ax-r2 35	. 2 (((a⊥ ∩ (a →3 b⊥ )⊥ ) ∪ (a⊥ ∩ (a →3 b⊥ )⊥ ⊥ )) ∪ (a ∩ (a⊥ ∪ (a →3 b⊥ )⊥ ))) = (a →1 b)
68	1, 67	ax-r2 35	1 (a →3 (a →3 b⊥ )⊥ ) = (a →1 b)

Syntax hints:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 9  0wf 10   →₁ wi1 13   →₃ wi3 15

This theorem is referenced by:  u3lem14aa2 775

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-i3 45  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org