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 syl5bb ( 𝑦 = 𝑃 → ( 𝑢 ∈ ( ( ( 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 𝑢 ) ∈ 𝐴 ) )