Metamath Proof Explorer

Theorem islly2

Description: An alternative expression for J e. Locally A when A passes to open subspaces: A space is locally A if every point is contained in an open neighborhood with property 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 )
islly2.2 
|- X = U. J
Assertion islly2 
|- ( ph -> ( J e. Locally A <-> ( J e. Top /\ A. y e. X E. u e. J ( y e. u /\ ( J |`t u ) e. A ) ) ) )

Proof

Step Hyp Ref Expression
1 restlly.1 
 |-  ( ( ph /\ ( j e. A /\ x e. j ) ) -> ( j |`t x ) e. A )
2 islly2.2 
 |-  X = U. J
3 llytop 
 |-  ( J e. Locally A -> J e. Top )
4 3 adantl 
 |-  ( ( ph /\ J e. Locally A ) -> J e. Top )
5 simplr 
 |-  ( ( ( ph /\ J e. Locally A ) /\ y e. X ) -> J e. Locally A )
6 4 adantr 
 |-  ( ( ( ph /\ J e. Locally A ) /\ y e. X ) -> J e. Top )
7 2 topopn 
 |-  ( J e. Top -> X e. J )
8 6 7 syl 
 |-  ( ( ( ph /\ J e. Locally A ) /\ y e. X ) -> X e. J )
9 simpr 
 |-  ( ( ( ph /\ J e. Locally A ) /\ y e. X ) -> y e. X )
10 llyi 
 |-  ( ( J e. Locally A /\ X e. J /\ y e. X ) -> E. u e. J ( u C_ X /\ y e. u /\ ( J |`t u ) e. A ) )
11 5 8 9 10 syl3anc 
 |-  ( ( ( ph /\ J e. Locally A ) /\ y e. X ) -> E. u e. J ( u C_ X /\ y e. u /\ ( J |`t u ) e. A ) )
12 3simpc 
 |-  ( ( u C_ X /\ y e. u /\ ( J |`t u ) e. A ) -> ( y e. u /\ ( J |`t u ) e. A ) )
13 12 reximi 
 |-  ( E. u e. J ( u C_ X /\ y e. u /\ ( J |`t u ) e. A ) -> E. u e. J ( y e. u /\ ( J |`t u ) e. A ) )
14 11 13 syl 
 |-  ( ( ( ph /\ J e. Locally A ) /\ y e. X ) -> E. u e. J ( y e. u /\ ( J |`t u ) e. A ) )
15 14 ralrimiva 
 |-  ( ( ph /\ J e. Locally A ) -> A. y e. X E. u e. J ( y e. u /\ ( J |`t u ) e. A ) )
16 4 15 jca 
 |-  ( ( ph /\ J e. Locally A ) -> ( J e. Top /\ A. y e. X E. u e. J ( y e. u /\ ( J |`t u ) e. A ) ) )
17 simprl 
 |-  ( ( ph /\ ( J e. Top /\ A. y e. X E. u e. J ( y e. u /\ ( J |`t u ) e. A ) ) ) -> J e. Top )
18 elssuni 
 |-  ( z e. J -> z C_ U. J )
19 18 2 sseqtrrdi 
 |-  ( z e. J -> z C_ X )
20 19 adantl 
 |-  ( ( ( ph /\ J e. Top ) /\ z e. J ) -> z C_ X )
21 ssralv 
 |-  ( z C_ X -> ( A. y e. X E. u e. J ( y e. u /\ ( J |`t u ) e. A ) -> A. y e. z E. u e. J ( y e. u /\ ( J |`t u ) e. A ) ) )
22 20 21 syl 
 |-  ( ( ( ph /\ J e. Top ) /\ z e. J ) -> ( A. y e. X E. u e. J ( y e. u /\ ( J |`t u ) e. A ) -> A. y e. z E. u e. J ( y e. u /\ ( J |`t u ) e. A ) ) )
23 simpllr 
 |-  ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J |`t u ) e. A ) ) ) -> J e. Top )
24 simplrl 
 |-  ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J |`t u ) e. A ) ) ) -> z e. J )
