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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1	0	cnlly
2		vj	$$setvarj$$
3		ctop	$$class\mathrm{Top}$$
4		vx	$$setvarx$$
5	2	cv	$$setvarj$$
6		vy	$$setvary$$
7	4	cv	$$setvarx$$
8		vu	$$setvaru$$
9		cnei	$$class\mathrm{nei}$$
10	5 9	cfv	$$class\mathrm{nei}\left(j\right)$$
11	6	cv	$$setvary$$
12	11	csn	$$class\left\{y\right\}$$
13	12 10	cfv	$$class\mathrm{nei}\left(j\right)\left(\left\{y\right\}\right)$$
14	7	cpw	$$class𝒫x$$
15	13 14	cin	$$class\left(\mathrm{nei}\left(j\right)\left(\left\{y\right\}\right)\cap 𝒫x\right)$$
16		crest	$$class{\upharpoonright }_{𝑡}$$
17	8	cv	$$setvaru$$
18	5 17 16	co	$$class\left(j{\upharpoonright }_{𝑡}u\right)$$
19	18 0	wcel	$$wffj{\upharpoonright }_{𝑡}u\in A$$
20	19 8 15	wrex	$$wff\exists u\in \left(\mathrm{nei}\left(j\right)\left(\left\{y\right\}\right)\cap 𝒫x\right)j{\upharpoonright }_{𝑡}u\in A$$
21	20 6 7	wral	$$wff\forall y\in x\exists u\in \left(\mathrm{nei}\left(j\right)\left(\left\{y\right\}\right)\cap 𝒫x\right)j{\upharpoonright }_{𝑡}u\in A$$
22	21 4 5	wral	$$wff\forall x\in j\forall y\in x\exists u\in \left(\mathrm{nei}\left(j\right)\left(\left\{y\right\}\right)\cap 𝒫x\right)j{\upharpoonright }_{𝑡}u\in A$$
23	22 2 3	crab	$$class\left\{j\in \mathrm{Top}|\forall x\in j\forall y\in x\exists u\in \left(\mathrm{nei}\left(j\right)\left(\left\{y\right\}\right)\cap 𝒫x\right)j{\upharpoonright }_{𝑡}u\in A\right\}$$
24	1 23	wceq