df-lly

Description: Define a space that is locally A , where A is a topological property like "compact", "connected", or "path-connected". A topological space is locally A if every neighborhood of a point contains an open subneighborhood that is A in the subspace topology. (Contributed by Mario Carneiro, 2-Mar-2015)

		Ref	Expression
	Assertion	df-lly	$⊢ LocallyA=\{j \in Top \| \forall x \in j \forall y \in x \exists u \in (j \cap 𝒫 x) (y \in u \land j ↾_{𝑡} u \in A)\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$class A$
1	0	clly	$class LocallyA$
2		vj	$setvar j$
3		ctop	$class Top$
4		vx	$setvar x$
5	2	cv	$setvar j$
6		vy	$setvar y$
7	4	cv	$setvar x$
8		vu	$setvar u$
9	7	cpw	$class 𝒫 x$
10	5 9	cin	$class (j \cap 𝒫 x)$
11	6	cv	$setvar y$
12	8	cv	$setvar u$
13	11 12	wcel	$wff y \in u$
14		crest	$class ↾_{𝑡}$
15	5 12 14	co	$class (j ↾_{𝑡} u)$
16	15 0	wcel	$wff j ↾_{𝑡} u \in A$
17	13 16	wa	$wff (y \in u \land j ↾_{𝑡} u \in A)$
18	17 8 10	wrex	$wff \exists u \in (j \cap 𝒫 x) (y \in u \land j ↾_{𝑡} u \in A)$
19	18 6 7	wral	$wff \forall y \in x \exists u \in (j \cap 𝒫 x) (y \in u \land j ↾_{𝑡} u \in A)$
20	19 4 5	wral	$wff \forall x \in j \forall y \in x \exists u \in (j \cap 𝒫 x) (y \in u \land j ↾_{𝑡} u \in A)$
21	20 2 3	crab	$class \{j \in Top \| \forall x \in j \forall y \in x \exists u \in (j \cap 𝒫 x) (y \in u \land j ↾_{𝑡} u \in A)\}$
22	1 21	wceq	$wff LocallyA=\{j \in Top \| \forall x \in j \forall y \in x \exists u \in (j \cap 𝒫 x) (y \in u \land j ↾_{𝑡} u \in A)\}$

Metamath Proof Explorer

Definition df-lly

Detailed syntax breakdown