Metamath Proof Explorer

Theorem llyrest

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

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

Proof

Step Hyp Ref Expression
1 llytop 
 |-  ( J e. Locally A -> J e. Top )
2 resttop 
 |-  ( ( J e. Top /\ B e. J ) -> ( J |`t B ) e. Top )
3 1 2 sylan 
 |-  ( ( J e. 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. Locally A /\ B e. J ) -> ( x e. ( J |`t B ) <-> ( x e. J /\ x C_ B ) ) )
6 simp1l 
 |-  ( ( ( J e. Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) -> J e. Locally A )
7 simp2l 
 |-  ( ( ( J e. Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) -> x e. J )
8 simp3 
 |-  ( ( ( J e. Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) -> y e. x )
9 llyi 
 |-  ( ( J e. Locally A /\ x e. J /\ y e. x ) -> E. v e. J ( v C_ x /\ y e. v /\ ( J |`t v ) e. A ) )
10 6 7 8 9 syl3anc 
 |-  ( ( ( J e. Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) -> E. v e. J ( v C_ x /\ y e. v /\ ( J |`t v ) e. A ) )
11 simprl 
 |-  ( ( ( ( J e. Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ ( v e. J /\ ( v C_ x /\ y e. v /\ ( J |`t v ) e. A ) ) ) -> v e. J )
12 simprr1 
 |-  ( ( ( ( J e. Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ ( v e. J /\ ( v C_ x /\ y e. v /\ ( J |`t v ) e. A ) ) ) -> v C_ x )
13 simpl2r 
 |-  ( ( ( ( J e. Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ ( v e. J /\ ( v C_ x /\ y e. v /\ ( J |`t v ) e. A ) ) ) -> x C_ B )
14 12 13 sstrd 
 |-  ( ( ( ( J e. Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ ( v e. J /\ ( v C_ x /\ y e. v /\ ( J |`t v ) e. A ) ) ) -> v C_ B )
15 6 1 syl 
 |-  ( ( ( J e. Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) -> J e. Top )
16 15 adantr 
 |-  ( ( ( ( J e. Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ ( v e. J /\ ( v C_ x /\ y e. v /\ ( J |`t v ) e. A ) ) ) -> J e. Top )
17 simpl1r 
 |-  ( ( ( ( J e. Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ ( v e. J /\ ( v C_ x /\ y e. v /\ ( J |`t v ) e. A ) ) ) -> B e. J )
18 restopn2 
 |-  ( ( J e. Top /\ B e. J ) -> ( v e. ( J |`t B ) <-> ( v e. J /\ v C_ B ) ) )
19 16 17 18 syl2anc 
 |-  ( ( ( ( J e. Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ ( v e. J /\ ( v C_ x /\ y e. v /\ ( J |`t v ) e. A ) ) ) -> ( v e. ( J |`t B ) <-> ( v e. J /\ v C_ B ) ) )
20 11 14 19 mpbir2and 
 |-  ( ( ( ( J e. Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ ( v e. J /\ ( v C_ x /\ y e. v /\ ( J |`t v ) e. A ) ) ) -> v e. ( J |`t B ) )
21 velpw 
 |-  ( v e. ~P x <-> v C_ x )
22 12 21 sylibr 
 |-  ( ( ( ( J e. Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ ( v e. J /\ ( v C_ x /\ y e. v /\ ( J |`t v ) e. A ) ) ) -> v e. ~P x )
23 20 22 elind 
 |-  ( ( ( ( J e. Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ ( v e. J /\ ( v C_ x /\ y e. v /\ ( J |`t v ) e. A ) ) ) -> v e. ( ( J |`t B ) i^i ~P x ) )
24 simprr2 
 |-  ( ( ( ( J e. Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ ( v e. J /\ ( v C_ x /\ y e. v /\ ( J |`t v ) e. A ) ) ) -> y e. v )
25 restabs 
 |-  ( ( J e. Top /\ v C_ B /\ B e. J ) -> ( ( J |`t B ) |`t v ) = ( J |`t v ) )
26 16 14 17 25 syl3anc 
 |-  ( ( ( ( J e. Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ ( v e. J /\ ( v C_ x /\ y e. v /\ ( J |`t v ) e. A ) ) ) -> ( ( J |`t B ) |`t v ) = ( J |`t v ) )
27 simprr3 
 |-  ( ( ( ( J e. Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ ( v e. J /\ ( v C_ x /\ y e. v /\ ( J |`t v ) e. A ) ) ) -> ( J |`t v ) e. A )
28 26 27 eqeltrd 
 |-  ( ( ( ( J e. Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ ( v e. J /\ ( v C_ x /\ y e. v /\ ( J |`t v ) e. A ) ) ) -> ( ( J |`t B ) |`t v ) e. A )
29 23 24 28 jca32 
 |-  ( ( ( ( J e. Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) /\ ( v e. J /\ ( v C_ x /\ y e. v /\ ( J |`t v ) e. A ) ) ) -> ( v e. ( ( J |`t B ) i^i ~P x ) /\ ( y e. v /\ ( ( J |`t B ) |`t v ) e. A ) ) )
30 29 ex 
 |-  ( ( ( J e. Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) -> ( ( v e. J /\ ( v C_ x /\ y e. v /\ ( J |`t v ) e. A ) ) -> ( v e. ( ( J |`t B ) i^i ~P x ) /\ ( y e. v /\ ( ( J |`t B ) |`t v ) e. A ) ) ) )
31 30 reximdv2 
 |-  ( ( ( J e. Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) -> ( E. v e. J ( v C_ x /\ y e. v /\ ( J |`t v ) e. A ) -> E. v e. ( ( J |`t B ) i^i ~P x ) ( y e. v /\ ( ( J |`t B ) |`t v ) e. A ) ) )
32 10 31 mpd 
 |-  ( ( ( J e. Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) /\ y e. x ) -> E. v e. ( ( J |`t B ) i^i ~P x ) ( y e. v /\ ( ( J |`t B ) |`t v ) e. A ) )
33 32 3expa 
 |-  ( ( ( ( J e. Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) ) /\ y e. x ) -> E. v e. ( ( J |`t B ) i^i ~P x ) ( y e. v /\ ( ( J |`t B ) |`t v ) e. A ) )
34 33 ralrimiva 
 |-  ( ( ( J e. Locally A /\ B e. J ) /\ ( x e. J /\ x C_ B ) ) -> A. y e. x E. v e. ( ( J |`t B ) i^i ~P x ) ( y e. v /\ ( ( J |`t B ) |`t v ) e. A ) )
35 34 ex 
 |-  ( ( J e. Locally A /\ B e. J ) -> ( ( x e. J /\ x C_ B ) -> A. y e. x E. v e. ( ( J |`t B ) i^i ~P x ) ( y e. v /\ ( ( J |`t B ) |`t v ) e. A ) ) )
36 5 35 sylbid 
 |-  ( ( J e. Locally A /\ B e. J ) -> ( x e. ( J |`t B ) -> A. y e. x E. v e. ( ( J |`t B ) i^i ~P x ) ( y e. v /\ ( ( J |`t B ) |`t v ) e. A ) ) )
37 36 ralrimiv 
 |-  ( ( J e. Locally A /\ B e. J ) -> A. x e. ( J |`t B ) A. y e. x E. v e. ( ( J |`t B ) i^i ~P x ) ( y e. v /\ ( ( J |`t B ) |`t v ) e. A ) )
38 islly 
 |-  ( ( J |`t B ) e. Locally A <-> ( ( J |`t B ) e. Top /\ A. x e. ( J |`t B ) A. y e. x E. v e. ( ( J |`t B ) i^i ~P x ) ( y e. v /\ ( ( J |`t B ) |`t v ) e. A ) ) )
39 3 37 38 sylanbrc 
 |-  ( ( J e. Locally A /\ B e. J ) -> ( J |`t B ) e. Locally A )