Definition df-nlly 21640

Description: Define a space that is n-locally 𝐴, where 𝐴 is a topological property like "compact", "connected", or "path-connected". A topological space is n-locally 𝐴 if every neighborhood of a point contains a sub-neighborhood that is 𝐴 in the subspace topology.

The terminology "n-locally", where 'n' stands for "neighborhood", is not standard, although this is sometimes called "weakly locally 𝐴". The reason for the distinction is that some notions only make sense for arbitrary neighborhoods (such as "locally compact", which is actually 𝑛-Locally Comp in our terminology - open compact sets are not very useful), while others such as "locally connected" are strictly weaker notions if the neighborhoods are not required to be open. (Contributed by Mario Carneiro, 2-Mar-2015.)

Assertion

Ref	Expression
df-nlly	⊢ 𝑛-Locally 𝐴 = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴}

Distinct variable group:   𝑢,𝑗,𝑥,𝑦,𝐴

Detailed syntax breakdown of Definition df-nlly

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	cnlly 21638	. 2 class 𝑛-Locally 𝐴
3		vj	. . . . . . . . 9 setvar 𝑗
4	3	cv 1657	. . . . . . . 8 class 𝑗
5		vu	. . . . . . . . 9 setvar 𝑢
6	5	cv 1657	. . . . . . . 8 class 𝑢
7		crest 16433	. . . . . . . 8 class ↾t
8	4, 6, 7	co 6904	. . . . . . 7 class (𝑗 ↾t 𝑢)
9	8, 1	wcel 2166	. . . . . 6 wff (𝑗 ↾t 𝑢) ∈ 𝐴
10		vy	. . . . . . . . . 10 setvar 𝑦
11	10	cv 1657	. . . . . . . . 9 class 𝑦
12	11	csn 4396	. . . . . . . 8 class {𝑦}
13		cnei 21271	. . . . . . . . 9 class nei
14	4, 13	cfv 6122	. . . . . . . 8 class (nei‘𝑗)
15	12, 14	cfv 6122	. . . . . . 7 class ((nei‘𝑗)‘{𝑦})
16		vx	. . . . . . . . 9 setvar 𝑥
17	16	cv 1657	. . . . . . . 8 class 𝑥
18	17	cpw 4377	. . . . . . 7 class 𝒫 𝑥
19	15, 18	cin 3796	. . . . . 6 class (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)
20	9, 5, 19	wrex 3117	. . . . 5 wff ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴
21	20, 10, 17	wral 3116	. . . 4 wff ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴
22	21, 16, 4	wral 3116	. . 3 wff ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴
23		ctop 21067	. . 3 class Top
24	22, 3, 23	crab 3120	. 2 class {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴}
25	2, 24	wceq 1658	1 wff 𝑛-Locally 𝐴 = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴}

This definition is referenced by:  isnlly  21642  nllyeq  21644