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