Metamath Proof Explorer

Theorem restnlly

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

Ref Expression
Hypothesis restlly.1 
|- ( ( ph /\ ( j e. A /\ x e. j ) ) -> ( j |`t x ) e. A )
Assertion restnlly 
|- ( ph -> N-Locally A = Locally A )

Proof

Step Hyp Ref Expression
1 restlly.1 
 |-  ( ( ph /\ ( j e. A /\ x e. j ) ) -> ( j |`t x ) e. A )
2 nllytop 
 |-  ( k e. N-Locally A -> k e. Top )
3 2 adantl 
 |-  ( ( ph /\ k e. N-Locally A ) -> k e. Top )
4 nlly2i 
 |-  ( ( k e. N-Locally A /\ y e. k /\ u e. y ) -> E. s e. ~P y E. x e. k ( u e. x /\ x C_ s /\ ( k |`t s ) e. A ) )
5 4 3adant1l 
 |-  ( ( ( ph /\ k e. N-Locally A ) /\ y e. k /\ u e. y ) -> E. s e. ~P y E. x e. k ( u e. x /\ x C_ s /\ ( k |`t s ) e. A ) )
6 simprl 
 |-  ( ( ( ( ( ph /\ k e. N-Locally A ) /\ y e. k /\ u e. y ) /\ s e. ~P y ) /\ ( x e. k /\ ( u e. x /\ x C_ s /\ ( k |`t s ) e. A ) ) ) -> x e. k )
7 simprr2 
 |-  ( ( ( ( ( ph /\ k e. N-Locally A ) /\ y e. k /\ u e. y ) /\ s e. ~P y ) /\ ( x e. k /\ ( u e. x /\ x C_ s /\ ( k |`t s ) e. A ) ) ) -> x C_ s )
8 simplr 
 |-  ( ( ( ( ( ph /\ k e. N-Locally A ) /\ y e. k /\ u e. y ) /\ s e. ~P y ) /\ ( x e. k /\ ( u e. x /\ x C_ s /\ ( k |`t s ) e. A ) ) ) -> s e. ~P y )
9 8 elpwid 
 |-  ( ( ( ( ( ph /\ k e. N-Locally A ) /\ y e. k /\ u e. y ) /\ s e. ~P y ) /\ ( x e. k /\ ( u e. x /\ x C_ s /\ ( k |`t s ) e. A ) ) ) -> s C_ y )
10 7 9 sstrd 
 |-  ( ( ( ( ( ph /\ k e. N-Locally A ) /\ y e. k /\ u e. y ) /\ s e. ~P y ) /\ ( x e. k /\ ( u e. x /\ x C_ s /\ ( k |`t s ) e. A ) ) ) -> x C_ y )
11 velpw 
 |-  ( x e. ~P y <-> x C_ y )
12 10 11 sylibr 
 |-  ( ( ( ( ( ph /\ k e. N-Locally A ) /\ y e. k /\ u e. y ) /\ s e. ~P y ) /\ ( x e. k /\ ( u e. x /\ x C_ s /\ ( k |`t s ) e. A ) ) ) -> x e. ~P y )
13 6 12 elind 
 |-  ( ( ( ( ( ph /\ k e. N-Locally A ) /\ y e. k /\ u e. y ) /\ s e. ~P y ) /\ ( x e. k /\ ( u e. x /\ x C_ s /\ ( k |`t s ) e. A ) ) ) -> x e. ( k i^i ~P y ) )
14 simprr1 
 |-  ( ( ( ( ( ph /\ k e. N-Locally A ) /\ y e. k /\ u e. y ) /\ s e. ~P y ) /\ ( x e. k /\ ( u e. x /\ x C_ s /\ ( k |`t s ) e. A ) ) ) -> u e. x )
15 simpll1 
 |-  ( ( ( ( ( ph /\ k e. N-Locally A ) /\ y e. k /\ u e. y ) /\ s e. ~P y ) /\ ( x e. k /\ ( u e. x /\ x C_ s /\ ( k |`t s ) e. A ) ) ) -> ( ph /\ k e. N-Locally A ) )
16 15 2 simpl2im 
 |-  ( ( ( ( ( ph /\ k e. N-Locally A ) /\ y e. k /\ u e. y ) /\ s e. ~P y ) /\ ( x e. k /\ ( u e. x /\ x C_ s /\ ( k |`t s ) e. A ) ) ) -> k e. Top )
