# Metamath Proof Explorer

## Definition df-lly

Description: Define a space that is locally A , where A is a topological property like "compact", "connected", or "path-connected". A topological space is locally A if every neighborhood of a point contains an open subneighborhood that is A in the subspace topology. (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Assertion df-lly ${⊢}Locally{A}=\left\{{j}\in \mathrm{Top}|\forall {x}\in {j}\phantom{\rule{.4em}{0ex}}\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cA ${class}{A}$
1 0 clly ${class}Locally{A}$
2 vj ${setvar}{j}$
3 ctop ${class}\mathrm{Top}$
4 vx ${setvar}{x}$
5 2 cv ${setvar}{j}$
6 vy ${setvar}{y}$
7 4 cv ${setvar}{x}$
8 vu ${setvar}{u}$
9 7 cpw ${class}𝒫{x}$
10 5 9 cin ${class}\left({j}\cap 𝒫{x}\right)$
11 6 cv ${setvar}{y}$
12 8 cv ${setvar}{u}$
13 11 12 wcel ${wff}{y}\in {u}$
14 crest ${class}{↾}_{𝑡}$
15 5 12 14 co ${class}\left({j}{↾}_{𝑡}{u}\right)$
16 15 0 wcel ${wff}{j}{↾}_{𝑡}{u}\in {A}$
17 13 16 wa ${wff}\left({y}\in {u}\wedge {j}{↾}_{𝑡}{u}\in {A}\right)$
18 17 8 10 wrex ${wff}\exists {u}\in \left({j}\cap 𝒫{x}\right)\phantom{\rule{.4em}{0ex}}\left({y}\in {u}\wedge {j}{↾}_{𝑡}{u}\in {A}\right)$
19 18 6 7 wral ${wff}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {u}\in \left({j}\cap 𝒫{x}\right)\phantom{\rule{.4em}{0ex}}\left({y}\in {u}\wedge {j}{↾}_{𝑡}{u}\in {A}\right)$
20 19 4 5 wral ${wff}\forall {x}\in {j}\phantom{\rule{.4em}{0ex}}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {u}\in \left({j}\cap 𝒫{x}\right)\phantom{\rule{.4em}{0ex}}\left({y}\in {u}\wedge {j}{↾}_{𝑡}{u}\in {A}\right)$
21 20 2 3 crab ${class}\left\{{j}\in \mathrm{Top}|\forall {x}\in {j}\phantom{\rule{.4em}{0ex}}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {u}\in \left({j}\cap 𝒫{x}\right)\phantom{\rule{.4em}{0ex}}\left({y}\in {u}\wedge {j}{↾}_{𝑡}{u}\in {A}\right)\right\}$
22 1 21 wceq ${wff}Locally{A}=\left\{{j}\in \mathrm{Top}|\forall {x}\in {j}\phantom{\rule{.4em}{0ex}}\right\}$