nlly2i

Description: Eliminate the neighborhood symbol from nllyi . (Contributed by Mario Carneiro, 2-Mar-2015)

		Ref	Expression
	Assertion	nlly2i	$⊢ (J \in N-LocallyA\landU \in J\landP \in U\to\exists s \in 𝒫 U \exists u \in J (P \in u \land u \subseteq s \land J ↾_{𝑡} s \in A))$

Proof

Step	Hyp	Ref	Expression
1		nllyi	$⊢ (J \in N-LocallyA\landU \in J\landP \in U\to\exists s \in nei (J) (\{P\}) (s \subseteq U \land J ↾_{𝑡} s \in A))$
2		simprrl	$⊢ ((J \in N-LocallyA\landU \in J\landP \in U\land(s \in nei (J) (\{P\}) \land (s \subseteq U \land J ↾_{𝑡} s \in A))\tos \subseteq U))$
3		velpw	$⊢ s \in 𝒫 U \leftrightarrow s \subseteq U$
4	2 3	sylibr	$⊢ ((J \in N-LocallyA\landU \in J\landP \in U\land(s \in nei (J) (\{P\}) \land (s \subseteq U \land J ↾_{𝑡} s \in A))\tos \in 𝒫 U))$
5		simpl1	$⊢ ((J \in N-LocallyA\landU \in J\landP \in U\land(s \in nei (J) (\{P\}) \land (s \subseteq U \land J ↾_{𝑡} s \in A))\toJ \in N-LocallyA))$
6		nllytop	$⊢ J \in N-LocallyA\toJ \in Top$
7	5 6	syl	$⊢ ((J \in N-LocallyA\landU \in J\landP \in U\land(s \in nei (J) (\{P\}) \land (s \subseteq U \land J ↾_{𝑡} s \in A))\toJ \in Top))$
8		simprl	$⊢ ((J \in N-LocallyA\landU \in J\landP \in U\land(s \in nei (J) (\{P\}) \land (s \subseteq U \land J ↾_{𝑡} s \in A))\tos \in nei (J) (\{P\})))$
9		neii2	$⊢ (J \in Top \land s \in nei (J) (\{P\})) \to \exists u \in J (\{P\} \subseteq u \land u \subseteq s)$
10	7 8 9	syl2anc	$⊢ ((J \in N-LocallyA\landU \in J\landP \in U\land(s \in nei (J) (\{P\}) \land (s \subseteq U \land J ↾_{𝑡} s \in A))\to\exists u \in J (\{P\} \subseteq u \land u \subseteq s)))$
11		simprl	$⊢ (((J \in N-LocallyA\landU \in J\landP \in U\land(s \in nei (J) (\{P\}) \land (s \subseteq U \land J ↾_{𝑡} s \in A))\land(\{P\} \subseteq u \land u \subseteq s)\to\{P\} \subseteq u)))$
12		simpll3	$⊢ (((J \in N-LocallyA\landU \in J\landP \in U\land(s \in nei (J) (\{P\}) \land (s \subseteq U \land J ↾_{𝑡} s \in A))\land(\{P\} \subseteq u \land u \subseteq s)\toP \in U)))$
13		snssg	$⊢ P \in U \to (P \in u \leftrightarrow \{P\} \subseteq u)$
14	12 13	syl	$⊢ (((J \in N-LocallyA\landU \in J\landP \in U\land(s \in nei (J) (\{P\}) \land (s \subseteq U \land J ↾_{𝑡} s \in A))\land(\{P\} \subseteq u \land u \subseteq s)\to(P \in u \leftrightarrow \{P\} \subseteq u))))$
15	11 14	mpbird	$⊢ (((J \in N-LocallyA\landU \in J\landP \in U\land(s \in nei (J) (\{P\}) \land (s \subseteq U \land J ↾_{𝑡} s \in A))\land(\{P\} \subseteq u \land u \subseteq s)\toP \in u)))$
16		simprr	$⊢ (((J \in N-LocallyA\landU \in J\landP \in U\land(s \in nei (J) (\{P\}) \land (s \subseteq U \land J ↾_{𝑡} s \in A))\land(\{P\} \subseteq u \land u \subseteq s)\tou \subseteq s)))$
17		simprrr	$⊢ ((J \in N-LocallyA\landU \in J\landP \in U\land(s \in nei (J) (\{P\}) \land (s \subseteq U \land J ↾_{𝑡} s \in A))\toJ ↾_{𝑡} s \in A))$
18	17	adantr	$⊢ (((J \in N-LocallyA\landU \in J\landP \in U\land(s \in nei (J) (\{P\}) \land (s \subseteq U \land J ↾_{𝑡} s \in A))\land(\{P\} \subseteq u \land u \subseteq s)\toJ ↾_{𝑡} s \in A)))$
19	15 16 18	3jca	$⊢ (((J \in N-LocallyA\landU \in J\landP \in U\land(s \in nei (J) (\{P\}) \land (s \subseteq U \land J ↾_{𝑡} s \in A))\land(\{P\} \subseteq u \land u \subseteq s)\to(P \in u \land u \subseteq s \land J ↾_{𝑡} s \in A))))$
20	19	ex	$⊢ ((J \in N-LocallyA\landU \in J\landP \in U\land(s \in nei (J) (\{P\}) \land (s \subseteq U \land J ↾_{𝑡} s \in A))\to((\{P\} \subseteq u \land u \subseteq s) \to (P \in u \land u \subseteq s \land J ↾_{𝑡} s \in A))))$
21	20	reximdv	$⊢ ((J \in N-LocallyA\landU \in J\landP \in U\land(s \in nei (J) (\{P\}) \land (s \subseteq U \land J ↾_{𝑡} s \in A))\to(\exists u \in J (\{P\} \subseteq u \land u \subseteq s) \to \exists u \in J (P \in u \land u \subseteq s \land J ↾_{𝑡} s \in A))))$
22	10 21	mpd	$⊢ ((J \in N-LocallyA\landU \in J\landP \in U\land(s \in nei (J) (\{P\}) \land (s \subseteq U \land J ↾_{𝑡} s \in A))\to\exists u \in J (P \in u \land u \subseteq s \land J ↾_{𝑡} s \in A)))$
23	1 4 22	reximssdv	$⊢ (J \in N-LocallyA\landU \in J\landP \in U\to\exists s \in 𝒫 U \exists u \in J (P \in u \land u \subseteq s \land J ↾_{𝑡} s \in A))$

Metamath Proof Explorer

Theorem nlly2i

Proof