17 restabs 
 |-  ( ( k e. Top /\ x C_ s /\ s e. ~P y ) -> ( ( k |`t s ) |`t x ) = ( k |`t x ) )
18 16 7 8 17 syl3anc 
 |-  ( ( ( ( ( ph /\ k e. N-Locally A ) /\ y e. k /\ u e. y ) /\ s e. ~P y ) /\ ( x e. k /\ ( u e. x /\ x C_ s /\ ( k |`t s ) e. A ) ) ) -> ( ( k |`t s ) |`t x ) = ( k |`t x ) )
19 df-ss 
 |-  ( x C_ s <-> ( x i^i s ) = x )
20 7 19 sylib 
 |-  ( ( ( ( ( ph /\ k e. N-Locally A ) /\ y e. k /\ u e. y ) /\ s e. ~P y ) /\ ( x e. k /\ ( u e. x /\ x C_ s /\ ( k |`t s ) e. A ) ) ) -> ( x i^i s ) = x )
21 elrestr 
 |-  ( ( k e. Top /\ s e. ~P y /\ x e. k ) -> ( x i^i s ) e. ( k |`t s ) )
22 16 8 6 21 syl3anc 
 |-  ( ( ( ( ( ph /\ k e. N-Locally A ) /\ y e. k /\ u e. y ) /\ s e. ~P y ) /\ ( x e. k /\ ( u e. x /\ x C_ s /\ ( k |`t s ) e. A ) ) ) -> ( x i^i s ) e. ( k |`t s ) )
23 20 22 eqeltrrd 
 |-  ( ( ( ( ( ph /\ k e. N-Locally A ) /\ y e. k /\ u e. y ) /\ s e. ~P y ) /\ ( x e. k /\ ( u e. x /\ x C_ s /\ ( k |`t s ) e. A ) ) ) -> x e. ( k |`t s ) )
24 eleq2 
 |-  ( j = ( k |`t s ) -> ( x e. j <-> x e. ( k |`t s ) ) )
25 oveq1 
 |-  ( j = ( k |`t s ) -> ( j |`t x ) = ( ( k |`t s ) |`t x ) )
26 25 eleq1d 
 |-  ( j = ( k |`t s ) -> ( ( j |`t x ) e. A <-> ( ( k |`t s ) |`t x ) e. A ) )
27 24 26 imbi12d 
 |-  ( j = ( k |`t s ) -> ( ( x e. j -> ( j |`t x ) e. A ) <-> ( x e. ( k |`t s ) -> ( ( k |`t s ) |`t x ) e. A ) ) )
28 15 simpld 
 |-  ( ( ( ( ( ph /\ k e. N-Locally A ) /\ y e. k /\ u e. y ) /\ s e. ~P y ) /\ ( x e. k /\ ( u e. x /\ x C_ s /\ ( k |`t s ) e. A ) ) ) -> ph )
29 1 expr 
 |-  ( ( ph /\ j e. A ) -> ( x e. j -> ( j |`t x ) e. A ) )
30 29 ralrimiva 
 |-  ( ph -> A. j e. A ( x e. j -> ( j |`t x ) e. A ) )
31 28 30 syl 
 |-  ( ( ( ( ( ph /\ k e. N-Locally A ) /\ y e. k /\ u e. y ) /\ s e. ~P y ) /\ ( x e. k /\ ( u e. x /\ x C_ s /\ ( k |`t s ) e. A ) ) ) -> A. j e. A ( x e. j -> ( j |`t x ) e. A ) )
32 simprr3 
 |-  ( ( ( ( ( ph /\ k e. N-Locally A ) /\ y e. k /\ u e. y ) /\ s e. ~P y ) /\ ( x e. k /\ ( u e. x /\ x C_ s /\ ( k |`t s ) e. A ) ) ) -> ( k |`t s ) e. A )
33 27 31 32 rspcdva 
 |-  ( ( ( ( ( ph /\ k e. N-Locally A ) /\ y e. k /\ u e. y ) /\ s e. ~P y ) /\ ( x e. k /\ ( u e. x /\ x C_ s /\ ( k |`t s ) e. A ) ) ) -> ( x e. ( k |`t s ) -> ( ( k |`t s ) |`t x ) e. A ) )
34 23 33 mpd 
 |-  ( ( ( ( ( ph /\ k e. N-Locally A ) /\ y e. k /\ u e. y ) /\ s e. ~P y ) /\ ( x e. k /\ ( u e. x /\ x C_ s /\ ( k |`t s ) e. A ) ) ) -> ( ( k |`t s ) |`t x ) e. A )
