Metamath Proof Explorer

Theorem cnllysconn

Description: The topology of the complex numbers is locally simply connected. (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Hypothesis cnllysconn.j 
|- J = ( TopOpen ` CCfld )
Assertion cnllysconn 
|- J e. Locally SConn

Proof

Step Hyp Ref Expression
1 cnllysconn.j 
 |-  J = ( TopOpen ` CCfld )
2 1 cnfldtop 
 |-  J e. Top
3 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
4 1 cnfldtopn 
 |-  J = ( MetOpen ` ( abs o. - ) )
5 4 mopni2 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ x e. J /\ y e. x ) -> E. r e. RR+ ( y ( ball ` ( abs o. - ) ) r ) C_ x )
6 3 5 mp3an1 
 |-  ( ( x e. J /\ y e. x ) -> E. r e. RR+ ( y ( ball ` ( abs o. - ) ) r ) C_ x )
7 3 a1i 
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> ( abs o. - ) e. ( *Met ` CC ) )
8 1 cnfldtopon 
 |-  J e. ( TopOn ` CC )
9 simpll 
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> x e. J )
10 toponss 
 |-  ( ( J e. ( TopOn ` CC ) /\ x e. J ) -> x C_ CC )
11 8 9 10 sylancr 
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> x C_ CC )
12 simplr 
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> y e. x )
13 11 12 sseldd 
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> y e. CC )
14 rpxr 
 |-  ( r e. RR+ -> r e. RR* )
15 14 ad2antrl 
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> r e. RR* )
16 4 blopn 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ y e. CC /\ r e. RR* ) -> ( y ( ball ` ( abs o. - ) ) r ) e. J )
17 7 13 15 16 syl3anc 
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> ( y ( ball ` ( abs o. - ) ) r ) e. J )
18 simprr 
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> ( y ( ball ` ( abs o. - ) ) r ) C_ x )
19 vex 
 |-  x e. _V
20 19 elpw2 
 |-  ( ( y ( ball ` ( abs o. - ) ) r ) e. ~P x <-> ( y ( ball ` ( abs o. - ) ) r ) C_ x )
21 18 20 sylibr 
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> ( y ( ball ` ( abs o. - ) ) r ) e. ~P x )
22 17 21 elind 
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> ( y ( ball ` ( abs o. - ) ) r ) e. ( J i^i ~P x ) )
23 simprl 
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> r e. RR+ )
24 blcntr 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ y e. CC /\ r e. RR+ ) -> y e. ( y ( ball ` ( abs o. - ) ) r ) )
25 7 13 23 24 syl3anc 
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> y e. ( y ( ball ` ( abs o. - ) ) r ) )
26 eqid 
 |-  ( y ( ball ` ( abs o. - ) ) r ) = ( y ( ball ` ( abs o. - ) ) r )
27 eqid 
 |-  ( J |`t ( y ( ball ` ( abs o. - ) ) r ) ) = ( J |`t ( y ( ball ` ( abs o. - ) ) r ) )
28 1 26 27 blsconn 
 |-  ( ( y e. CC /\ r e. RR* ) -> ( J |`t ( y ( ball ` ( abs o. - ) ) r ) ) e. SConn )
29 13 15 28 syl2anc 
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> ( J |`t ( y ( ball ` ( abs o. - ) ) r ) ) e. SConn )
30 eleq2 
 |-  ( u = ( y ( ball ` ( abs o. - ) ) r ) -> ( y e. u <-> y e. ( y ( ball ` ( abs o. - ) ) r ) ) )
31 oveq2 
 |-  ( u = ( y ( ball ` ( abs o. - ) ) r ) -> ( J |`t u ) = ( J |`t ( y ( ball ` ( abs o. - ) ) r ) ) )
32 31 eleq1d 
 |-  ( u = ( y ( ball ` ( abs o. - ) ) r ) -> ( ( J |`t u ) e. SConn <-> ( J |`t ( y ( ball ` ( abs o. - ) ) r ) ) e. SConn ) )
33 30 32 anbi12d 
 |-  ( u = ( y ( ball ` ( abs o. - ) ) r ) -> ( ( y e. u /\ ( J |`t u ) e. SConn ) <-> ( y e. ( y ( ball ` ( abs o. - ) ) r ) /\ ( J |`t ( y ( ball ` ( abs o. - ) ) r ) ) e. SConn ) ) )
34 33 rspcev 
 |-  ( ( ( y ( ball ` ( abs o. - ) ) r ) e. ( J i^i ~P x ) /\ ( y e. ( y ( ball ` ( abs o. - ) ) r ) /\ ( J |`t ( y ( ball ` ( abs o. - ) ) r ) ) e. SConn ) ) -> E. u e. ( J i^i ~P x ) ( y e. u /\ ( J |`t u ) e. SConn ) )
35 22 25 29 34 syl12anc 
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> E. u e. ( J i^i ~P x ) ( y e. u /\ ( J |`t u ) e. SConn ) )
36 6 35 rexlimddv 
 |-  ( ( x e. J /\ y e. x ) -> E. u e. ( J i^i ~P x ) ( y e. u /\ ( J |`t u ) e. SConn ) )
37 36 rgen2 
 |-  A. x e. J A. y e. x E. u e. ( J i^i ~P x ) ( y e. u /\ ( J |`t u ) e. SConn )
38 islly 
 |-  ( J e. Locally SConn <-> ( 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. SConn ) ) )
39 2 37 38 mpbir2an 
 |-  J e. Locally SConn