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 = j ∈ Top | ∀ x ∈ j ∀ y ∈ x ∃ u ∈ j ∩ 𝒫 x y ∈ u ∧ j ↾ 𝑡 u ∈ A

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 0 clly class Locally A
2 vj setvar j
3 ctop class 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 j ∩ 𝒫 x
11 6 cv setvar y
12 8 cv setvar u
13 11 12 wcel wff y ∈ u
14 crest class ↾ 𝑡
15 5 12 14 co class j ↾ 𝑡 u
16 15 0 wcel wff j ↾ 𝑡 u ∈ A
17 13 16 wa wff y ∈ u ∧ j ↾ 𝑡 u ∈ A
18 17 8 10 wrex wff ∃ u ∈ j ∩ 𝒫 x y ∈ u ∧ j ↾ 𝑡 u ∈ A
19 18 6 7 wral wff ∀ y ∈ x ∃ u ∈ j ∩ 𝒫 x y ∈ u ∧ j ↾ 𝑡 u ∈ A
20 19 4 5 wral wff ∀ x ∈ j ∀ y ∈ x ∃ u ∈ j ∩ 𝒫 x y ∈ u ∧ j ↾ 𝑡 u ∈ A
21 20 2 3 crab class j ∈ Top | ∀ x ∈ j ∀ y ∈ x ∃ u ∈ j ∩ 𝒫 x y ∈ u ∧ j ↾ 𝑡 u ∈ A
22 1 21 wceq wff Locally A = j ∈ Top | ∀ x ∈ j ∀ y ∈ x ∃ u ∈ j ∩ 𝒫 x y ∈ u ∧ j ↾ 𝑡 u ∈ A