Definition df-nlly

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

The terminology "n-locally", where 'n' stands for "neighborhood", is not standard, although this is sometimes called "weakly locally A ". The reason for the distinction is that some notions only make sense for arbitrary neighborhoods (such as "locally compact", which is actually N-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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1	0	cnlly	⊢ 𝑛-Locally 𝐴
2		vj	⊢ 𝑗
3		ctop	⊢ Top
4		vx	⊢ 𝑥
5	2	cv	⊢ 𝑗
6		vy	⊢ 𝑦
7	4	cv	⊢ 𝑥
8		vu	⊢ 𝑢
9		cnei	⊢ nei
10	5 9	cfv	⊢ ( nei ‘ 𝑗 )
11	6	cv	⊢ 𝑦
12	11	csn	⊢ { 𝑦 }
13	12 10	cfv	⊢ ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } )
14	7	cpw	⊢ 𝒫 𝑥
15	13 14	cin	⊢ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 )
16		crest	⊢ ↾t
17	8	cv	⊢ 𝑢
18	5 17 16	co	⊢ ( 𝑗 ↾t 𝑢 )
19	18 0	wcel	⊢ ( 𝑗 ↾t 𝑢 ) ∈ 𝐴
20	19 8 15	wrex	⊢ ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐴
21	20 6 7	wral	⊢ ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐴
22	21 4 5	wral	⊢ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐴
23	22 2 3	crab	⊢ { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 }
24	1 23	wceq	⊢ 𝑛-Locally 𝐴 = { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 }