Definition df-nlly 22599

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 subneighborhood 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 22597	. 2 class 𝑛-Locally 𝐴
3		vj	. . . . . . . . 9 setvar 𝑗
4	3	cv 1540	. . . . . . . 8 class 𝑗
5		vu	. . . . . . . . 9 setvar 𝑢
6	5	cv 1540	. . . . . . . 8 class 𝑢
7		crest 17112	. . . . . . . 8 class ↾t
8	4, 6, 7	co 7268	. . . . . . 7 class (𝑗 ↾t 𝑢)
9	8, 1	wcel 2109	. . . . . 6 wff (𝑗 ↾t 𝑢) ∈ 𝐴
10		vy	. . . . . . . . . 10 setvar 𝑦
11	10	cv 1540	. . . . . . . . 9 class 𝑦
12	11	csn 4566	. . . . . . . 8 class {𝑦}
13		cnei 22229	. . . . . . . . 9 class nei
14	4, 13	cfv 6430	. . . . . . . 8 class (nei‘𝑗)
15	12, 14	cfv 6430	. . . . . . 7 class ((nei‘𝑗)‘{𝑦})
16		vx	. . . . . . . . 9 setvar 𝑥
17	16	cv 1540	. . . . . . . 8 class 𝑥
18	17	cpw 4538	. . . . . . 7 class 𝒫 𝑥
19	15, 18	cin 3890	. . . . . 6 class (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)
20	9, 5, 19	wrex 3066	. . . . 5 wff ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴
21	20, 10, 17	wral 3065	. . . 4 wff ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴
22	21, 16, 4	wral 3065	. . 3 wff ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴
23		ctop 22023	. . 3 class Top
24	22, 3, 23	crab 3069	. 2 class {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴}
25	2, 24	wceq 1541	1 wff 𝑛-Locally 𝐴 = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴}

This definition is referenced by:  isnlly  22601  nllyeq  22603