Metamath Proof Explorer

Theorem rellysconn

Description: The real numbers are locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015)

Ref Expression
Assertion rellysconn 
|- ( topGen ` ran (,) ) e. Locally SConn

Proof

Step Hyp Ref Expression
1 retop 
 |-  ( topGen ` ran (,) ) e. Top
2 tg2 
 |-  ( ( x e. ( topGen ` ran (,) ) /\ y e. x ) -> E. z e. ran (,) ( y e. z /\ z C_ x ) )
3 retopbas 
 |-  ran (,) e. TopBases
4 bastg 
 |-  ( ran (,) e. TopBases -> ran (,) C_ ( topGen ` ran (,) ) )
5 3 4 ax-mp 
 |-  ran (,) C_ ( topGen ` ran (,) )
6 simprl 
 |-  ( ( ( x e. ( topGen ` ran (,) ) /\ y e. x ) /\ ( z e. ran (,) /\ ( y e. z /\ z C_ x ) ) ) -> z e. ran (,) )
7 5 6 sseldi 
 |-  ( ( ( x e. ( topGen ` ran (,) ) /\ y e. x ) /\ ( z e. ran (,) /\ ( y e. z /\ z C_ x ) ) ) -> z e. ( topGen ` ran (,) ) )
8 simprrr 
 |-  ( ( ( x e. ( topGen ` ran (,) ) /\ y e. x ) /\ ( z e. ran (,) /\ ( y e. z /\ z C_ x ) ) ) -> z C_ x )
9 velpw 
 |-  ( z e. ~P x <-> z C_ x )
10 8 9 sylibr 
 |-  ( ( ( x e. ( topGen ` ran (,) ) /\ y e. x ) /\ ( z e. ran (,) /\ ( y e. z /\ z C_ x ) ) ) -> z e. ~P x )
11 7 10 elind 
 |-  ( ( ( x e. ( topGen ` ran (,) ) /\ y e. x ) /\ ( z e. ran (,) /\ ( y e. z /\ z C_ x ) ) ) -> z e. ( ( topGen ` ran (,) ) i^i ~P x ) )
12 simprrl 
 |-  ( ( ( x e. ( topGen ` ran (,) ) /\ y e. x ) /\ ( z e. ran (,) /\ ( y e. z /\ z C_ x ) ) ) -> y e. z )
13 ioof 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
14 ffn 
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> (,) Fn ( RR* X. RR* ) )
15 ovelrn 
 |-  ( (,) Fn ( RR* X. RR* ) -> ( z e. ran (,) <-> E. a e. RR* E. b e. RR* z = ( a (,) b ) ) )
16 13 14 15 mp2b 
 |-  ( z e. ran (,) <-> E. a e. RR* E. b e. RR* z = ( a (,) b ) )
17 oveq2 
 |-  ( z = ( a (,) b ) -> ( ( topGen ` ran (,) ) |`t z ) = ( ( topGen ` ran (,) ) |`t ( a (,) b ) ) )
18 ioosconn 
 |-  ( ( topGen ` ran (,) ) |`t ( a (,) b ) ) e. SConn
19 17 18 eqeltrdi 
 |-  ( z = ( a (,) b ) -> ( ( topGen ` ran (,) ) |`t z ) e. SConn )
20 19 rexlimivw 
 |-  ( E. b e. RR* z = ( a (,) b ) -> ( ( topGen ` ran (,) ) |`t z ) e. SConn )
21 20 rexlimivw 
 |-  ( E. a e. RR* E. b e. RR* z = ( a (,) b ) -> ( ( topGen ` ran (,) ) |`t z ) e. SConn )
22 16 21 sylbi 
 |-  ( z e. ran (,) -> ( ( topGen ` ran (,) ) |`t z ) e. SConn )
23 22 ad2antrl 
 |-  ( ( ( x e. ( topGen ` ran (,) ) /\ y e. x ) /\ ( z e. ran (,) /\ ( y e. z /\ z C_ x ) ) ) -> ( ( topGen ` ran (,) ) |`t z ) e. SConn )
24 11 12 23 jca32 
 |-  ( ( ( x e. ( topGen ` ran (,) ) /\ y e. x ) /\ ( z e. ran (,) /\ ( y e. z /\ z C_ x ) ) ) -> ( z e. ( ( topGen ` ran (,) ) i^i ~P x ) /\ ( y e. z /\ ( ( topGen ` ran (,) ) |`t z ) e. SConn ) ) )
25 24 ex 
 |-  ( ( x e. ( topGen ` ran (,) ) /\ y e. x ) -> ( ( z e. ran (,) /\ ( y e. z /\ z C_ x ) ) -> ( z e. ( ( topGen ` ran (,) ) i^i ~P x ) /\ ( y e. z /\ ( ( topGen ` ran (,) ) |`t z ) e. SConn ) ) ) )
26 25 reximdv2 
 |-  ( ( x e. ( topGen ` ran (,) ) /\ y e. x ) -> ( E. z e. ran (,) ( y e. z /\ z C_ x ) -> E. z e. ( ( topGen ` ran (,) ) i^i ~P x ) ( y e. z /\ ( ( topGen ` ran (,) ) |`t z ) e. SConn ) ) )
27 2 26 mpd 
 |-  ( ( x e. ( topGen ` ran (,) ) /\ y e. x ) -> E. z e. ( ( topGen ` ran (,) ) i^i ~P x ) ( y e. z /\ ( ( topGen ` ran (,) ) |`t z ) e. SConn ) )
28 27 rgen2 
 |-  A. x e. ( topGen ` ran (,) ) A. y e. x E. z e. ( ( topGen ` ran (,) ) i^i ~P x ) ( y e. z /\ ( ( topGen ` ran (,) ) |`t z ) e. SConn )
29 islly 
 |-  ( ( topGen ` ran (,) ) e. Locally SConn <-> ( ( topGen ` ran (,) ) e. Top /\ A. x e. ( topGen ` ran (,) ) A. y e. x E. z e. ( ( topGen ` ran (,) ) i^i ~P x ) ( y e. z /\ ( ( topGen ` ran (,) ) |`t z ) e. SConn ) ) )
30 1 28 29 mpbir2an 
 |-  ( topGen ` ran (,) ) e. Locally SConn