25 simprl 
 |-  ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J |`t u ) e. A ) ) ) -> u e. J )
26 inopn 
 |-  ( ( J e. Top /\ z e. J /\ u e. J ) -> ( z i^i u ) e. J )
27 23 24 25 26 syl3anc 
 |-  ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J |`t u ) e. A ) ) ) -> ( z i^i u ) e. J )
28 vex 
 |-  z e. _V
29 inss1 
 |-  ( z i^i u ) C_ z
30 28 29 elpwi2 
 |-  ( z i^i u ) e. ~P z
31 30 a1i 
 |-  ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J |`t u ) e. A ) ) ) -> ( z i^i u ) e. ~P z )
32 27 31 elind 
 |-  ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J |`t u ) e. A ) ) ) -> ( z i^i u ) e. ( J i^i ~P z ) )
33 simplrr 
 |-  ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J |`t u ) e. A ) ) ) -> y e. z )
34 simprrl 
 |-  ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J |`t u ) e. A ) ) ) -> y e. u )
35 33 34 elind 
 |-  ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J |`t u ) e. A ) ) ) -> y e. ( z i^i u ) )
36 inss2 
 |-  ( z i^i u ) C_ u
37 36 a1i 
 |-  ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J |`t u ) e. A ) ) ) -> ( z i^i u ) C_ u )
38 restabs 
 |-  ( ( J e. Top /\ ( z i^i u ) C_ u /\ u e. J ) -> ( ( J |`t u ) |`t ( z i^i u ) ) = ( J |`t ( z i^i u ) ) )
39 23 37 25 38 syl3anc 
 |-  ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J |`t u ) e. A ) ) ) -> ( ( J |`t u ) |`t ( z i^i u ) ) = ( J |`t ( z i^i u ) ) )
40 oveq2 
 |-  ( x = ( z i^i u ) -> ( ( J |`t u ) |`t x ) = ( ( J |`t u ) |`t ( z i^i u ) ) )
41 40 eleq1d 
 |-  ( x = ( z i^i u ) -> ( ( ( J |`t u ) |`t x ) e. A <-> ( ( J |`t u ) |`t ( z i^i u ) ) e. A ) )
42 oveq1 
 |-  ( j = ( J |`t u ) -> ( j |`t x ) = ( ( J |`t u ) |`t x ) )
43 42 eleq1d 
 |-  ( j = ( J |`t u ) -> ( ( j |`t x ) e. A <-> ( ( J |`t u ) |`t x ) e. A ) )
44 43 raleqbi1dv 
 |-  ( j = ( J |`t u ) -> ( A. x e. j ( j |`t x ) e. A <-> A. x e. ( J |`t u ) ( ( J |`t u ) |`t x ) e. A ) )
45 1 ralrimivva 
 |-  ( ph -> A. j e. A A. x e. j ( j |`t x ) e. A )
46 45 ad3antrrr 
 |-  ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J |`t u ) e. A ) ) ) -> A. j e. A A. x e. j ( j |`t x ) e. A )
47 simprrr 
 |-  ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J |`t u ) e. A ) ) ) -> ( J |`t u ) e. A )
48 44 46 47 rspcdva 
 |-  ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J |`t u ) e. A ) ) ) -> A. x e. ( J |`t u ) ( ( J |`t u ) |`t x ) e. A )
49 elrestr 
 |-  ( ( J e. Top /\ u e. J /\ z e. J ) -> ( z i^i u ) e. ( J |`t u ) )
50 23 25 24 49 syl3anc 
 |-  ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J |`t u ) e. A ) ) ) -> ( z i^i u ) e. ( J |`t u ) )
