isnlly

Description: The property of being an n-locally A topological space. (Contributed by Mario Carneiro, 2-Mar-2015)

		Ref	Expression
	Assertion	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)$

Step	Hyp	Ref	Expression
1		fveq2	$⊢ j = J \to nei (j) = nei (J)$
2	1	fveq1d	$⊢ j = J \to nei (j) (\{y\}) = nei (J) (\{y\})$
3	2	ineq1d	$⊢ j = J \to nei (j) (\{y\}) \cap 𝒫 x = nei (J) (\{y\}) \cap 𝒫 x$
4		oveq1	$⊢ j = J \to j ↾_{𝑡} u = J ↾_{𝑡} u$
5	4	eleq1d	$⊢ j = J \to (j ↾_{𝑡} u \in A \leftrightarrow J ↾_{𝑡} u \in A)$
6	3 5	rexeqbidv	$⊢ j = J \to (\exists u \in (nei (j) (\{y\}) \cap 𝒫 x) j ↾_{𝑡} u \in A \leftrightarrow \exists u \in (nei (J) (\{y\}) \cap 𝒫 x) J ↾_{𝑡} u \in A)$
7	6	ralbidv	$⊢ j = J \to (\forall y \in x \exists u \in (nei (j) (\{y\}) \cap 𝒫 x) j ↾_{𝑡} u \in A \leftrightarrow \forall y \in x \exists u \in (nei (J) (\{y\}) \cap 𝒫 x) J ↾_{𝑡} u \in A)$
8	7	raleqbi1dv	$⊢ j = J \to (\forall x \in j \forall y \in x \exists u \in (nei (j) (\{y\}) \cap 𝒫 x) j ↾_{𝑡} u \in A \leftrightarrow \forall x \in J \forall y \in x \exists u \in (nei (J) (\{y\}) \cap 𝒫 x) J ↾_{𝑡} u \in A)$
9		df-nlly	$⊢ N-LocallyA=\{j \in Top \| \forall x \in j \forall y \in x \exists u \in (nei (j) (\{y\}) \cap 𝒫 x) j ↾_{𝑡} u \in A\}$
10	8 9	elrab2	$⊢ 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)$

Metamath Proof Explorer