Metamath Proof Explorer

Theorem nlly2i

Description: Eliminate the neighborhood symbol from nllyi . (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Assertion nlly2i ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) → ∃ 𝑠 ∈ 𝒫 𝑈 ∃ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 nllyi ⊢ ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) → ∃ 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) )
2 simprrl ⊢ ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑠 ⊆ 𝑈 )
3 velpw ⊢ ( 𝑠 ∈ 𝒫 𝑈 ↔ 𝑠 ⊆ 𝑈 )
4 2 3 sylibr ⊢ ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑠 ∈ 𝒫 𝑈 )
5 simpl1 ⊢ ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝐽 ∈ 𝑛-Locally 𝐴 )
6 nllytop ⊢ ( 𝐽 ∈ 𝑛-Locally 𝐴 → 𝐽 ∈ Top )
7 5 6 syl ⊢ ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝐽 ∈ Top )
8 simprl ⊢ ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) )
9 neii2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ) → ∃ 𝑢 ∈ 𝐽 ( { 𝑃 } ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠 ) )
10 7 8 9 syl2anc ⊢ ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → ∃ 𝑢 ∈ 𝐽 ( { 𝑃 } ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠 ) )
11 simprl ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) ∧ ( { 𝑃 } ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠 ) ) → { 𝑃 } ⊆ 𝑢 )
12 simpll3 ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) ∧ ( { 𝑃 } ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠 ) ) → 𝑃 ∈ 𝑈 )
13 snssg ⊢ ( 𝑃 ∈ 𝑈 → ( 𝑃 ∈ 𝑢 ↔ { 𝑃 } ⊆ 𝑢 ) )
14 12 13 syl ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) ∧ ( { 𝑃 } ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠 ) ) → ( 𝑃 ∈ 𝑢 ↔ { 𝑃 } ⊆ 𝑢 ) )
15 11 14 mpbird ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) ∧ ( { 𝑃 } ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠 ) ) → 𝑃 ∈ 𝑢 )
16 simprr ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) ∧ ( { 𝑃 } ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠 ) ) → 𝑢 ⊆ 𝑠 )
17 simprrr ⊢ ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 )
18 17 adantr ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) ∧ ( { 𝑃 } ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠 ) ) → ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 )
19 15 16 18 3jca ⊢ ( ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) ∧ ( { 𝑃 } ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠 ) ) → ( 𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) )
20 19 ex ⊢ ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → ( ( { 𝑃 } ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠 ) → ( 𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) )
21 20 reximdv ⊢ ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → ( ∃ 𝑢 ∈ 𝐽 ( { 𝑃 } ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠 ) → ∃ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) )
22 10 21 mpd ⊢ ( ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑠 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( 𝑠 ⊆ 𝑈 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → ∃ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) )
23 1 4 22 reximssdv ⊢ ( ( 𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) → ∃ 𝑠 ∈ 𝒫 𝑈 ∃ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ 𝐴 ) )