Metamath Proof Explorer


Theorem rellysconn

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

Ref Expression
Assertion rellysconn topGenran.Locally SConn

Proof

Step Hyp Ref Expression
1 retop topGenran.Top
2 tg2 xtopGenran.yxzran.yzzx
3 retopbas ran.TopBases
4 bastg ran.TopBasesran.topGenran.
5 3 4 ax-mp ran.topGenran.
6 simprl xtopGenran.yxzran.yzzxzran.
7 5 6 sselid xtopGenran.yxzran.yzzxztopGenran.
8 simprrr xtopGenran.yxzran.yzzxzx
9 velpw z𝒫xzx
10 8 9 sylibr xtopGenran.yxzran.yzzxz𝒫x
11 7 10 elind xtopGenran.yxzran.yzzxztopGenran.𝒫x
12 simprrl xtopGenran.yxzran.yzzxyz
13 ioof .:*×*𝒫
14 ffn .:*×*𝒫.Fn*×*
15 ovelrn .Fn*×*zran.a*b*z=ab
16 13 14 15 mp2b zran.a*b*z=ab
17 oveq2 z=abtopGenran.𝑡z=topGenran.𝑡ab
18 ioosconn topGenran.𝑡abSConn
19 17 18 eqeltrdi z=abtopGenran.𝑡zSConn
20 19 rexlimivw b*z=abtopGenran.𝑡zSConn
21 20 rexlimivw a*b*z=abtopGenran.𝑡zSConn
22 16 21 sylbi zran.topGenran.𝑡zSConn
23 22 ad2antrl xtopGenran.yxzran.yzzxtopGenran.𝑡zSConn
24 11 12 23 jca32 xtopGenran.yxzran.yzzxztopGenran.𝒫xyztopGenran.𝑡zSConn
25 24 ex xtopGenran.yxzran.yzzxztopGenran.𝒫xyztopGenran.𝑡zSConn
26 25 reximdv2 xtopGenran.yxzran.yzzxztopGenran.𝒫xyztopGenran.𝑡zSConn
27 2 26 mpd xtopGenran.yxztopGenran.𝒫xyztopGenran.𝑡zSConn
28 27 rgen2 xtopGenran.yxztopGenran.𝒫xyztopGenran.𝑡zSConn
29 islly topGenran.Locally SConn topGenran.TopxtopGenran.yxztopGenran.𝒫xyztopGenran.𝑡zSConn
30 1 28 29 mpbir2an topGenran.Locally SConn