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 𝐴 = { 𝑗 ∈ 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 𝑢 ) ∈ 𝐴 ) }