Definition df-nlly 23779

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 23777	. 2 class 𝑛-Locally 𝐴
3		vj	. . . . . . . . 9 setvar 𝑗
4	3	cv 1569	. . . . . . . 8 class 𝑗
5		vu	. . . . . . . . 9 setvar 𝑢
6	5	cv 1569	. . . . . . . 8 class 𝑢
7		crest 17584	. . . . . . . 8 class ↾t
8	4, 6, 7	co 7418	. . . . . . 7 class (𝑗 ↾t 𝑢)
9	8, 1	wcel 2145	. . . . . 6 wff (𝑗 ↾t 𝑢) ∈ 𝐴
10		vy	. . . . . . . . . 10 setvar 𝑦
11	10	cv 1569	. . . . . . . . 9 class 𝑦
12	11	csn 4584	. . . . . . . 8 class {𝑦}
13		cnei 23408	. . . . . . . . 9 class nei
14	4, 13	cfv 6537	. . . . . . . 8 class (nei‘𝑗)
15	12, 14	cfv 6537	. . . . . . 7 class ((nei‘𝑗)‘{𝑦})
16		vx	. . . . . . . . 9 setvar 𝑥
17	16	cv 1569	. . . . . . . 8 class 𝑥
18	17	cpw 4557	. . . . . . 7 class 𝒫 𝑥
19	15, 18	cin 3898	. . . . . 6 class (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)
20	9, 5, 19	wrex 3087	. . . . 5 wff ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴
21	20, 10, 17	wral 3077	. . . 4 wff ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴
22	21, 16, 4	wral 3077	. . 3 wff ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴
23		ctop 23204	. . 3 class Top
24	22, 3, 23	crab 3413	. 2 class {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴}
25	2, 24	wceq 1570	1 wff 𝑛-Locally 𝐴 = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴}

This definition is used by:  isnlly  23781  nllyeq  23783