35 18 34 eqeltrrd 
 |-  ( ( ( ( ( ph /\ k e. N-Locally A ) /\ y e. k /\ u e. y ) /\ s e. ~P y ) /\ ( x e. k /\ ( u e. x /\ x C_ s /\ ( k |`t s ) e. A ) ) ) -> ( k |`t x ) e. A )
36 13 14 35 jca32 
 |-  ( ( ( ( ( ph /\ k e. N-Locally A ) /\ y e. k /\ u e. y ) /\ s e. ~P y ) /\ ( x e. k /\ ( u e. x /\ x C_ s /\ ( k |`t s ) e. A ) ) ) -> ( x e. ( k i^i ~P y ) /\ ( u e. x /\ ( k |`t x ) e. A ) ) )
37 36 ex 
 |-  ( ( ( ( ph /\ k e. N-Locally A ) /\ y e. k /\ u e. y ) /\ s e. ~P y ) -> ( ( x e. k /\ ( u e. x /\ x C_ s /\ ( k |`t s ) e. A ) ) -> ( x e. ( k i^i ~P y ) /\ ( u e. x /\ ( k |`t x ) e. A ) ) ) )
38 37 reximdv2 
 |-  ( ( ( ( ph /\ k e. N-Locally A ) /\ y e. k /\ u e. y ) /\ s e. ~P y ) -> ( E. x e. k ( u e. x /\ x C_ s /\ ( k |`t s ) e. A ) -> E. x e. ( k i^i ~P y ) ( u e. x /\ ( k |`t x ) e. A ) ) )
39 38 rexlimdva 
 |-  ( ( ( ph /\ k e. N-Locally A ) /\ y e. k /\ u e. y ) -> ( E. s e. ~P y E. x e. k ( u e. x /\ x C_ s /\ ( k |`t s ) e. A ) -> E. x e. ( k i^i ~P y ) ( u e. x /\ ( k |`t x ) e. A ) ) )
40 5 39 mpd 
 |-  ( ( ( ph /\ k e. N-Locally A ) /\ y e. k /\ u e. y ) -> E. x e. ( k i^i ~P y ) ( u e. x /\ ( k |`t x ) e. A ) )
41 40 3expb 
 |-  ( ( ( ph /\ k e. N-Locally A ) /\ ( y e. k /\ u e. y ) ) -> E. x e. ( k i^i ~P y ) ( u e. x /\ ( k |`t x ) e. A ) )
42 41 ralrimivva 
 |-  ( ( ph /\ k e. N-Locally A ) -> A. y e. k A. u e. y E. x e. ( k i^i ~P y ) ( u e. x /\ ( k |`t x ) e. A ) )
43 islly 
 |-  ( k e. Locally A <-> ( k e. Top /\ A. y e. k A. u e. y E. x e. ( k i^i ~P y ) ( u e. x /\ ( k |`t x ) e. A ) ) )
44 3 42 43 sylanbrc 
 |-  ( ( ph /\ k e. N-Locally A ) -> k e. Locally A )
45 44 ex 
 |-  ( ph -> ( k e. N-Locally A -> k e. Locally A ) )
46 45 ssrdv 
 |-  ( ph -> N-Locally A C_ Locally A )
47 llyssnlly 
 |-  Locally A C_ N-Locally A
48 47 a1i 
 |-  ( ph -> Locally A C_ N-Locally A )
49 46 48 eqssd 
 |-  ( ph -> N-Locally A = Locally A )