Definition df-lly 22525

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

Assertion

Ref	Expression
df-lly	⊢ Locally 𝐴 = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝑗 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝐴)}

Distinct variable group:   𝑢,𝑗,𝑥,𝑦,𝐴

Detailed syntax breakdown of Definition df-lly

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	clly 22523	. 2 class Locally 𝐴
3		vy	. . . . . . . 8 setvar 𝑦
4		vu	. . . . . . . 8 setvar 𝑢
5	3, 4	wel 2109	. . . . . . 7 wff 𝑦 ∈ 𝑢
6		vj	. . . . . . . . . 10 setvar 𝑗
7	6	cv 1538	. . . . . . . . 9 class 𝑗
8	4	cv 1538	. . . . . . . . 9 class 𝑢
9		crest 17048	. . . . . . . . 9 class ↾t
10	7, 8, 9	co 7255	. . . . . . . 8 class (𝑗 ↾t 𝑢)
11	10, 1	wcel 2108	. . . . . . 7 wff (𝑗 ↾t 𝑢) ∈ 𝐴
12	5, 11	wa 395	. . . . . 6 wff (𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝐴)
13		vx	. . . . . . . . 9 setvar 𝑥
14	13	cv 1538	. . . . . . . 8 class 𝑥
15	14	cpw 4530	. . . . . . 7 class 𝒫 𝑥
16	7, 15	cin 3882	. . . . . 6 class (𝑗 ∩ 𝒫 𝑥)
17	12, 4, 16	wrex 3064	. . . . 5 wff ∃𝑢 ∈ (𝑗 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝐴)
18	17, 3, 14	wral 3063	. . . 4 wff ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝑗 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝐴)
19	18, 13, 7	wral 3063	. . 3 wff ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝑗 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝐴)
20		ctop 21950	. . 3 class Top
21	19, 6, 20	crab 3067	. 2 class {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝑗 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝐴)}
22	2, 21	wceq 1539	1 wff Locally 𝐴 = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝑗 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝐴)}

This definition is referenced by:  islly  22527  llyeq  22529