Definition df-lly 22068

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 22066	. 2 class Locally 𝐴
3		vy	. . . . . . . 8 setvar 𝑦
4		vu	. . . . . . . 8 setvar 𝑢
5	3, 4	wel 2111	. . . . . . 7 wff 𝑦 ∈ 𝑢
6		vj	. . . . . . . . . 10 setvar 𝑗
7	6	cv 1532	. . . . . . . . 9 class 𝑗
8	4	cv 1532	. . . . . . . . 9 class 𝑢
9		crest 16688	. . . . . . . . 9 class ↾t
10	7, 8, 9	co 7150	. . . . . . . 8 class (𝑗 ↾t 𝑢)
11	10, 1	wcel 2110	. . . . . . 7 wff (𝑗 ↾t 𝑢) ∈ 𝐴
12	5, 11	wa 398	. . . . . 6 wff (𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝐴)
13		vx	. . . . . . . . 9 setvar 𝑥
14	13	cv 1532	. . . . . . . 8 class 𝑥
15	14	cpw 4539	. . . . . . 7 class 𝒫 𝑥
16	7, 15	cin 3935	. . . . . 6 class (𝑗 ∩ 𝒫 𝑥)
17	12, 4, 16	wrex 3139	. . . . 5 wff ∃𝑢 ∈ (𝑗 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝐴)
18	17, 3, 14	wral 3138	. . . 4 wff ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝑗 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝐴)
19	18, 13, 7	wral 3138	. . 3 wff ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝑗 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝐴)
20		ctop 21495	. . 3 class Top
21	19, 6, 20	crab 3142	. 2 class {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝑗 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝐴)}
22	2, 21	wceq 1533	1 wff Locally 𝐴 = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝑗 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝐴)}

This definition is referenced by:  islly  22070  llyeq  22072