Metamath Proof Explorer

Theorem nlly2i

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

Ref Expression
Assertion nlly2i 
|- ( ( J e. N-Locally A /\ U e. J /\ P e. U ) -> E. s e. ~P U E. u e. J ( P e. u /\ u C_ s /\ ( J |`t s ) e. A ) )

Proof

Step Hyp Ref Expression
1 nllyi 
 |-  ( ( J e. N-Locally A /\ U e. J /\ P e. U ) -> E. s e. ( ( nei ` J ) ` { P } ) ( s C_ U /\ ( J |`t s ) e. A ) )
2 simprrl 
 |-  ( ( ( J e. N-Locally A /\ U e. J /\ P e. U ) /\ ( s e. ( ( nei ` J ) ` { P } ) /\ ( s C_ U /\ ( J |`t s ) e. A ) ) ) -> s C_ U )
3 velpw 
 |-  ( s e. ~P U <-> s C_ U )
4 2 3 sylibr 
 |-  ( ( ( J e. N-Locally A /\ U e. J /\ P e. U ) /\ ( s e. ( ( nei ` J ) ` { P } ) /\ ( s C_ U /\ ( J |`t s ) e. A ) ) ) -> s e. ~P U )
5 simpl1 
 |-  ( ( ( J e. N-Locally A /\ U e. J /\ P e. U ) /\ ( s e. ( ( nei ` J ) ` { P } ) /\ ( s C_ U /\ ( J |`t s ) e. A ) ) ) -> J e. N-Locally A )
6 nllytop 
 |-  ( J e. N-Locally A -> J e. Top )
7 5 6 syl 
 |-  ( ( ( J e. N-Locally A /\ U e. J /\ P e. U ) /\ ( s e. ( ( nei ` J ) ` { P } ) /\ ( s C_ U /\ ( J |`t s ) e. A ) ) ) -> J e. Top )
8 simprl 
 |-  ( ( ( J e. N-Locally A /\ U e. J /\ P e. U ) /\ ( s e. ( ( nei ` J ) ` { P } ) /\ ( s C_ U /\ ( J |`t s ) e. A ) ) ) -> s e. ( ( nei ` J ) ` { P } ) )
9 neii2 
 |-  ( ( J e. Top /\ s e. ( ( nei ` J ) ` { P } ) ) -> E. u e. J ( { P } C_ u /\ u C_ s ) )
10 7 8 9 syl2anc 
 |-  ( ( ( J e. N-Locally A /\ U e. J /\ P e. U ) /\ ( s e. ( ( nei ` J ) ` { P } ) /\ ( s C_ U /\ ( J |`t s ) e. A ) ) ) -> E. u e. J ( { P } C_ u /\ u C_ s ) )
11 simprl 
 |-  ( ( ( ( J e. N-Locally A /\ U e. J /\ P e. U ) /\ ( s e. ( ( nei ` J ) ` { P } ) /\ ( s C_ U /\ ( J |`t s ) e. A ) ) ) /\ ( { P } C_ u /\ u C_ s ) ) -> { P } C_ u )
12 simpll3 
 |-  ( ( ( ( J e. N-Locally A /\ U e. J /\ P e. U ) /\ ( s e. ( ( nei ` J ) ` { P } ) /\ ( s C_ U /\ ( J |`t s ) e. A ) ) ) /\ ( { P } C_ u /\ u C_ s ) ) -> P e. U )
13 snssg 
 |-  ( P e. U -> ( P e. u <-> { P } C_ u ) )
14 12 13 syl 
 |-  ( ( ( ( J e. N-Locally A /\ U e. J /\ P e. U ) /\ ( s e. ( ( nei ` J ) ` { P } ) /\ ( s C_ U /\ ( J |`t s ) e. A ) ) ) /\ ( { P } C_ u /\ u C_ s ) ) -> ( P e. u <-> { P } C_ u ) )
15 11 14 mpbird 
 |-  ( ( ( ( J e. N-Locally A /\ U e. J /\ P e. U ) /\ ( s e. ( ( nei ` J ) ` { P } ) /\ ( s C_ U /\ ( J |`t s ) e. A ) ) ) /\ ( { P } C_ u /\ u C_ s ) ) -> P e. u )
16 simprr 
 |-  ( ( ( ( J e. N-Locally A /\ U e. J /\ P e. U ) /\ ( s e. ( ( nei ` J ) ` { P } ) /\ ( s C_ U /\ ( J |`t s ) e. A ) ) ) /\ ( { P } C_ u /\ u C_ s ) ) -> u C_ s )
17 simprrr 
 |-  ( ( ( J e. N-Locally A /\ U e. J /\ P e. U ) /\ ( s e. ( ( nei ` J ) ` { P } ) /\ ( s C_ U /\ ( J |`t s ) e. A ) ) ) -> ( J |`t s ) e. A )
18 17 adantr 
 |-  ( ( ( ( J e. N-Locally A /\ U e. J /\ P e. U ) /\ ( s e. ( ( nei ` J ) ` { P } ) /\ ( s C_ U /\ ( J |`t s ) e. A ) ) ) /\ ( { P } C_ u /\ u C_ s ) ) -> ( J |`t s ) e. A )
19 15 16 18 3jca 
 |-  ( ( ( ( J e. N-Locally A /\ U e. J /\ P e. U ) /\ ( s e. ( ( nei ` J ) ` { P } ) /\ ( s C_ U /\ ( J |`t s ) e. A ) ) ) /\ ( { P } C_ u /\ u C_ s ) ) -> ( P e. u /\ u C_ s /\ ( J |`t s ) e. A ) )
20 19 ex 
 |-  ( ( ( J e. N-Locally A /\ U e. J /\ P e. U ) /\ ( s e. ( ( nei ` J ) ` { P } ) /\ ( s C_ U /\ ( J |`t s ) e. A ) ) ) -> ( ( { P } C_ u /\ u C_ s ) -> ( P e. u /\ u C_ s /\ ( J |`t s ) e. A ) ) )
21 20 reximdv 
 |-  ( ( ( J e. N-Locally A /\ U e. J /\ P e. U ) /\ ( s e. ( ( nei ` J ) ` { P } ) /\ ( s C_ U /\ ( J |`t s ) e. A ) ) ) -> ( E. u e. J ( { P } C_ u /\ u C_ s ) -> E. u e. J ( P e. u /\ u C_ s /\ ( J |`t s ) e. A ) ) )
22 10 21 mpd 
 |-  ( ( ( J e. N-Locally A /\ U e. J /\ P e. U ) /\ ( s e. ( ( nei ` J ) ` { P } ) /\ ( s C_ U /\ ( J |`t s ) e. A ) ) ) -> E. u e. J ( P e. u /\ u C_ s /\ ( J |`t s ) e. A ) )
23 1 4 22 reximssdv 
 |-  ( ( J e. N-Locally A /\ U e. J /\ P e. U ) -> E. s e. ~P U E. u e. J ( P e. u /\ u C_ s /\ ( J |`t s ) e. A ) )