Theorem isnlly

Description: The property of being an n-locally A topological space. (Contributed by Mario Carneiro, 2-Mar-2015)

	Ref	Expression
Assertion	isnlly	⊢ ( 𝐽 ∈ 𝑛-Locally 𝐴 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑗 = 𝐽 → ( nei ‘ 𝑗 ) = ( nei ‘ 𝐽 ) )
2	1	fveq1d	⊢ ( 𝑗 = 𝐽 → ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) = ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) )
3	2	ineq1d	⊢ ( 𝑗 = 𝐽 → ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) = ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) )
4		oveq1	⊢ ( 𝑗 = 𝐽 → ( 𝑗 ↾t 𝑢 ) = ( 𝐽 ↾t 𝑢 ) )
5	4	eleq1d	⊢ ( 𝑗 = 𝐽 → ( ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 ↔ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) )
6	3 5	rexeqbidv	⊢ ( 𝑗 = 𝐽 → ( ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 ↔ ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) )
7	6	ralbidv	⊢ ( 𝑗 = 𝐽 → ( ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 ↔ ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) )
8	7	raleqbi1dv	⊢ ( 𝑗 = 𝐽 → ( ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) )
9		df-nlly	⊢ 𝑛-Locally 𝐴 = { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 }
10	8 9	elrab2	⊢ ( 𝐽 ∈ 𝑛-Locally 𝐴 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) )