Metamath Proof Explorer


Theorem connpconn

Description: A connected and locally path-connected space is path-connected. (Contributed by Mario Carneiro, 7-Jul-2015)

Ref Expression
Assertion connpconn J Conn J N-Locally PConn J PConn

Proof

Step Hyp Ref Expression
1 conntop J Conn J Top
2 1 adantr J Conn J N-Locally PConn J Top
3 eqid J = J
4 simpll J Conn J N-Locally PConn x J J Conn
5 inss1 J Clsd J J
6 simplr J Conn J N-Locally PConn x J z J J N-Locally PConn
7 1 ad2antrr J Conn J N-Locally PConn x J z J J Top
8 3 topopn J Top J J
9 7 8 syl J Conn J N-Locally PConn x J z J J J
10 simprr J Conn J N-Locally PConn x J z J z J
11 nlly2i J N-Locally PConn J J z J s 𝒫 J u J z u u s J 𝑡 s PConn
12 6 9 10 11 syl3anc J Conn J N-Locally PConn x J z J s 𝒫 J u J z u u s J 𝑡 s PConn
13 simprr1 J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn z u
14 eqeq2 y = w f 1 = y f 1 = w
15 14 anbi2d y = w f 0 = x f 1 = y f 0 = x f 1 = w
16 15 rexbidv y = w f II Cn J f 0 = x f 1 = y f II Cn J f 0 = x f 1 = w
17 16 elrab w y J | f II Cn J f 0 = x f 1 = y w J f II Cn J f 0 = x f 1 = w
18 17 simprbi w y J | f II Cn J f 0 = x f 1 = y f II Cn J f 0 = x f 1 = w
19 simprr3 J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn J 𝑡 s PConn
20 19 adantr J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u J 𝑡 s PConn
21 simprr2 J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn u s
22 21 adantr J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u u s
23 simprll J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u w u
24 22 23 sseldd J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u w s
25 7 ad2antrr J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u J Top
26 elpwi s 𝒫 J s J
27 26 ad2antrl J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn s J
28 27 adantr J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u s J
29 3 restuni J Top s J s = J 𝑡 s
30 25 28 29 syl2anc J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u s = J 𝑡 s
31 24 30 eleqtrd J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u w J 𝑡 s
32 simprr J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u y u
33 22 32 sseldd J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u y s
34 33 30 eleqtrd J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u y J 𝑡 s
35 eqid J 𝑡 s = J 𝑡 s
36 35 pconncn J 𝑡 s PConn w J 𝑡 s y J 𝑡 s h II Cn J 𝑡 s h 0 = w h 1 = y
37 20 31 34 36 syl3anc J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u h II Cn J 𝑡 s h 0 = w h 1 = y
38 simplrl w u g II Cn J g 0 = x g 1 = w y u g II Cn J
39 38 ad2antlr J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u h II Cn J 𝑡 s h 0 = w h 1 = y g II Cn J
40 25 adantr J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u h II Cn J 𝑡 s h 0 = w h 1 = y J Top
41 cnrest2r J Top II Cn J 𝑡 s II Cn J
42 40 41 syl J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u h II Cn J 𝑡 s h 0 = w h 1 = y II Cn J 𝑡 s II Cn J
43 simprl J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u h II Cn J 𝑡 s h 0 = w h 1 = y h II Cn J 𝑡 s
44 42 43 sseldd J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u h II Cn J 𝑡 s h 0 = w h 1 = y h II Cn J
45 simplrr w u g II Cn J g 0 = x g 1 = w y u g 0 = x g 1 = w
46 45 ad2antlr J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u h II Cn J 𝑡 s h 0 = w h 1 = y g 0 = x g 1 = w
47 46 simprd J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u h II Cn J 𝑡 s h 0 = w h 1 = y g 1 = w
48 simprrl J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u h II Cn J 𝑡 s h 0 = w h 1 = y h 0 = w
49 47 48 eqtr4d J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u h II Cn J 𝑡 s h 0 = w h 1 = y g 1 = h 0
50 39 44 49 pcocn J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u h II Cn J 𝑡 s h 0 = w h 1 = y g * 𝑝 J h II Cn J
51 39 44 pco0 J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u h II Cn J 𝑡 s h 0 = w h 1 = y g * 𝑝 J h 0 = g 0
52 46 simpld J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u h II Cn J 𝑡 s h 0 = w h 1 = y g 0 = x
53 51 52 eqtrd J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u h II Cn J 𝑡 s h 0 = w h 1 = y g * 𝑝 J h 0 = x
54 39 44 pco1 J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u h II Cn J 𝑡 s h 0 = w h 1 = y g * 𝑝 J h 1 = h 1
55 simprrr J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u h II Cn J 𝑡 s h 0 = w h 1 = y h 1 = y
56 54 55 eqtrd J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u h II Cn J 𝑡 s h 0 = w h 1 = y g * 𝑝 J h 1 = y
57 fveq1 f = g * 𝑝 J h f 0 = g * 𝑝 J h 0
58 57 eqeq1d f = g * 𝑝 J h f 0 = x g * 𝑝 J h 0 = x
59 fveq1 f = g * 𝑝 J h f 1 = g * 𝑝 J h 1
60 59 eqeq1d f = g * 𝑝 J h f 1 = y g * 𝑝 J h 1 = y
61 58 60 anbi12d f = g * 𝑝 J h f 0 = x f 1 = y g * 𝑝 J h 0 = x g * 𝑝 J h 1 = y
62 61 rspcev g * 𝑝 J h II Cn J g * 𝑝 J h 0 = x g * 𝑝 J h 1 = y f II Cn J f 0 = x f 1 = y
63 50 53 56 62 syl12anc J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u h II Cn J 𝑡 s h 0 = w h 1 = y f II Cn J f 0 = x f 1 = y
64 37 63 rexlimddv J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u f II Cn J f 0 = x f 1 = y
65 64 anassrs J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u f II Cn J f 0 = x f 1 = y
66 65 ralrimiva J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u f II Cn J f 0 = x f 1 = y
67 66 anassrs J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u f II Cn J f 0 = x f 1 = y
68 67 rexlimdvaa J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w y u f II Cn J f 0 = x f 1 = y
69 21 adantr J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u u s
70 simplrl J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u s 𝒫 J
71 70 26 syl J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u s J
72 69 71 sstrd J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u u J
73 68 72 jctild J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u g II Cn J g 0 = x g 1 = w u J y u f II Cn J f 0 = x f 1 = y
74 fveq1 f = g f 0 = g 0
75 74 eqeq1d f = g f 0 = x g 0 = x
76 fveq1 f = g f 1 = g 1
77 76 eqeq1d f = g f 1 = w g 1 = w
78 75 77 anbi12d f = g f 0 = x f 1 = w g 0 = x g 1 = w
79 78 cbvrexvw f II Cn J f 0 = x f 1 = w g II Cn J g 0 = x g 1 = w
80 ssrab u y J | f II Cn J f 0 = x f 1 = y u J y u f II Cn J f 0 = x f 1 = y
81 73 79 80 3imtr4g J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u f II Cn J f 0 = x f 1 = w u y J | f II Cn J f 0 = x f 1 = y
82 18 81 syl5 J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u w y J | f II Cn J f 0 = x f 1 = y u y J | f II Cn J f 0 = x f 1 = y
83 82 ralrimiva J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn w u w y J | f II Cn J f 0 = x f 1 = y u y J | f II Cn J f 0 = x f 1 = y
84 13 83 jca J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn z u w u w y J | f II Cn J f 0 = x f 1 = y u y J | f II Cn J f 0 = x f 1 = y
85 84 expr J Conn J N-Locally PConn x J z J s 𝒫 J z u u s J 𝑡 s PConn z u w u w y J | f II Cn J f 0 = x f 1 = y u y J | f II Cn J f 0 = x f 1 = y
86 85 reximdv J Conn J N-Locally PConn x J z J s 𝒫 J u J z u u s J 𝑡 s PConn u J z u w u w y J | f II Cn J f 0 = x f 1 = y u y J | f II Cn J f 0 = x f 1 = y
87 86 rexlimdva J Conn J N-Locally PConn x J z J s 𝒫 J u J z u u s J 𝑡 s PConn u J z u w u w y J | f II Cn J f 0 = x f 1 = y u y J | f II Cn J f 0 = x f 1 = y
88 12 87 mpd J Conn J N-Locally PConn x J z J u J z u w u w y J | f II Cn J f 0 = x f 1 = y u y J | f II Cn J f 0 = x f 1 = y
89 88 anassrs J Conn J N-Locally PConn x J z J u J z u w u w y J | f II Cn J f 0 = x f 1 = y u y J | f II Cn J f 0 = x f 1 = y
90 89 ralrimiva J Conn J N-Locally PConn x J z J u J z u w u w y J | f II Cn J f 0 = x f 1 = y u y J | f II Cn J f 0 = x f 1 = y
91 1 ad2antrr J Conn J N-Locally PConn x J J Top
92 ssrab2 y J | f II Cn J f 0 = x f 1 = y J
93 3 isclo2 J Top y J | f II Cn J f 0 = x f 1 = y J y J | f II Cn J f 0 = x f 1 = y J Clsd J z J u J z u w u w y J | f II Cn J f 0 = x f 1 = y u y J | f II Cn J f 0 = x f 1 = y
94 91 92 93 sylancl J Conn J N-Locally PConn x J y J | f II Cn J f 0 = x f 1 = y J Clsd J z J u J z u w u w y J | f II Cn J f 0 = x f 1 = y u y J | f II Cn J f 0 = x f 1 = y
95 90 94 mpbird J Conn J N-Locally PConn x J y J | f II Cn J f 0 = x f 1 = y J Clsd J
96 5 95 sselid J Conn J N-Locally PConn x J y J | f II Cn J f 0 = x f 1 = y J
97 simpr J Conn J N-Locally PConn x J x J
98 iitopon II TopOn 0 1
99 98 a1i J Conn J N-Locally PConn x J II TopOn 0 1
100 3 toptopon J Top J TopOn J
101 91 100 sylib J Conn J N-Locally PConn x J J TopOn J
102 cnconst2 II TopOn 0 1 J TopOn J x J 0 1 × x II Cn J
103 99 101 97 102 syl3anc J Conn J N-Locally PConn x J 0 1 × x II Cn J
104 0elunit 0 0 1
105 vex x V
106 105 fvconst2 0 0 1 0 1 × x 0 = x
107 104 106 mp1i J Conn J N-Locally PConn x J 0 1 × x 0 = x
108 1elunit 1 0 1
109 105 fvconst2 1 0 1 0 1 × x 1 = x
110 108 109 mp1i J Conn J N-Locally PConn x J 0 1 × x 1 = x
111 eqeq2 y = x f 1 = y f 1 = x
112 111 anbi2d y = x f 0 = x f 1 = y f 0 = x f 1 = x
113 fveq1 f = 0 1 × x f 0 = 0 1 × x 0
114 113 eqeq1d f = 0 1 × x f 0 = x 0 1 × x 0 = x
115 fveq1 f = 0 1 × x f 1 = 0 1 × x 1
116 115 eqeq1d f = 0 1 × x f 1 = x 0 1 × x 1 = x
117 114 116 anbi12d f = 0 1 × x f 0 = x f 1 = x 0 1 × x 0 = x 0 1 × x 1 = x
118 112 117 rspc2ev x J 0 1 × x II Cn J 0 1 × x 0 = x 0 1 × x 1 = x y J f II Cn J f 0 = x f 1 = y
119 97 103 107 110 118 syl112anc J Conn J N-Locally PConn x J y J f II Cn J f 0 = x f 1 = y
120 rabn0 y J | f II Cn J f 0 = x f 1 = y y J f II Cn J f 0 = x f 1 = y
121 119 120 sylibr J Conn J N-Locally PConn x J y J | f II Cn J f 0 = x f 1 = y
122 inss2 J Clsd J Clsd J
123 122 95 sselid J Conn J N-Locally PConn x J y J | f II Cn J f 0 = x f 1 = y Clsd J
124 3 4 96 121 123 connclo J Conn J N-Locally PConn x J y J | f II Cn J f 0 = x f 1 = y = J
125 124 eqcomd J Conn J N-Locally PConn x J J = y J | f II Cn J f 0 = x f 1 = y
126 rabid2 J = y J | f II Cn J f 0 = x f 1 = y y J f II Cn J f 0 = x f 1 = y
127 125 126 sylib J Conn J N-Locally PConn x J y J f II Cn J f 0 = x f 1 = y
128 127 ralrimiva J Conn J N-Locally PConn x J y J f II Cn J f 0 = x f 1 = y
129 3 ispconn J PConn J Top x J y J f II Cn J f 0 = x f 1 = y
130 2 128 129 sylanbrc J Conn J N-Locally PConn J PConn