Metamath Proof Explorer


Theorem llynlly

Description: A locally A space is n-locally A : the "n-locally" predicate is the weaker notion. (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Assertion llynlly ( 𝐽 ∈ Locally 𝐴𝐽 ∈ 𝑛-Locally 𝐴 )

Proof

Step Hyp Ref Expression
1 llytop ( 𝐽 ∈ Locally 𝐴𝐽 ∈ Top )
2 llyi ( ( 𝐽 ∈ Locally 𝐴𝑥𝐽𝑦𝑥 ) → ∃ 𝑢𝐽 ( 𝑢𝑥𝑦𝑢 ∧ ( 𝐽t 𝑢 ) ∈ 𝐴 ) )
3 simpl1 ( ( ( 𝐽 ∈ Locally 𝐴𝑥𝐽𝑦𝑥 ) ∧ ( 𝑢𝐽 ∧ ( 𝑢𝑥𝑦𝑢 ∧ ( 𝐽t 𝑢 ) ∈ 𝐴 ) ) ) → 𝐽 ∈ Locally 𝐴 )
4 3 1 syl ( ( ( 𝐽 ∈ Locally 𝐴𝑥𝐽𝑦𝑥 ) ∧ ( 𝑢𝐽 ∧ ( 𝑢𝑥𝑦𝑢 ∧ ( 𝐽t 𝑢 ) ∈ 𝐴 ) ) ) → 𝐽 ∈ Top )
5 simprl ( ( ( 𝐽 ∈ Locally 𝐴𝑥𝐽𝑦𝑥 ) ∧ ( 𝑢𝐽 ∧ ( 𝑢𝑥𝑦𝑢 ∧ ( 𝐽t 𝑢 ) ∈ 𝐴 ) ) ) → 𝑢𝐽 )
6 simprr2 ( ( ( 𝐽 ∈ Locally 𝐴𝑥𝐽𝑦𝑥 ) ∧ ( 𝑢𝐽 ∧ ( 𝑢𝑥𝑦𝑢 ∧ ( 𝐽t 𝑢 ) ∈ 𝐴 ) ) ) → 𝑦𝑢 )
7 opnneip ( ( 𝐽 ∈ Top ∧ 𝑢𝐽𝑦𝑢 ) → 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) )
8 4 5 6 7 syl3anc ( ( ( 𝐽 ∈ Locally 𝐴𝑥𝐽𝑦𝑥 ) ∧ ( 𝑢𝐽 ∧ ( 𝑢𝑥𝑦𝑢 ∧ ( 𝐽t 𝑢 ) ∈ 𝐴 ) ) ) → 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) )
9 simprr1 ( ( ( 𝐽 ∈ Locally 𝐴𝑥𝐽𝑦𝑥 ) ∧ ( 𝑢𝐽 ∧ ( 𝑢𝑥𝑦𝑢 ∧ ( 𝐽t 𝑢 ) ∈ 𝐴 ) ) ) → 𝑢𝑥 )
10 velpw ( 𝑢 ∈ 𝒫 𝑥𝑢𝑥 )
11 9 10 sylibr ( ( ( 𝐽 ∈ Locally 𝐴𝑥𝐽𝑦𝑥 ) ∧ ( 𝑢𝐽 ∧ ( 𝑢𝑥𝑦𝑢 ∧ ( 𝐽t 𝑢 ) ∈ 𝐴 ) ) ) → 𝑢 ∈ 𝒫 𝑥 )
12 8 11 elind ( ( ( 𝐽 ∈ Locally 𝐴𝑥𝐽𝑦𝑥 ) ∧ ( 𝑢𝐽 ∧ ( 𝑢𝑥𝑦𝑢 ∧ ( 𝐽t 𝑢 ) ∈ 𝐴 ) ) ) → 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) )
13 simprr3 ( ( ( 𝐽 ∈ Locally 𝐴𝑥𝐽𝑦𝑥 ) ∧ ( 𝑢𝐽 ∧ ( 𝑢𝑥𝑦𝑢 ∧ ( 𝐽t 𝑢 ) ∈ 𝐴 ) ) ) → ( 𝐽t 𝑢 ) ∈ 𝐴 )
14 2 12 13 reximssdv ( ( 𝐽 ∈ Locally 𝐴𝑥𝐽𝑦𝑥 ) → ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽t 𝑢 ) ∈ 𝐴 )
15 14 3expb ( ( 𝐽 ∈ Locally 𝐴 ∧ ( 𝑥𝐽𝑦𝑥 ) ) → ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽t 𝑢 ) ∈ 𝐴 )
16 15 ralrimivva ( 𝐽 ∈ Locally 𝐴 → ∀ 𝑥𝐽𝑦𝑥𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽t 𝑢 ) ∈ 𝐴 )
17 isnlly ( 𝐽 ∈ 𝑛-Locally 𝐴 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥𝐽𝑦𝑥𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽t 𝑢 ) ∈ 𝐴 ) )
18 1 16 17 sylanbrc ( 𝐽 ∈ Locally 𝐴𝐽 ∈ 𝑛-Locally 𝐴 )