51 41 48 50 rspcdva 
 |-  ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J |`t u ) e. A ) ) ) -> ( ( J |`t u ) |`t ( z i^i u ) ) e. A )
52 39 51 eqeltrrd 
 |-  ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J |`t u ) e. A ) ) ) -> ( J |`t ( z i^i u ) ) e. A )
53 eleq2 
 |-  ( v = ( z i^i u ) -> ( y e. v <-> y e. ( z i^i u ) ) )
54 oveq2 
 |-  ( v = ( z i^i u ) -> ( J |`t v ) = ( J |`t ( z i^i u ) ) )
55 54 eleq1d 
 |-  ( v = ( z i^i u ) -> ( ( J |`t v ) e. A <-> ( J |`t ( z i^i u ) ) e. A ) )
56 53 55 anbi12d 
 |-  ( v = ( z i^i u ) -> ( ( y e. v /\ ( J |`t v ) e. A ) <-> ( y e. ( z i^i u ) /\ ( J |`t ( z i^i u ) ) e. A ) ) )
57 56 rspcev 
 |-  ( ( ( z i^i u ) e. ( J i^i ~P z ) /\ ( y e. ( z i^i u ) /\ ( J |`t ( z i^i u ) ) e. A ) ) -> E. v e. ( J i^i ~P z ) ( y e. v /\ ( J |`t v ) e. A ) )
58 32 35 52 57 syl12anc 
 |-  ( ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) /\ ( u e. J /\ ( y e. u /\ ( J |`t u ) e. A ) ) ) -> E. v e. ( J i^i ~P z ) ( y e. v /\ ( J |`t v ) e. A ) )
59 58 rexlimdvaa 
 |-  ( ( ( ph /\ J e. Top ) /\ ( z e. J /\ y e. z ) ) -> ( E. u e. J ( y e. u /\ ( J |`t u ) e. A ) -> E. v e. ( J i^i ~P z ) ( y e. v /\ ( J |`t v ) e. A ) ) )
60 59 anassrs 
 |-  ( ( ( ( ph /\ J e. Top ) /\ z e. J ) /\ y e. z ) -> ( E. u e. J ( y e. u /\ ( J |`t u ) e. A ) -> E. v e. ( J i^i ~P z ) ( y e. v /\ ( J |`t v ) e. A ) ) )
61 60 ralimdva 
 |-  ( ( ( ph /\ J e. Top ) /\ z e. J ) -> ( A. y e. z E. u e. J ( y e. u /\ ( J |`t u ) e. A ) -> A. y e. z E. v e. ( J i^i ~P z ) ( y e. v /\ ( J |`t v ) e. A ) ) )
62 22 61 syld 
 |-  ( ( ( ph /\ J e. Top ) /\ z e. J ) -> ( A. y e. X E. u e. J ( y e. u /\ ( J |`t u ) e. A ) -> A. y e. z E. v e. ( J i^i ~P z ) ( y e. v /\ ( J |`t v ) e. A ) ) )
63 62 ralrimdva 
 |-  ( ( ph /\ J e. Top ) -> ( A. y e. X E. u e. J ( y e. u /\ ( J |`t u ) e. A ) -> A. z e. J A. y e. z E. v e. ( J i^i ~P z ) ( y e. v /\ ( J |`t v ) e. A ) ) )
64 63 impr 
 |-  ( ( ph /\ ( J e. Top /\ A. y e. X E. u e. J ( y e. u /\ ( J |`t u ) e. A ) ) ) -> A. z e. J A. y e. z E. v e. ( J i^i ~P z ) ( y e. v /\ ( J |`t v ) e. A ) )
65 islly 
 |-  ( J e. Locally A <-> ( J e. Top /\ A. z e. J A. y e. z E. v e. ( J i^i ~P z ) ( y e. v /\ ( J |`t v ) e. A ) ) )
66 17 64 65 sylanbrc 
 |-  ( ( ph /\ ( J e. Top /\ A. y e. X E. u e. J ( y e. u /\ ( J |`t u ) e. A ) ) ) -> J e. Locally A )
67 16 66 impbida 
 |-  ( ph -> ( J e. Locally A <-> ( J e. Top /\ A. y e. X E. u e. J ( y e. u /\ ( J |`t u ) e. A ) ) ) )