Metamath Proof Explorer

Theorem nllyrest

Description: An open subspace of an n-locally A space is also n-locally A . (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Assertion nllyrest 
|- ( ( J e. N-Locally A /\ B e. J ) -> ( J |`t B ) e. N-Locally A )

Proof

Step Hyp Ref Expression
1 nllytop 
 |-  ( J e. N-Locally A -> J e. Top )
2 resttop 
 |-  ( ( J e. Top /\ B e. J ) -> ( J |`t B ) e. Top )
3 1 2 sylan 
 |-  ( ( J e. N-Locally A /\ B e. J ) -> ( J |`t B ) e. Top )
4 restopn2 
 |-  ( ( J e. Top /\ B e. J ) -> ( x e. ( J |`t B ) <-> ( x e. J /\ x C_ B ) ) )
5 1 4 sylan 
 |-  ( ( J e. N-Locally A /\ B e. J ) -> ( x e. ( J |`t B ) <-> ( x e. J /\ x C_ B ) ) )
6 simp1l 
 |-  ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) -> J e. N-Locally A )
7 simp2l 
 |-  ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) -> x e. J )
8 simp3 
 |-  ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) -> y e. x )
9 nlly2i 
 |-  ( ( J e. N-Locally A /\ x e. J /\ y e. x ) -> E. s e. ~P x E. u e. J ( y e. u /\ u C_ s /\ ( J |`t s ) e. A ) )
10 6 7 8 9 syl3anc 
 |-  ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) -> E. s e. ~P x E. u e. J ( y e. u /\ u C_ s /\ ( J |`t s ) e. A ) )
11 3 3ad2ant1 
 |-  ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) -> ( J |`t B ) e. Top )
12 11 3ad2ant1 
 |-  ( ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ s e. ~P x /\ ( u e. J /\ ( y e. u /\ u C_ s /\ ( J |`t s ) e. A ) ) ) -> ( J |`t B ) e. Top )
13 simp3l 
 |-  ( ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ s e. ~P x /\ ( u e. J /\ ( y e. u /\ u C_ s /\ ( J |`t s ) e. A ) ) ) -> u e. J )
14 simp3r2 
 |-  ( ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ s e. ~P x /\ ( u e. J /\ ( y e. u /\ u C_ s /\ ( J |`t s ) e. A ) ) ) -> u C_ s )
15 simp2 
 |-  ( ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ s e. ~P x /\ ( u e. J /\ ( y e. u /\ u C_ s /\ ( J |`t s ) e. A ) ) ) -> s e. ~P x )
16 15 elpwid 
 |-  ( ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ s e. ~P x /\ ( u e. J /\ ( y e. u /\ u C_ s /\ ( J |`t s ) e. A ) ) ) -> s C_ x )
17 simp12r 
 |-  ( ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ s e. ~P x /\ ( u e. J /\ ( y e. u /\ u C_ s /\ ( J |`t s ) e. A ) ) ) -> x C_ B )
18 16 17 sstrd 
 |-  ( ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ s e. ~P x /\ ( u e. J /\ ( y e. u /\ u C_ s /\ ( J |`t s ) e. A ) ) ) -> s C_ B )
19 14 18 sstrd 
 |-  ( ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ s e. ~P x /\ ( u e. J /\ ( y e. u /\ u C_ s /\ ( J |`t s ) e. A ) ) ) -> u C_ B )
20 6 3ad2ant1 
 |-  ( ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ s e. ~P x /\ ( u e. J /\ ( y e. u /\ u C_ s /\ ( J |`t s ) e. A ) ) ) -> J e. N-Locally A )
21 20 1 syl 
 |-  ( ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ s e. ~P x /\ ( u e. J /\ ( y e. u /\ u C_ s /\ ( J |`t s ) e. A ) ) ) -> J e. Top )
22 simp11r 
 |-  ( ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ s e. ~P x /\ ( u e. J /\ ( y e. u /\ u C_ s /\ ( J |`t s ) e. A ) ) ) -> B e. J )
