Metamath Proof Explorer


Theorem iccllysconn

Description: A closed interval is locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015)

Ref Expression
Assertion iccllysconn ABtopGenran.𝑡ABLocally SConn

Proof

Step Hyp Ref Expression
1 simprl ABxtopGenran.yxABxtopGenran.
2 inss1 xABx
3 simprr ABxtopGenran.yxAByxAB
4 2 3 sselid ABxtopGenran.yxAByx
5 tg2 xtopGenran.yxzran.yzzx
6 1 4 5 syl2anc ABxtopGenran.yxABzran.yzzx
7 ioof .:*×*𝒫
8 ffn .:*×*𝒫.Fn*×*
9 ovelrn .Fn*×*zran.a*b*z=ab
10 7 8 9 mp2b zran.a*b*z=ab
11 inss1 zABz
12 simprrr ABxtopGenran.yxABz=abyzzxzx
13 11 12 sstrid ABxtopGenran.yxABz=abyzzxzABx
14 simprrl ABxtopGenran.yxABz=abyzzxyz
15 simprl ABxtopGenran.yxABz=abyzzxz=ab
16 15 ineq1d ABxtopGenran.yxABz=abyzzxzAB=abAB
17 16 oveq2d ABxtopGenran.yxABz=abyzzxtopGenran.𝑡zAB=topGenran.𝑡abAB
18 ioosconn topGenran.𝑡abSConn
19 ioossre ab
20 eqid topGenran.𝑡ab=topGenran.𝑡ab
21 20 resconn abtopGenran.𝑡abSConntopGenran.𝑡abConn
22 reconn abtopGenran.𝑡abConnuabvabuvab
23 21 22 bitrd abtopGenran.𝑡abSConnuabvabuvab
24 19 23 ax-mp topGenran.𝑡abSConnuabvabuvab
25 18 24 mpbi uabvabuvab
26 inss1 abABab
27 ssralv abABabvabuvabvabABuvab
28 27 ralimdv abABabuabvabuvabuabvabABuvab
29 ssralv abABabuabvabABuvabuabABvabABuvab
30 28 29 syld abABabuabvabuvabuabABvabABuvab
31 26 30 ax-mp uabvabuvabuabABvabABuvab
32 25 31 mp1i ABxtopGenran.yxABz=abyzzxuabABvabABuvab
33 inss2 abABAB
34 iccconn ABtopGenran.𝑡ABConn
35 iccssre ABAB
36 reconn ABtopGenran.𝑡ABConnuABvABuvAB
37 35 36 syl ABtopGenran.𝑡ABConnuABvABuvAB
38 34 37 mpbid ABuABvABuvAB
39 38 ad2antrr ABxtopGenran.yxABz=abyzzxuABvABuvAB
40 ssralv abABABvABuvABvabABuvAB
41 40 ralimdv abABABuABvABuvABuABvabABuvAB
42 ssralv abABABuABvabABuvABuabABvabABuvAB
43 41 42 syld abABABuABvABuvABuabABvabABuvAB
44 33 39 43 mpsyl ABxtopGenran.yxABz=abyzzxuabABvabABuvAB
45 ssin uvabuvABuvabAB
46 45 2ralbii uabABvabABuvabuvABuabABvabABuvabAB
47 r19.26-2 uabABvabABuvabuvABuabABvabABuvabuabABvabABuvAB
48 46 47 bitr3i uabABvabABuvabABuabABvabABuvabuabABvabABuvAB
49 32 44 48 sylanbrc ABxtopGenran.yxABz=abyzzxuabABvabABuvabAB
50 26 19 sstri abAB
51 eqid topGenran.𝑡abAB=topGenran.𝑡abAB
52 51 resconn abABtopGenran.𝑡abABSConntopGenran.𝑡abABConn
53 reconn abABtopGenran.𝑡abABConnuabABvabABuvabAB
54 52 53 bitrd abABtopGenran.𝑡abABSConnuabABvabABuvabAB
55 50 54 ax-mp topGenran.𝑡abABSConnuabABvabABuvabAB
56 49 55 sylibr ABxtopGenran.yxABz=abyzzxtopGenran.𝑡abABSConn
57 17 56 eqeltrd ABxtopGenran.yxABz=abyzzxtopGenran.𝑡zABSConn
58 13 14 57 3jca ABxtopGenran.yxABz=abyzzxzABxyztopGenran.𝑡zABSConn
59 58 exp32 ABxtopGenran.yxABz=abyzzxzABxyztopGenran.𝑡zABSConn
60 59 rexlimdvw ABxtopGenran.yxABb*z=abyzzxzABxyztopGenran.𝑡zABSConn
61 60 rexlimdvw ABxtopGenran.yxABa*b*z=abyzzxzABxyztopGenran.𝑡zABSConn
62 10 61 syl5bi ABxtopGenran.yxABzran.yzzxzABxyztopGenran.𝑡zABSConn
63 62 reximdvai ABxtopGenran.yxABzran.yzzxzran.zABxyztopGenran.𝑡zABSConn
64 retopbas ran.TopBases
65 bastg ran.TopBasesran.topGenran.
66 ssrexv ran.topGenran.zran.zABxyztopGenran.𝑡zABSConnztopGenran.zABxyztopGenran.𝑡zABSConn
67 64 65 66 mp2b zran.zABxyztopGenran.𝑡zABSConnztopGenran.zABxyztopGenran.𝑡zABSConn
68 63 67 syl6 ABxtopGenran.yxABzran.yzzxztopGenran.zABxyztopGenran.𝑡zABSConn
69 6 68 mpd ABxtopGenran.yxABztopGenran.zABxyztopGenran.𝑡zABSConn
70 69 ralrimivva ABxtopGenran.yxABztopGenran.zABxyztopGenran.𝑡zABSConn
71 retop topGenran.Top
72 ovex ABV
73 subislly topGenran.TopABVtopGenran.𝑡ABLocally SConn xtopGenran.yxABztopGenran.zABxyztopGenran.𝑡zABSConn
74 71 72 73 mp2an topGenran.𝑡ABLocally SConn xtopGenran.yxABztopGenran.zABxyztopGenran.𝑡zABSConn
75 70 74 sylibr ABtopGenran.𝑡ABLocally SConn