Description: A closed interval is locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | iccllysconn | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simprl | |
|
2 | inss1 | |
|
3 | simprr | |
|
4 | 2 3 | sselid | |
5 | tg2 | |
|
6 | 1 4 5 | syl2anc | |
7 | ioof | |
|
8 | ffn | |
|
9 | ovelrn | |
|
10 | 7 8 9 | mp2b | |
11 | inss1 | |
|
12 | simprrr | |
|
13 | 11 12 | sstrid | |
14 | simprrl | |
|
15 | simprl | |
|
16 | 15 | ineq1d | |
17 | 16 | oveq2d | |
18 | ioosconn | |
|
19 | ioossre | |
|
20 | eqid | |
|
21 | 20 | resconn | |
22 | reconn | |
|
23 | 21 22 | bitrd | |
24 | 19 23 | ax-mp | |
25 | 18 24 | mpbi | |
26 | inss1 | |
|
27 | ssralv | |
|
28 | 27 | ralimdv | |
29 | ssralv | |
|
30 | 28 29 | syld | |
31 | 26 30 | ax-mp | |
32 | 25 31 | mp1i | |
33 | inss2 | |
|
34 | iccconn | |
|
35 | iccssre | |
|
36 | reconn | |
|
37 | 35 36 | syl | |
38 | 34 37 | mpbid | |
39 | 38 | ad2antrr | |
40 | ssralv | |
|
41 | 40 | ralimdv | |
42 | ssralv | |
|
43 | 41 42 | syld | |
44 | 33 39 43 | mpsyl | |
45 | ssin | |
|
46 | 45 | 2ralbii | |
47 | r19.26-2 | |
|
48 | 46 47 | bitr3i | |
49 | 32 44 48 | sylanbrc | |
50 | 26 19 | sstri | |
51 | eqid | |
|
52 | 51 | resconn | |
53 | reconn | |
|
54 | 52 53 | bitrd | |
55 | 50 54 | ax-mp | |
56 | 49 55 | sylibr | |
57 | 17 56 | eqeltrd | |
58 | 13 14 57 | 3jca | |
59 | 58 | exp32 | |
60 | 59 | rexlimdvw | |
61 | 60 | rexlimdvw | |
62 | 10 61 | syl5bi | |
63 | 62 | reximdvai | |
64 | retopbas | |
|
65 | bastg | |
|
66 | ssrexv | |
|
67 | 64 65 66 | mp2b | |
68 | 63 67 | syl6 | |
69 | 6 68 | mpd | |
70 | 69 | ralrimivva | |
71 | retop | |
|
72 | ovex | |
|
73 | subislly | |
|
74 | 71 72 73 | mp2an | |
75 | 70 74 | sylibr | |