Metamath Proof Explorer

Theorem llynlly

Description: A locally A space is n-locally A : the "n-locally" predicate is the weaker notion. (Contributed by Mario Carneiro, 2-Mar-2015)

		Ref	Expression
	Assertion	llynlly	$⊢ J \in LocallyA\toJ \in N-LocallyA$

Proof

Step	Hyp	Ref	Expression
1		llytop	$⊢ J \in LocallyA\toJ \in Top$
2		llyi	$⊢ (J \in LocallyA\landx \in J\landy \in x\to\exists u \in J (u \subseteq x \land y \in u \land J ↾_{𝑡} u \in A))$
3		simpl1	$⊢ ((J \in LocallyA\landx \in J\landy \in x\land(u \in J \land (u \subseteq x \land y \in u \land J ↾_{𝑡} u \in A))\toJ \in LocallyA))$
4	3 1	syl	$⊢ ((J \in LocallyA\landx \in J\landy \in x\land(u \in J \land (u \subseteq x \land y \in u \land J ↾_{𝑡} u \in A))\toJ \in Top))$
5		simprl	$⊢ ((J \in LocallyA\landx \in J\landy \in x\land(u \in J \land (u \subseteq x \land y \in u \land J ↾_{𝑡} u \in A))\tou \in J))$
6		simprr2	$⊢ ((J \in LocallyA\landx \in J\landy \in x\land(u \in J \land (u \subseteq x \land y \in u \land J ↾_{𝑡} u \in A))\toy \in u))$
7		opnneip	$⊢ (J \in Top \land u \in J \land y \in u) \to u \in nei (J) (\{y\})$
8	4 5 6 7	syl3anc	$⊢ ((J \in LocallyA\landx \in J\landy \in x\land(u \in J \land (u \subseteq x \land y \in u \land J ↾_{𝑡} u \in A))\tou \in nei (J) (\{y\})))$
9		simprr1	$⊢ ((J \in LocallyA\landx \in J\landy \in x\land(u \in J \land (u \subseteq x \land y \in u \land J ↾_{𝑡} u \in A))\tou \subseteq x))$
10		velpw	$⊢ u \in 𝒫 x \leftrightarrow u \subseteq x$
11	9 10	sylibr	$⊢ ((J \in LocallyA\landx \in J\landy \in x\land(u \in J \land (u \subseteq x \land y \in u \land J ↾_{𝑡} u \in A))\tou \in 𝒫 x))$
12	8 11	elind	$⊢ ((J \in LocallyA\landx \in J\landy \in x\land(u \in J \land (u \subseteq x \land y \in u \land J ↾_{𝑡} u \in A))\tou \in (nei (J) (\{y\}) \cap 𝒫 x)))$
13		simprr3	$⊢ ((J \in LocallyA\landx \in J\landy \in x\land(u \in J \land (u \subseteq x \land y \in u \land J ↾_{𝑡} u \in A))\toJ ↾_{𝑡} u \in A))$
14	2 12 13	reximssdv	$⊢ (J \in LocallyA\landx \in J\landy \in x\to\exists u \in (nei (J) (\{y\}) \cap 𝒫 x) J ↾_{𝑡} u \in A)$
15	14	3expb	$⊢ (J \in LocallyA\land(x \in J \land y \in x)\to\exists u \in (nei (J) (\{y\}) \cap 𝒫 x) J ↾_{𝑡} u \in A)$
16	15	ralrimivva	$⊢ J \in LocallyA\to\forall x \in J \forall y \in x \exists u \in (nei (J) (\{y\}) \cap 𝒫 x) J ↾_{𝑡} u \in A$
17		isnlly	$⊢ J \in N-LocallyA\leftrightarrow(J \in Top \land \forall x \in J \forall y \in x \exists u \in (nei (J) (\{y\}) \cap 𝒫 x) J ↾_{𝑡} u \in A)$
18	1 16 17	sylanbrc	$⊢ J \in LocallyA\toJ \in N-LocallyA$