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

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 𝐴 )