Metamath Proof Explorer


Theorem ptpconn

Description: The topological product of a collection of path-connected spaces is path-connected. The proof uses the axiom of choice. (Contributed by Mario Carneiro, 17-Feb-2015)

Ref Expression
Assertion ptpconn AVF:APConn𝑡FPConn

Proof

Step Hyp Ref Expression
1 pconntop xPConnxTop
2 1 ssriv PConnTop
3 fss F:APConnPConnTopF:ATop
4 2 3 mpan2 F:APConnF:ATop
5 pttop AVF:ATop𝑡FTop
6 4 5 sylan2 AVF:APConn𝑡FTop
7 fvi AVIA=A
8 7 ad2antrr AVF:APConnx𝑡Fy𝑡FIA=A
9 8 eleq2d AVF:APConnx𝑡Fy𝑡FtIAtA
10 9 biimpa AVF:APConnx𝑡Fy𝑡FtIAtA
11 simplr AVF:APConnx𝑡Fy𝑡FF:APConn
12 11 ffvelrnda AVF:APConnx𝑡Fy𝑡FtAFtPConn
13 simprl AVF:APConnx𝑡Fy𝑡Fx𝑡F
14 eqid 𝑡F=𝑡F
15 14 ptuni AVF:AToptAFt=𝑡F
16 4 15 sylan2 AVF:APConntAFt=𝑡F
17 16 adantr AVF:APConnx𝑡Fy𝑡FtAFt=𝑡F
18 13 17 eleqtrrd AVF:APConnx𝑡Fy𝑡FxtAFt
19 vex xV
20 19 elixp xtAFtxFnAtAxtFt
21 18 20 sylib AVF:APConnx𝑡Fy𝑡FxFnAtAxtFt
22 21 simprd AVF:APConnx𝑡Fy𝑡FtAxtFt
23 22 r19.21bi AVF:APConnx𝑡Fy𝑡FtAxtFt
24 simprr AVF:APConnx𝑡Fy𝑡Fy𝑡F
25 24 17 eleqtrrd AVF:APConnx𝑡Fy𝑡FytAFt
26 vex yV
27 26 elixp ytAFtyFnAtAytFt
28 25 27 sylib AVF:APConnx𝑡Fy𝑡FyFnAtAytFt
29 28 simprd AVF:APConnx𝑡Fy𝑡FtAytFt
30 29 r19.21bi AVF:APConnx𝑡Fy𝑡FtAytFt
31 eqid Ft=Ft
32 31 pconncn FtPConnxtFtytFtfIICnFtf0=xtf1=yt
33 12 23 30 32 syl3anc AVF:APConnx𝑡Fy𝑡FtAfIICnFtf0=xtf1=yt
34 df-rex fIICnFtf0=xtf1=ytffIICnFtf0=xtf1=yt
35 33 34 sylib AVF:APConnx𝑡Fy𝑡FtAffIICnFtf0=xtf1=yt
36 10 35 syldan AVF:APConnx𝑡Fy𝑡FtIAffIICnFtf0=xtf1=yt
37 36 ralrimiva AVF:APConnx𝑡Fy𝑡FtIAffIICnFtf0=xtf1=yt
38 fvex IAV
39 eleq1 f=gtfIICnFtgtIICnFt
40 fveq1 f=gtf0=gt0
41 40 eqeq1d f=gtf0=xtgt0=xt
42 fveq1 f=gtf1=gt1
43 42 eqeq1d f=gtf1=ytgt1=yt
44 41 43 anbi12d f=gtf0=xtf1=ytgt0=xtgt1=yt
45 39 44 anbi12d f=gtfIICnFtf0=xtf1=ytgtIICnFtgt0=xtgt1=yt
46 38 45 ac6s2 tIAffIICnFtf0=xtf1=ytggFnIAtIAgtIICnFtgt0=xtgt1=yt
47 37 46 syl AVF:APConnx𝑡Fy𝑡FggFnIAtIAgtIICnFtgt0=xtgt1=yt
48 iitopon IITopOn01
49 48 a1i AVF:APConnx𝑡Fy𝑡FgFnIAtIAgtIICnFtgt0=xtgt1=ytIITopOn01
50 simplll AVF:APConnx𝑡Fy𝑡FgFnIAtIAgtIICnFtgt0=xtgt1=ytAV
51 11 adantr AVF:APConnx𝑡Fy𝑡FgFnIAtIAgtIICnFtgt0=xtgt1=ytF:APConn
52 51 4 syl AVF:APConnx𝑡Fy𝑡FgFnIAtIAgtIICnFtgt0=xtgt1=ytF:ATop
53 8 adantr AVF:APConnx𝑡Fy𝑡FgFnIAtIAgtIICnFtgt0=xtgt1=ytIA=A
54 53 eleq2d AVF:APConnx𝑡Fy𝑡FgFnIAtIAgtIICnFtgt0=xtgt1=ytiIAiA
55 54 biimpar AVF:APConnx𝑡Fy𝑡FgFnIAtIAgtIICnFtgt0=xtgt1=ytiAiIA
56 simprr AVF:APConnx𝑡Fy𝑡FgFnIAtIAgtIICnFtgt0=xtgt1=yttIAgtIICnFtgt0=xtgt1=yt
57 fveq2 t=igt=gi
58 fveq2 t=iFt=Fi
59 58 oveq2d t=iIICnFt=IICnFi
60 57 59 eleq12d t=igtIICnFtgiIICnFi
61 57 fveq1d t=igt0=gi0
62 fveq2 t=ixt=xi
63 61 62 eqeq12d t=igt0=xtgi0=xi
64 57 fveq1d t=igt1=gi1
65 fveq2 t=iyt=yi
66 64 65 eqeq12d t=igt1=ytgi1=yi
67 63 66 anbi12d t=igt0=xtgt1=ytgi0=xigi1=yi
68 60 67 anbi12d t=igtIICnFtgt0=xtgt1=ytgiIICnFigi0=xigi1=yi
69 68 rspccva tIAgtIICnFtgt0=xtgt1=ytiIAgiIICnFigi0=xigi1=yi
70 56 69 sylan AVF:APConnx𝑡Fy𝑡FgFnIAtIAgtIICnFtgt0=xtgt1=ytiIAgiIICnFigi0=xigi1=yi
71 55 70 syldan AVF:APConnx𝑡Fy𝑡FgFnIAtIAgtIICnFtgt0=xtgt1=ytiAgiIICnFigi0=xigi1=yi
72 71 simpld AVF:APConnx𝑡Fy𝑡FgFnIAtIAgtIICnFtgt0=xtgt1=ytiAgiIICnFi
73 iiuni 01=II
74 eqid Fi=Fi
75 73 74 cnf giIICnFigi:01Fi
76 72 75 syl AVF:APConnx𝑡Fy𝑡FgFnIAtIAgtIICnFtgt0=xtgt1=ytiAgi:01Fi
77 76 feqmptd AVF:APConnx𝑡Fy𝑡FgFnIAtIAgtIICnFtgt0=xtgt1=ytiAgi=z01giz
78 77 72 eqeltrrd AVF:APConnx𝑡Fy𝑡FgFnIAtIAgtIICnFtgt0=xtgt1=ytiAz01gizIICnFi
79 14 49 50 52 78 ptcn AVF:APConnx𝑡Fy𝑡FgFnIAtIAgtIICnFtgt0=xtgt1=ytz01iAgizIICn𝑡F
80 71 simprd AVF:APConnx𝑡Fy𝑡FgFnIAtIAgtIICnFtgt0=xtgt1=ytiAgi0=xigi1=yi
81 80 simpld AVF:APConnx𝑡Fy𝑡FgFnIAtIAgtIICnFtgt0=xtgt1=ytiAgi0=xi
82 81 mpteq2dva AVF:APConnx𝑡Fy𝑡FgFnIAtIAgtIICnFtgt0=xtgt1=ytiAgi0=iAxi
83 0elunit 001
84 mptexg AViAgi0V
85 50 84 syl AVF:APConnx𝑡Fy𝑡FgFnIAtIAgtIICnFtgt0=xtgt1=ytiAgi0V
86 fveq2 z=0giz=gi0
87 86 mpteq2dv z=0iAgiz=iAgi0
88 eqid z01iAgiz=z01iAgiz
89 87 88 fvmptg 001iAgi0Vz01iAgiz0=iAgi0
90 83 85 89 sylancr AVF:APConnx𝑡Fy𝑡FgFnIAtIAgtIICnFtgt0=xtgt1=ytz01iAgiz0=iAgi0
91 21 simpld AVF:APConnx𝑡Fy𝑡FxFnA
92 91 adantr AVF:APConnx𝑡Fy𝑡FgFnIAtIAgtIICnFtgt0=xtgt1=ytxFnA
93 dffn5 xFnAx=iAxi
94 92 93 sylib AVF:APConnx𝑡Fy𝑡FgFnIAtIAgtIICnFtgt0=xtgt1=ytx=iAxi
95 82 90 94 3eqtr4d AVF:APConnx𝑡Fy𝑡FgFnIAtIAgtIICnFtgt0=xtgt1=ytz01iAgiz0=x
96 80 simprd AVF:APConnx𝑡Fy𝑡FgFnIAtIAgtIICnFtgt0=xtgt1=ytiAgi1=yi
97 96 mpteq2dva AVF:APConnx𝑡Fy𝑡FgFnIAtIAgtIICnFtgt0=xtgt1=ytiAgi1=iAyi
98 1elunit 101
99 mptexg AViAgi1V
100 50 99 syl AVF:APConnx𝑡Fy𝑡FgFnIAtIAgtIICnFtgt0=xtgt1=ytiAgi1V
101 fveq2 z=1giz=gi1
102 101 mpteq2dv z=1iAgiz=iAgi1
103 102 88 fvmptg 101iAgi1Vz01iAgiz1=iAgi1
104 98 100 103 sylancr AVF:APConnx𝑡Fy𝑡FgFnIAtIAgtIICnFtgt0=xtgt1=ytz01iAgiz1=iAgi1
105 28 simpld AVF:APConnx𝑡Fy𝑡FyFnA
106 105 adantr AVF:APConnx𝑡Fy𝑡FgFnIAtIAgtIICnFtgt0=xtgt1=ytyFnA
107 dffn5 yFnAy=iAyi
108 106 107 sylib AVF:APConnx𝑡Fy𝑡FgFnIAtIAgtIICnFtgt0=xtgt1=yty=iAyi
109 97 104 108 3eqtr4d AVF:APConnx𝑡Fy𝑡FgFnIAtIAgtIICnFtgt0=xtgt1=ytz01iAgiz1=y
110 fveq1 f=z01iAgizf0=z01iAgiz0
111 110 eqeq1d f=z01iAgizf0=xz01iAgiz0=x
112 fveq1 f=z01iAgizf1=z01iAgiz1
113 112 eqeq1d f=z01iAgizf1=yz01iAgiz1=y
114 111 113 anbi12d f=z01iAgizf0=xf1=yz01iAgiz0=xz01iAgiz1=y
115 114 rspcev z01iAgizIICn𝑡Fz01iAgiz0=xz01iAgiz1=yfIICn𝑡Ff0=xf1=y
116 79 95 109 115 syl12anc AVF:APConnx𝑡Fy𝑡FgFnIAtIAgtIICnFtgt0=xtgt1=ytfIICn𝑡Ff0=xf1=y
117 47 116 exlimddv AVF:APConnx𝑡Fy𝑡FfIICn𝑡Ff0=xf1=y
118 117 ralrimivva AVF:APConnx𝑡Fy𝑡FfIICn𝑡Ff0=xf1=y
119 eqid 𝑡F=𝑡F
120 119 ispconn 𝑡FPConn𝑡FTopx𝑡Fy𝑡FfIICn𝑡Ff0=xf1=y
121 6 118 120 sylanbrc AVF:APConn𝑡FPConn