This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nllyi

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

Ref Expression
Assertion nllyi ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) → ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑢 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 isnlly ⊢ ( 𝐽 ∈ 𝑛-Locally 𝐴 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) )
2 1 simprbi ⊢ ( 𝐽 ∈ 𝑛-Locally 𝐴 → ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 )
3 pweq ⊢ ( 𝑥 = 𝑈 → 𝒫 𝑥 = 𝒫 𝑈 )
4 3 ineq2d ⊢ ( 𝑥 = 𝑈 → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) = ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑈 ) )
5 4 rexeqdv ⊢ ( 𝑥 = 𝑈 → ( ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ↔ ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑈 ) ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) )
6 5 raleqbi1dv ⊢ ( 𝑥 = 𝑈 → ( ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ↔ ∀ 𝑦 ∈ 𝑈 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑈 ) ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) )
7 6 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ∧ 𝑈 ∈ 𝐽 ) → ∀ 𝑦 ∈ 𝑈 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑈 ) ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 )
8 2 7 sylan ⊢ ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ) → ∀ 𝑦 ∈ 𝑈 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑈 ) ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 )
9 elin ⊢ ( 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑈 ) ↔ ( 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∧ 𝑢 ∈ 𝒫 𝑈 ) )
10 sneq ⊢ ( 𝑦 = 𝑃 → { 𝑦 } = { 𝑃 } )
11 10 fveq2d ⊢ ( 𝑦 = 𝑃 → ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) = ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) )
12 11 eleq2d ⊢ ( 𝑦 = 𝑃 → ( 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ↔ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) )
13 velpw ⊢ ( 𝑢 ∈ 𝒫 𝑈 ↔ 𝑢 ⊆ 𝑈 )
14 13 a1i ⊢ ( 𝑦 = 𝑃 → ( 𝑢 ∈ 𝒫 𝑈 ↔ 𝑢 ⊆ 𝑈 ) )
15 12 14 anbi12d ⊢ ( 𝑦 = 𝑃 → ( ( 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∧ 𝑢 ∈ 𝒫 𝑈 ) ↔ ( 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ 𝑢 ⊆ 𝑈 ) ) )
16 9 15 bitrid ⊢ ( 𝑦 = 𝑃 → ( 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑈 ) ↔ ( 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ 𝑢 ⊆ 𝑈 ) ) )
17 16 anbi1d ⊢ ( 𝑦 = 𝑃 → ( ( 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑈 ) ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ↔ ( ( 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ 𝑢 ⊆ 𝑈 ) ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) )
18 anass ⊢ ( ( ( 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ 𝑢 ⊆ 𝑈 ) ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ↔ ( 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑢 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) )
19 17 18 bitrdi ⊢ ( 𝑦 = 𝑃 → ( ( 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑈 ) ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ↔ ( 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑢 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) )
20 19 rexbidv2 ⊢ ( 𝑦 = 𝑃 → ( ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑈 ) ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ↔ ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑢 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) )
21 20 rspccva ⊢ ( ( ∀ 𝑦 ∈ 𝑈 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑈 ) ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ∧ 𝑃 ∈ 𝑈 ) → ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑢 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) )
22 8 21 stoic3 ⊢ ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) → ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑢 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) )