23 restopn2 
 |-  ( ( J e. Top /\ B e. J ) -> ( u e. ( J |`t B ) <-> ( u e. J /\ u C_ B ) ) )
24 21 22 23 syl2anc 
 |-  ( ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ s e. ~P x /\ ( u e. J /\ ( y e. u /\ u C_ s /\ ( J |`t s ) e. A ) ) ) -> ( u e. ( J |`t B ) <-> ( u e. J /\ u C_ B ) ) )
25 13 19 24 mpbir2and 
 |-  ( ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ s e. ~P x /\ ( u e. J /\ ( y e. u /\ u C_ s /\ ( J |`t s ) e. A ) ) ) -> u e. ( J |`t B ) )
26 simp3r1 
 |-  ( ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ s e. ~P x /\ ( u e. J /\ ( y e. u /\ u C_ s /\ ( J |`t s ) e. A ) ) ) -> y e. u )
27 opnneip 
 |-  ( ( ( J |`t B ) e. Top /\ u e. ( J |`t B ) /\ y e. u ) -> u e. ( ( nei ` ( J |`t B ) ) ` { y } ) )
28 12 25 26 27 syl3anc 
 |-  ( ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ s e. ~P x /\ ( u e. J /\ ( y e. u /\ u C_ s /\ ( J |`t s ) e. A ) ) ) -> u e. ( ( nei ` ( J |`t B ) ) ` { y } ) )
29 elssuni 
 |-  ( B e. J -> B C_ U. J )
30 22 29 syl 
 |-  ( ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ s e. ~P x /\ ( u e. J /\ ( y e. u /\ u C_ s /\ ( J |`t s ) e. A ) ) ) -> B C_ U. J )
31 eqid 
 |-  U. J = U. J
32 31 restuni 
 |-  ( ( J e. Top /\ B C_ U. J ) -> B = U. ( J |`t B ) )
33 21 30 32 syl2anc 
 |-  ( ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ s e. ~P x /\ ( u e. J /\ ( y e. u /\ u C_ s /\ ( J |`t s ) e. A ) ) ) -> B = U. ( J |`t B ) )
34 18 33 sseqtrd 
 |-  ( ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ s e. ~P x /\ ( u e. J /\ ( y e. u /\ u C_ s /\ ( J |`t s ) e. A ) ) ) -> s C_ U. ( J |`t B ) )
35 eqid 
 |-  U. ( J |`t B ) = U. ( J |`t B )
36 35 ssnei2 
 |-  ( ( ( ( J |`t B ) e. Top /\ u e. ( ( nei ` ( J |`t B ) ) ` { y } ) ) /\ ( u C_ s /\ s C_ U. ( J |`t B ) ) ) -> s e. ( ( nei ` ( J |`t B ) ) ` { y } ) )
37 12 28 14 34 36 syl22anc 
 |-  ( ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ s e. ~P x /\ ( u e. J /\ ( y e. u /\ u C_ s /\ ( J |`t s ) e. A ) ) ) -> s e. ( ( nei ` ( J |`t B ) ) ` { y } ) )
38 37 15 elind 
 |-  ( ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ s e. ~P x /\ ( u e. J /\ ( y e. u /\ u C_ s /\ ( J |`t s ) e. A ) ) ) -> s e. ( ( ( nei ` ( J |`t B ) ) ` { y } ) i^i ~P x ) )
39 restabs 
 |-  ( ( J e. Top /\ s C_ B /\ B e. J ) -> ( ( J |`t B ) |`t s ) = ( J |`t s ) )
