This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem restlly

Description: If the property A passes to open subspaces, then a space which is A is also locally A . (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Hypotheses restlly.1 
|- ( ( ph /\ ( j e. A /\ x e. j ) ) -> ( j |`t x ) e. A )
restlly.2 
|- ( ph -> A C_ Top )
Assertion restlly 
|- ( ph -> A C_ Locally A )

Proof

Step Hyp Ref Expression
1 restlly.1 
 |-  ( ( ph /\ ( j e. A /\ x e. j ) ) -> ( j |`t x ) e. A )
2 restlly.2 
 |-  ( ph -> A C_ Top )
3 2 sselda 
 |-  ( ( ph /\ j e. A ) -> j e. Top )
4 simprl 
 |-  ( ( ( ph /\ j e. A ) /\ ( x e. j /\ y e. x ) ) -> x e. j )
5 vex 
 |-  x e. _V
6 5 pwid 
 |-  x e. ~P x
7 6 a1i 
 |-  ( ( ( ph /\ j e. A ) /\ ( x e. j /\ y e. x ) ) -> x e. ~P x )
8 4 7 elind 
 |-  ( ( ( ph /\ j e. A ) /\ ( x e. j /\ y e. x ) ) -> x e. ( j i^i ~P x ) )
9 simprr 
 |-  ( ( ( ph /\ j e. A ) /\ ( x e. j /\ y e. x ) ) -> y e. x )
10 1 anassrs 
 |-  ( ( ( ph /\ j e. A ) /\ x e. j ) -> ( j |`t x ) e. A )
11 10 adantrr 
 |-  ( ( ( ph /\ j e. A ) /\ ( x e. j /\ y e. x ) ) -> ( j |`t x ) e. A )
12 elequ2 
 |-  ( u = x -> ( y e. u <-> y e. x ) )
13 oveq2 
 |-  ( u = x -> ( j |`t u ) = ( j |`t x ) )
14 13 eleq1d 
 |-  ( u = x -> ( ( j |`t u ) e. A <-> ( j |`t x ) e. A ) )
15 12 14 anbi12d 
 |-  ( u = x -> ( ( y e. u /\ ( j |`t u ) e. A ) <-> ( y e. x /\ ( j |`t x ) e. A ) ) )
16 15 rspcev 
 |-  ( ( x e. ( j i^i ~P x ) /\ ( y e. x /\ ( j |`t x ) e. A ) ) -> E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. A ) )
17 8 9 11 16 syl12anc 
 |-  ( ( ( ph /\ j e. A ) /\ ( x e. j /\ y e. x ) ) -> E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. A ) )
18 17 ralrimivva 
 |-  ( ( ph /\ j e. A ) -> A. x e. j A. y e. x E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. A ) )
19 islly 
 |-  ( j e. Locally A <-> ( j e. Top /\ A. x e. j A. y e. x E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. A ) ) )
20 3 18 19 sylanbrc 
 |-  ( ( ph /\ j e. A ) -> j e. Locally A )
21 20 ex 
 |-  ( ph -> ( j e. A -> j e. Locally A ) )
22 21 ssrdv 
 |-  ( ph -> A C_ Locally A )