This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC TOPOLOGY Topology Local topological properties 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 𝐴 = { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝑗 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 ) }
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cA ⊢ 𝐴
1
0
clly ⊢ Locally 𝐴
2
vj ⊢ 𝑗
3
ctop ⊢ Top
4
vx ⊢ 𝑥
5
2
cv ⊢ 𝑗
6
vy ⊢ 𝑦
7
4
cv ⊢ 𝑥
8
vu ⊢ 𝑢
9
7
cpw ⊢ 𝒫 𝑥
10
5 9
cin ⊢ ( 𝑗 ∩ 𝒫 𝑥 )
11
6
cv ⊢ 𝑦
12
8
cv ⊢ 𝑢
13
11 12
wcel ⊢ 𝑦 ∈ 𝑢
14
crest ⊢ ↾t
15
5 12 14
co ⊢ ( 𝑗 ↾t 𝑢 )
16
15 0
wcel ⊢ ( 𝑗 ↾t 𝑢 ) ∈ 𝐴
17
13 16
wa ⊢ ( 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 )
18
17 8 10
wrex ⊢ ∃ 𝑢 ∈ ( 𝑗 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 )
19
18 6 7
wral ⊢ ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝑗 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 )
20
19 4 5
wral ⊢ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝑗 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 )
21
20 2 3
crab ⊢ { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝑗 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 ) }
22
1 21
wceq ⊢ Locally 𝐴 = { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝑗 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 ) }