40 21 18 22 39 syl3anc 
 |-  ( ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ s e. ~P x /\ ( u e. J /\ ( y e. u /\ u C_ s /\ ( J |`t s ) e. A ) ) ) -> ( ( J |`t B ) |`t s ) = ( J |`t s ) )
41 simp3r3 
 |-  ( ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ s e. ~P x /\ ( u e. J /\ ( y e. u /\ u C_ s /\ ( J |`t s ) e. A ) ) ) -> ( J |`t s ) e. A )
42 40 41 eqeltrd 
 |-  ( ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ s e. ~P x /\ ( u e. J /\ ( y e. u /\ u C_ s /\ ( J |`t s ) e. A ) ) ) -> ( ( J |`t B ) |`t s ) e. A )
43 38 42 jca 
 |-  ( ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ s e. ~P x /\ ( u e. J /\ ( y e. u /\ u C_ s /\ ( J |`t s ) e. A ) ) ) -> ( s e. ( ( ( nei ` ( J |`t B ) ) ` { y } ) i^i ~P x ) /\ ( ( J |`t B ) |`t s ) e. A ) )
44 43 3expa 
 |-  ( ( ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ s e. ~P x ) /\ ( u e. J /\ ( y e. u /\ u C_ s /\ ( J |`t s ) e. A ) ) ) -> ( s e. ( ( ( nei ` ( J |`t B ) ) ` { y } ) i^i ~P x ) /\ ( ( J |`t B ) |`t s ) e. A ) )
45 44 rexlimdvaa 
 |-  ( ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ s e. ~P x ) -> ( E. u e. J ( y e. u /\ u C_ s /\ ( J |`t s ) e. A ) -> ( s e. ( ( ( nei ` ( J |`t B ) ) ` { y } ) i^i ~P x ) /\ ( ( J |`t B ) |`t s ) e. A ) ) )
46 45 expimpd 
 |-  ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) -> ( ( s e. ~P x /\ E. u e. J ( y e. u /\ u C_ s /\ ( J |`t s ) e. A ) ) -> ( s e. ( ( ( nei ` ( J |`t B ) ) ` { y } ) i^i ~P x ) /\ ( ( J |`t B ) |`t s ) e. A ) ) )
47 46 reximdv2 
 |-  ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) -> ( E. s e. ~P x E. u e. J ( y e. u /\ u C_ s /\ ( J |`t s ) e. A ) -> E. s e. ( ( ( nei ` ( J |`t B ) ) ` { y } ) i^i ~P x ) ( ( J |`t B ) |`t s ) e. A ) )
48 10 47 mpd 
 |-  ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) -> E. s e. ( ( ( nei ` ( J |`t B ) ) ` { y } ) i^i ~P x ) ( ( J |`t B ) |`t s ) e. A )
49 48 3expa 
 |-  ( ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) ) /\ y e. x ) -> E. s e. ( ( ( nei ` ( J |`t B ) ) ` { y } ) i^i ~P x ) ( ( J |`t B ) |`t s ) e. A )
50 49 ralrimiva 
 |-  ( ( ( J e. N-Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) ) -> A. y e. x E. s e. ( ( ( nei ` ( J |`t B ) ) ` { y } ) i^i ~P x ) ( ( J |`t B ) |`t s ) e. A )
51 50 ex 
 |-  ( ( J e. N-Locally A /\ B e. J ) -> ( ( x e. J /\ x C_ B ) -> A. y e. x E. s e. ( ( ( nei ` ( J |`t B ) ) ` { y } ) i^i ~P x ) ( ( J |`t B ) |`t s ) e. A ) )
52 5 51 sylbid 
 |-  ( ( J e. N-Locally A /\ B e. J ) -> ( x e. ( J |`t B ) -> A. y e. x E. s e. ( ( ( nei ` ( J |`t B ) ) ` { y } ) i^i ~P x ) ( ( J |`t B ) |`t s ) e. A ) )
53 52 ralrimiv 
 |-  ( ( J e. N-Locally A /\ B e. J ) -> A. x e. ( J |`t B ) A. y e. x E. s e. ( ( ( nei ` ( J |`t B ) ) ` { y } ) i^i ~P x ) ( ( J |`t B ) |`t s ) e. A )
54 isnlly 
 |-  ( ( J |`t B ) e. N-Locally A <-> ( ( J |`t B ) e. Top /\ A. x e. ( J |`t B ) A. y e. x E. s e. ( ( ( nei ` ( J |`t B ) ) ` { y } ) i^i ~P x ) ( ( J |`t B ) |`t s ) e. A ) )
55 3 53 54 sylanbrc 
 |-  ( ( J e. N-Locally A /\ B e. J ) -> ( J |`t B ) e. N-Locally A )