islly

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

		Ref	Expression
	Assertion	islly	$⊢ J \in LocallyA\leftrightarrow(J \in Top \land \forall x \in J)$

Step	Hyp	Ref	Expression
1		ineq1	$⊢ j = J \to j \cap 𝒫 x = J \cap 𝒫 x$
2		oveq1	$⊢ j = J \to j ↾_{𝑡} u = J ↾_{𝑡} u$
3	2	eleq1d	$⊢ j = J \to (j ↾_{𝑡} u \in A \leftrightarrow J ↾_{𝑡} u \in A)$
4	3	anbi2d	$⊢ j = J \to ((y \in u \land j ↾_{𝑡} u \in A) \leftrightarrow (y \in u \land J ↾_{𝑡} u \in A))$
5	1 4	rexeqbidv	$⊢ j = J \to (\exists u \in (j \cap 𝒫 x) (y \in u \land j ↾_{𝑡} u \in A) \leftrightarrow \exists u \in (J \cap 𝒫 x) (y \in u \land J ↾_{𝑡} u \in A))$
6	5	ralbidv	$⊢ j = J \to (\forall y \in x \exists u \in (j \cap 𝒫 x) (y \in u \land j ↾_{𝑡} u \in A) \leftrightarrow \forall y \in x \exists u \in (J \cap 𝒫 x) (y \in u \land J ↾_{𝑡} u \in A))$
7	6	raleqbi1dv	$⊢ j = J \to (\forall x \in j \forall y \in x \exists u \in (j \cap 𝒫 x) (y \in u \land j ↾_{𝑡} u \in A) \leftrightarrow \forall x \in J \forall y \in x \exists u \in (J \cap 𝒫 x) (y \in u \land J ↾_{𝑡} u \in A))$
8		df-lly	$⊢ LocallyA=\{j \in Top \| \forall x \in j\}$
9	7 8	elrab2	$⊢ J \in LocallyA\leftrightarrow(J \in Top \land \forall x \in J)$

Metamath Proof Explorer