Theorem u3lem13a 789

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

Assertion

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

Proof of Theorem u3lem13a

Step	Hyp	Ref	Expression
1		df-i3 46	. 2 (a →3 (a →3 b⊥ )⊥ ) = (((a⊥ ∩ (a →3 b⊥ )⊥ ) ∪ (a⊥ ∩ (a →3 b⊥ )⊥ ⊥ )) ∪ (a ∩ (a⊥ ∪ (a →3 b⊥ )⊥ )))
2		ancom 74	. . . . . . 7 (a⊥ ∩ (a →3 b⊥ )⊥ ) = ((a →3 b⊥ )⊥ ∩ a⊥ )
3		u3lemnana 647	. . . . . . 7 ((a →3 b⊥ )⊥ ∩ a⊥ ) = (a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )))
4	2, 3	ax-r2 36	. . . . . 6 (a⊥ ∩ (a →3 b⊥ )⊥ ) = (a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )))
5		ax-a1 30	. . . . . . . . 9 (a →3 b⊥ ) = (a →3 b⊥ )⊥ ⊥
6	5	ax-r1 35	. . . . . . . 8 (a →3 b⊥ )⊥ ⊥ = (a →3 b⊥ )
7	6	lan 77	. . . . . . 7 (a⊥ ∩ (a →3 b⊥ )⊥ ⊥ ) = (a⊥ ∩ (a →3 b⊥ ))
8		ancom 74	. . . . . . . 8 (a⊥ ∩ (a →3 b⊥ )) = ((a →3 b⊥ ) ∩ a⊥ )
9		u3lemana 607	. . . . . . . 8 ((a →3 b⊥ ) ∩ a⊥ ) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))
10	8, 9	ax-r2 36	. . . . . . 7 (a⊥ ∩ (a →3 b⊥ )) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))
11	7, 10	ax-r2 36	. . . . . 6 (a⊥ ∩ (a →3 b⊥ )⊥ ⊥ ) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))
12	4, 11	2or 72	. . . . 5 ((a⊥ ∩ (a →3 b⊥ )⊥ ) ∪ (a⊥ ∩ (a →3 b⊥ )⊥ ⊥ )) = ((a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )))
13		comanr1 464	. . . . . . . 8 a⊥ C (a⊥ ∩ b⊥ )
14		comanr1 464	. . . . . . . 8 a⊥ C (a⊥ ∩ b⊥ ⊥ )
15	13, 14	com2or 483	. . . . . . 7 a⊥ C ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))
16		comorr 184	. . . . . . . . 9 a C (a ∪ b⊥ )
17		comorr 184	. . . . . . . . 9 a C (a ∪ b⊥ ⊥ )
18	16, 17	com2an 484	. . . . . . . 8 a C ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))
19	18	comcom3 454	. . . . . . 7 a⊥ C ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))
20	15, 19	fh4r 476	. . . . . 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 31	. . . . . . . . 9 (a⊥ ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) = (((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) ∪ a⊥ )
22		lea 160	. . . . . . . . . . 11 (a⊥ ∩ b⊥ ) ≤ a⊥
23		lea 160	. . . . . . . . . . 11 (a⊥ ∩ b⊥ ⊥ ) ≤ a⊥
24	22, 23	lel2or 170	. . . . . . . . . 10 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) ≤ a⊥
25	24	df-le2 131	. . . . . . . . 9 (((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) ∪ a⊥ ) = a⊥
26	21, 25	ax-r2 36	. . . . . . . 8 (a⊥ ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) = a⊥
27		anor2 89	. . . . . . . . . . . . 13 (a⊥ ∩ b⊥ ) = (a ∪ b⊥ ⊥ )⊥
28		anor3 90	. . . . . . . . . . . . 13 (a⊥ ∩ b⊥ ⊥ ) = (a ∪ b⊥ )⊥
29	27, 28	2or 72	. . . . . . . . . . . 12 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) = ((a ∪ b⊥ ⊥ )⊥ ∪ (a ∪ b⊥ )⊥ )
30		ax-a2 31	. . . . . . . . . . . 12 ((a ∪ b⊥ ⊥ )⊥ ∪ (a ∪ b⊥ )⊥ ) = ((a ∪ b⊥ )⊥ ∪ (a ∪ b⊥ ⊥ )⊥ )
31	29, 30	ax-r2 36	. . . . . . . . . . 11 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) = ((a ∪ b⊥ )⊥ ∪ (a ∪ b⊥ ⊥ )⊥ )
32		oran3 93	. . . . . . . . . . 11 ((a ∪ b⊥ )⊥ ∪ (a ∪ b⊥ ⊥ )⊥ ) = ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))⊥
33	31, 32	ax-r2 36	. . . . . . . . . 10 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) = ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))⊥
34	33	lor 70	. . . . . . . . 9 (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) = (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))⊥ )
35		df-t 41	. . . . . . . . . 10 1 = (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))⊥ )
36	35	ax-r1 35	. . . . . . . . 9 (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))⊥ ) = 1
37	34, 36	ax-r2 36	. . . . . . . 8 (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) = 1
38	26, 37	2an 79	. . . . . . 7 ((a⊥ ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) ∩ (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )))) = (a⊥ ∩ 1)
39		an1 106	. . . . . . 7 (a⊥ ∩ 1) = a⊥
40	38, 39	ax-r2 36	. . . . . 6 ((a⊥ ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) ∩ (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )))) = a⊥
41	20, 40	ax-r2 36	. . . . 5 ((a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) = a⊥
42	12, 41	ax-r2 36	. . . 4 ((a⊥ ∩ (a →3 b⊥ )⊥ ) ∪ (a⊥ ∩ (a →3 b⊥ )⊥ ⊥ )) = a⊥
43		comid 187	. . . . . . 7 a C a
44	43	comcom2 183	. . . . . 6 a C a⊥
45		comi31 508	. . . . . . 7 a C (a →3 b⊥ )
46	45	comcom2 183	. . . . . 6 a C (a →3 b⊥ )⊥
47	44, 46	fh1 469	. . . . 5 (a ∩ (a⊥ ∪ (a →3 b⊥ )⊥ )) = ((a ∩ a⊥ ) ∪ (a ∩ (a →3 b⊥ )⊥ ))
48		dff 101	. . . . . . . 8 0 = (a ∩ a⊥ )
49	48	ax-r1 35	. . . . . . 7 (a ∩ a⊥ ) = 0
50		ancom 74	. . . . . . . 8 (a ∩ (a →3 b⊥ )⊥ ) = ((a →3 b⊥ )⊥ ∩ a)
51		u3lemnaa 642	. . . . . . . 8 ((a →3 b⊥ )⊥ ∩ a) = (a ∩ b⊥ ⊥ )
52	50, 51	ax-r2 36	. . . . . . 7 (a ∩ (a →3 b⊥ )⊥ ) = (a ∩ b⊥ ⊥ )
53	49, 52	2or 72	. . . . . 6 ((a ∩ a⊥ ) ∪ (a ∩ (a →3 b⊥ )⊥ )) = (0 ∪ (a ∩ b⊥ ⊥ ))
54		ax-a2 31	. . . . . . 7 (0 ∪ (a ∩ b⊥ ⊥ )) = ((a ∩ b⊥ ⊥ ) ∪ 0)
55		or0 102	. . . . . . 7 ((a ∩ b⊥ ⊥ ) ∪ 0) = (a ∩ b⊥ ⊥ )
56	54, 55	ax-r2 36	. . . . . 6 (0 ∪ (a ∩ b⊥ ⊥ )) = (a ∩ b⊥ ⊥ )
57	53, 56	ax-r2 36	. . . . 5 ((a ∩ a⊥ ) ∪ (a ∩ (a →3 b⊥ )⊥ )) = (a ∩ b⊥ ⊥ )
58	47, 57	ax-r2 36	. . . 4 (a ∩ (a⊥ ∪ (a →3 b⊥ )⊥ )) = (a ∩ b⊥ ⊥ )
59	42, 58	2or 72	. . 3 (((a⊥ ∩ (a →3 b⊥ )⊥ ) ∪ (a⊥ ∩ (a →3 b⊥ )⊥ ⊥ )) ∪ (a ∩ (a⊥ ∪ (a →3 b⊥ )⊥ ))) = (a⊥ ∪ (a ∩ b⊥ ⊥ ))
60		ax-a1 30	. . . . . . 7 b = b⊥ ⊥
61	60	ax-r1 35	. . . . . 6 b⊥ ⊥ = b
62	61	lan 77	. . . . 5 (a ∩ b⊥ ⊥ ) = (a ∩ b)
63	62	lor 70	. . . 4 (a⊥ ∪ (a ∩ b⊥ ⊥ )) = (a⊥ ∪ (a ∩ b))
64		df-i1 44	. . . . 5 (a →1 b) = (a⊥ ∪ (a ∩ b))
65	64	ax-r1 35	. . . 4 (a⊥ ∪ (a ∩ b)) = (a →1 b)
66	63, 65	ax-r2 36	. . 3 (a⊥ ∪ (a ∩ b⊥ ⊥ )) = (a →1 b)
67	59, 66	ax-r2 36	. 2 (((a⊥ ∩ (a →3 b⊥ )⊥ ) ∪ (a⊥ ∩ (a →3 b⊥ )⊥ ⊥ )) ∪ (a ∩ (a⊥ ∪ (a →3 b⊥ )⊥ ))) = (a →1 b)
68	1, 67	ax-r2 36	1 (a →3 (a →3 b⊥ )⊥ ) = (a →1 b)

This proof depends on syntax axioms:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8  0wf 9   →₁ wi1 12   →₃ wi3 14

This proof depends on 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 proof depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-i3 46  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is used by:  u3lem14aa2  793