# 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 ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\to {\prod }_{𝑡}\left({F}\right)\in \mathrm{PConn}$

### Proof

Step Hyp Ref Expression
1 pconntop ${⊢}{x}\in \mathrm{PConn}\to {x}\in \mathrm{Top}$
2 1 ssriv ${⊢}\mathrm{PConn}\subseteq \mathrm{Top}$
3 fss ${⊢}\left({F}:{A}⟶\mathrm{PConn}\wedge \mathrm{PConn}\subseteq \mathrm{Top}\right)\to {F}:{A}⟶\mathrm{Top}$
4 2 3 mpan2 ${⊢}{F}:{A}⟶\mathrm{PConn}\to {F}:{A}⟶\mathrm{Top}$
5 pttop ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\to {\prod }_{𝑡}\left({F}\right)\in \mathrm{Top}$
6 4 5 sylan2 ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\to {\prod }_{𝑡}\left({F}\right)\in \mathrm{Top}$
7 fvi ${⊢}{A}\in {V}\to \mathrm{I}\left({A}\right)={A}$
8 7 ad2antrr ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\to \mathrm{I}\left({A}\right)={A}$
9 8 eleq2d ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\to \left({t}\in \mathrm{I}\left({A}\right)↔{t}\in {A}\right)$
10 9 biimpa ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge {t}\in \mathrm{I}\left({A}\right)\right)\to {t}\in {A}$
11 simplr ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\to {F}:{A}⟶\mathrm{PConn}$
12 11 ffvelrnda ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge {t}\in {A}\right)\to {F}\left({t}\right)\in \mathrm{PConn}$
13 simprl ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\to {x}\in \bigcup {\prod }_{𝑡}\left({F}\right)$
14 eqid ${⊢}{\prod }_{𝑡}\left({F}\right)={\prod }_{𝑡}\left({F}\right)$
15 14 ptuni ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{Top}\right)\to \underset{{t}\in {A}}{⨉}\bigcup {F}\left({t}\right)=\bigcup {\prod }_{𝑡}\left({F}\right)$
16 4 15 sylan2 ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\to \underset{{t}\in {A}}{⨉}\bigcup {F}\left({t}\right)=\bigcup {\prod }_{𝑡}\left({F}\right)$
17 16 adantr ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\to \underset{{t}\in {A}}{⨉}\bigcup {F}\left({t}\right)=\bigcup {\prod }_{𝑡}\left({F}\right)$
18 13 17 eleqtrrd ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\to {x}\in \underset{{t}\in {A}}{⨉}\bigcup {F}\left({t}\right)$
19 vex ${⊢}{x}\in \mathrm{V}$
20 19 elixp ${⊢}{x}\in \underset{{t}\in {A}}{⨉}\bigcup {F}\left({t}\right)↔\left({x}Fn{A}\wedge \forall {t}\in {A}\phantom{\rule{.4em}{0ex}}{x}\left({t}\right)\in \bigcup {F}\left({t}\right)\right)$
21 18 20 sylib ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\to \left({x}Fn{A}\wedge \forall {t}\in {A}\phantom{\rule{.4em}{0ex}}{x}\left({t}\right)\in \bigcup {F}\left({t}\right)\right)$
22 21 simprd ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\to \forall {t}\in {A}\phantom{\rule{.4em}{0ex}}{x}\left({t}\right)\in \bigcup {F}\left({t}\right)$
23 22 r19.21bi ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge {t}\in {A}\right)\to {x}\left({t}\right)\in \bigcup {F}\left({t}\right)$
24 simprr ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\to {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)$
25 24 17 eleqtrrd ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\to {y}\in \underset{{t}\in {A}}{⨉}\bigcup {F}\left({t}\right)$
26 vex ${⊢}{y}\in \mathrm{V}$
27 26 elixp ${⊢}{y}\in \underset{{t}\in {A}}{⨉}\bigcup {F}\left({t}\right)↔\left({y}Fn{A}\wedge \forall {t}\in {A}\phantom{\rule{.4em}{0ex}}{y}\left({t}\right)\in \bigcup {F}\left({t}\right)\right)$
28 25 27 sylib ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\to \left({y}Fn{A}\wedge \forall {t}\in {A}\phantom{\rule{.4em}{0ex}}{y}\left({t}\right)\in \bigcup {F}\left({t}\right)\right)$
29 28 simprd ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\to \forall {t}\in {A}\phantom{\rule{.4em}{0ex}}{y}\left({t}\right)\in \bigcup {F}\left({t}\right)$
30 29 r19.21bi ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge {t}\in {A}\right)\to {y}\left({t}\right)\in \bigcup {F}\left({t}\right)$
31 eqid ${⊢}\bigcup {F}\left({t}\right)=\bigcup {F}\left({t}\right)$
32 31 pconncn ${⊢}\left({F}\left({t}\right)\in \mathrm{PConn}\wedge {x}\left({t}\right)\in \bigcup {F}\left({t}\right)\wedge {y}\left({t}\right)\in \bigcup {F}\left({t}\right)\right)\to \exists {f}\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}\left({f}\left(0\right)={x}\left({t}\right)\wedge {f}\left(1\right)={y}\left({t}\right)\right)$
33 12 23 30 32 syl3anc ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge {t}\in {A}\right)\to \exists {f}\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}\left({f}\left(0\right)={x}\left({t}\right)\wedge {f}\left(1\right)={y}\left({t}\right)\right)$
34 df-rex ${⊢}\exists {f}\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\phantom{\rule{.4em}{0ex}}\left({f}\left(0\right)={x}\left({t}\right)\wedge {f}\left(1\right)={y}\left({t}\right)\right)↔\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({f}\left(0\right)={x}\left({t}\right)\wedge {f}\left(1\right)={y}\left({t}\right)\right)\right)$
35 33 34 sylib ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge {t}\in {A}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({f}\left(0\right)={x}\left({t}\right)\wedge {f}\left(1\right)={y}\left({t}\right)\right)\right)$
36 10 35 syldan ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge {t}\in \mathrm{I}\left({A}\right)\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({f}\left(0\right)={x}\left({t}\right)\wedge {f}\left(1\right)={y}\left({t}\right)\right)\right)$
37 36 ralrimiva ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\to \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({f}\left(0\right)={x}\left({t}\right)\wedge {f}\left(1\right)={y}\left({t}\right)\right)\right)$
38 fvex ${⊢}\mathrm{I}\left({A}\right)\in \mathrm{V}$
39 eleq1 ${⊢}{f}={g}\left({t}\right)\to \left({f}\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)↔{g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\right)$
40 fveq1 ${⊢}{f}={g}\left({t}\right)\to {f}\left(0\right)={g}\left({t}\right)\left(0\right)$
41 40 eqeq1d ${⊢}{f}={g}\left({t}\right)\to \left({f}\left(0\right)={x}\left({t}\right)↔{g}\left({t}\right)\left(0\right)={x}\left({t}\right)\right)$
42 fveq1 ${⊢}{f}={g}\left({t}\right)\to {f}\left(1\right)={g}\left({t}\right)\left(1\right)$
43 42 eqeq1d ${⊢}{f}={g}\left({t}\right)\to \left({f}\left(1\right)={y}\left({t}\right)↔{g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)$
44 41 43 anbi12d ${⊢}{f}={g}\left({t}\right)\to \left(\left({f}\left(0\right)={x}\left({t}\right)\wedge {f}\left(1\right)={y}\left({t}\right)\right)↔\left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)$
45 39 44 anbi12d ${⊢}{f}={g}\left({t}\right)\to \left(\left({f}\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({f}\left(0\right)={x}\left({t}\right)\wedge {f}\left(1\right)={y}\left({t}\right)\right)\right)↔\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)$
46 38 45 ac6s2 ${⊢}\forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({f}\left(0\right)={x}\left({t}\right)\wedge {f}\left(1\right)={y}\left({t}\right)\right)\right)\to \exists {g}\phantom{\rule{.4em}{0ex}}\left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)$
47 37 46 syl ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\to \exists {g}\phantom{\rule{.4em}{0ex}}\left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)$
48 iitopon ${⊢}\mathrm{II}\in \mathrm{TopOn}\left(\left[0,1\right]\right)$
49 48 a1i ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge \left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)\right)\to \mathrm{II}\in \mathrm{TopOn}\left(\left[0,1\right]\right)$
50 simplll ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge \left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)\right)\to {A}\in {V}$
51 11 adantr ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge \left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)\right)\to {F}:{A}⟶\mathrm{PConn}$
52 51 4 syl ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge \left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)\right)\to {F}:{A}⟶\mathrm{Top}$
53 8 adantr ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge \left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)\right)\to \mathrm{I}\left({A}\right)={A}$
54 53 eleq2d ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge \left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)\right)\to \left({i}\in \mathrm{I}\left({A}\right)↔{i}\in {A}\right)$
55 54 biimpar ${⊢}\left(\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge \left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)\right)\wedge {i}\in {A}\right)\to {i}\in \mathrm{I}\left({A}\right)$
56 simprr ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge \left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)\right)\to \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)$
57 fveq2 ${⊢}{t}={i}\to {g}\left({t}\right)={g}\left({i}\right)$
58 fveq2 ${⊢}{t}={i}\to {F}\left({t}\right)={F}\left({i}\right)$
59 58 oveq2d ${⊢}{t}={i}\to \mathrm{II}\mathrm{Cn}{F}\left({t}\right)=\mathrm{II}\mathrm{Cn}{F}\left({i}\right)$
60 57 59 eleq12d ${⊢}{t}={i}\to \left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)↔{g}\left({i}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({i}\right)\right)\right)$
61 57 fveq1d ${⊢}{t}={i}\to {g}\left({t}\right)\left(0\right)={g}\left({i}\right)\left(0\right)$
62 fveq2 ${⊢}{t}={i}\to {x}\left({t}\right)={x}\left({i}\right)$
63 61 62 eqeq12d ${⊢}{t}={i}\to \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)↔{g}\left({i}\right)\left(0\right)={x}\left({i}\right)\right)$
64 57 fveq1d ${⊢}{t}={i}\to {g}\left({t}\right)\left(1\right)={g}\left({i}\right)\left(1\right)$
65 fveq2 ${⊢}{t}={i}\to {y}\left({t}\right)={y}\left({i}\right)$
66 64 65 eqeq12d ${⊢}{t}={i}\to \left({g}\left({t}\right)\left(1\right)={y}\left({t}\right)↔{g}\left({i}\right)\left(1\right)={y}\left({i}\right)\right)$
67 63 66 anbi12d ${⊢}{t}={i}\to \left(\left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)↔\left({g}\left({i}\right)\left(0\right)={x}\left({i}\right)\wedge {g}\left({i}\right)\left(1\right)={y}\left({i}\right)\right)\right)$
68 60 67 anbi12d ${⊢}{t}={i}\to \left(\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)↔\left({g}\left({i}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({i}\right)\right)\wedge \left({g}\left({i}\right)\left(0\right)={x}\left({i}\right)\wedge {g}\left({i}\right)\left(1\right)={y}\left({i}\right)\right)\right)\right)$
69 68 rspccva ${⊢}\left(\forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\wedge {i}\in \mathrm{I}\left({A}\right)\right)\to \left({g}\left({i}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({i}\right)\right)\wedge \left({g}\left({i}\right)\left(0\right)={x}\left({i}\right)\wedge {g}\left({i}\right)\left(1\right)={y}\left({i}\right)\right)\right)$
70 56 69 sylan ${⊢}\left(\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge \left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)\right)\wedge {i}\in \mathrm{I}\left({A}\right)\right)\to \left({g}\left({i}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({i}\right)\right)\wedge \left({g}\left({i}\right)\left(0\right)={x}\left({i}\right)\wedge {g}\left({i}\right)\left(1\right)={y}\left({i}\right)\right)\right)$
71 55 70 syldan ${⊢}\left(\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge \left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)\right)\wedge {i}\in {A}\right)\to \left({g}\left({i}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({i}\right)\right)\wedge \left({g}\left({i}\right)\left(0\right)={x}\left({i}\right)\wedge {g}\left({i}\right)\left(1\right)={y}\left({i}\right)\right)\right)$
72 71 simpld ${⊢}\left(\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge \left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)\right)\wedge {i}\in {A}\right)\to {g}\left({i}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({i}\right)\right)$
73 iiuni ${⊢}\left[0,1\right]=\bigcup \mathrm{II}$
74 eqid ${⊢}\bigcup {F}\left({i}\right)=\bigcup {F}\left({i}\right)$
75 73 74 cnf ${⊢}{g}\left({i}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({i}\right)\right)\to {g}\left({i}\right):\left[0,1\right]⟶\bigcup {F}\left({i}\right)$
76 72 75 syl ${⊢}\left(\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge \left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)\right)\wedge {i}\in {A}\right)\to {g}\left({i}\right):\left[0,1\right]⟶\bigcup {F}\left({i}\right)$
77 76 feqmptd ${⊢}\left(\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge \left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)\right)\wedge {i}\in {A}\right)\to {g}\left({i}\right)=\left({z}\in \left[0,1\right]⟼{g}\left({i}\right)\left({z}\right)\right)$
78 77 72 eqeltrrd ${⊢}\left(\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge \left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)\right)\wedge {i}\in {A}\right)\to \left({z}\in \left[0,1\right]⟼{g}\left({i}\right)\left({z}\right)\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({i}\right)\right)$
79 14 49 50 52 78 ptcn ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge \left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)\right)\to \left({z}\in \left[0,1\right]⟼\left({i}\in {A}⟼{g}\left({i}\right)\left({z}\right)\right)\right)\in \left(\mathrm{II}\mathrm{Cn}{\prod }_{𝑡}\left({F}\right)\right)$
80 71 simprd ${⊢}\left(\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge \left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)\right)\wedge {i}\in {A}\right)\to \left({g}\left({i}\right)\left(0\right)={x}\left({i}\right)\wedge {g}\left({i}\right)\left(1\right)={y}\left({i}\right)\right)$
81 80 simpld ${⊢}\left(\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge \left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)\right)\wedge {i}\in {A}\right)\to {g}\left({i}\right)\left(0\right)={x}\left({i}\right)$
82 81 mpteq2dva ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge \left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)\right)\to \left({i}\in {A}⟼{g}\left({i}\right)\left(0\right)\right)=\left({i}\in {A}⟼{x}\left({i}\right)\right)$
83 0elunit ${⊢}0\in \left[0,1\right]$
84 mptexg ${⊢}{A}\in {V}\to \left({i}\in {A}⟼{g}\left({i}\right)\left(0\right)\right)\in \mathrm{V}$
85 50 84 syl ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge \left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)\right)\to \left({i}\in {A}⟼{g}\left({i}\right)\left(0\right)\right)\in \mathrm{V}$
86 fveq2 ${⊢}{z}=0\to {g}\left({i}\right)\left({z}\right)={g}\left({i}\right)\left(0\right)$
87 86 mpteq2dv ${⊢}{z}=0\to \left({i}\in {A}⟼{g}\left({i}\right)\left({z}\right)\right)=\left({i}\in {A}⟼{g}\left({i}\right)\left(0\right)\right)$
88 eqid ${⊢}\left({z}\in \left[0,1\right]⟼\left({i}\in {A}⟼{g}\left({i}\right)\left({z}\right)\right)\right)=\left({z}\in \left[0,1\right]⟼\left({i}\in {A}⟼{g}\left({i}\right)\left({z}\right)\right)\right)$
89 87 88 fvmptg ${⊢}\left(0\in \left[0,1\right]\wedge \left({i}\in {A}⟼{g}\left({i}\right)\left(0\right)\right)\in \mathrm{V}\right)\to \left({z}\in \left[0,1\right]⟼\left({i}\in {A}⟼{g}\left({i}\right)\left({z}\right)\right)\right)\left(0\right)=\left({i}\in {A}⟼{g}\left({i}\right)\left(0\right)\right)$
90 83 85 89 sylancr ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge \left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)\right)\to \left({z}\in \left[0,1\right]⟼\left({i}\in {A}⟼{g}\left({i}\right)\left({z}\right)\right)\right)\left(0\right)=\left({i}\in {A}⟼{g}\left({i}\right)\left(0\right)\right)$
91 21 simpld ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\to {x}Fn{A}$
92 91 adantr ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge \left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)\right)\to {x}Fn{A}$
93 dffn5 ${⊢}{x}Fn{A}↔{x}=\left({i}\in {A}⟼{x}\left({i}\right)\right)$
94 92 93 sylib ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge \left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)\right)\to {x}=\left({i}\in {A}⟼{x}\left({i}\right)\right)$
95 82 90 94 3eqtr4d ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge \left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)\right)\to \left({z}\in \left[0,1\right]⟼\left({i}\in {A}⟼{g}\left({i}\right)\left({z}\right)\right)\right)\left(0\right)={x}$
96 80 simprd ${⊢}\left(\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge \left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)\right)\wedge {i}\in {A}\right)\to {g}\left({i}\right)\left(1\right)={y}\left({i}\right)$
97 96 mpteq2dva ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge \left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)\right)\to \left({i}\in {A}⟼{g}\left({i}\right)\left(1\right)\right)=\left({i}\in {A}⟼{y}\left({i}\right)\right)$
98 1elunit ${⊢}1\in \left[0,1\right]$
99 mptexg ${⊢}{A}\in {V}\to \left({i}\in {A}⟼{g}\left({i}\right)\left(1\right)\right)\in \mathrm{V}$
100 50 99 syl ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge \left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)\right)\to \left({i}\in {A}⟼{g}\left({i}\right)\left(1\right)\right)\in \mathrm{V}$
101 fveq2 ${⊢}{z}=1\to {g}\left({i}\right)\left({z}\right)={g}\left({i}\right)\left(1\right)$
102 101 mpteq2dv ${⊢}{z}=1\to \left({i}\in {A}⟼{g}\left({i}\right)\left({z}\right)\right)=\left({i}\in {A}⟼{g}\left({i}\right)\left(1\right)\right)$
103 102 88 fvmptg ${⊢}\left(1\in \left[0,1\right]\wedge \left({i}\in {A}⟼{g}\left({i}\right)\left(1\right)\right)\in \mathrm{V}\right)\to \left({z}\in \left[0,1\right]⟼\left({i}\in {A}⟼{g}\left({i}\right)\left({z}\right)\right)\right)\left(1\right)=\left({i}\in {A}⟼{g}\left({i}\right)\left(1\right)\right)$
104 98 100 103 sylancr ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge \left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)\right)\to \left({z}\in \left[0,1\right]⟼\left({i}\in {A}⟼{g}\left({i}\right)\left({z}\right)\right)\right)\left(1\right)=\left({i}\in {A}⟼{g}\left({i}\right)\left(1\right)\right)$
105 28 simpld ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\to {y}Fn{A}$
106 105 adantr ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge \left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)\right)\to {y}Fn{A}$
107 dffn5 ${⊢}{y}Fn{A}↔{y}=\left({i}\in {A}⟼{y}\left({i}\right)\right)$
108 106 107 sylib ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge \left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)\right)\to {y}=\left({i}\in {A}⟼{y}\left({i}\right)\right)$
109 97 104 108 3eqtr4d ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge \left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)\right)\to \left({z}\in \left[0,1\right]⟼\left({i}\in {A}⟼{g}\left({i}\right)\left({z}\right)\right)\right)\left(1\right)={y}$
110 fveq1 ${⊢}{f}=\left({z}\in \left[0,1\right]⟼\left({i}\in {A}⟼{g}\left({i}\right)\left({z}\right)\right)\right)\to {f}\left(0\right)=\left({z}\in \left[0,1\right]⟼\left({i}\in {A}⟼{g}\left({i}\right)\left({z}\right)\right)\right)\left(0\right)$
111 110 eqeq1d ${⊢}{f}=\left({z}\in \left[0,1\right]⟼\left({i}\in {A}⟼{g}\left({i}\right)\left({z}\right)\right)\right)\to \left({f}\left(0\right)={x}↔\left({z}\in \left[0,1\right]⟼\left({i}\in {A}⟼{g}\left({i}\right)\left({z}\right)\right)\right)\left(0\right)={x}\right)$
112 fveq1 ${⊢}{f}=\left({z}\in \left[0,1\right]⟼\left({i}\in {A}⟼{g}\left({i}\right)\left({z}\right)\right)\right)\to {f}\left(1\right)=\left({z}\in \left[0,1\right]⟼\left({i}\in {A}⟼{g}\left({i}\right)\left({z}\right)\right)\right)\left(1\right)$
113 112 eqeq1d ${⊢}{f}=\left({z}\in \left[0,1\right]⟼\left({i}\in {A}⟼{g}\left({i}\right)\left({z}\right)\right)\right)\to \left({f}\left(1\right)={y}↔\left({z}\in \left[0,1\right]⟼\left({i}\in {A}⟼{g}\left({i}\right)\left({z}\right)\right)\right)\left(1\right)={y}\right)$
114 111 113 anbi12d ${⊢}{f}=\left({z}\in \left[0,1\right]⟼\left({i}\in {A}⟼{g}\left({i}\right)\left({z}\right)\right)\right)\to \left(\left({f}\left(0\right)={x}\wedge {f}\left(1\right)={y}\right)↔\left(\left({z}\in \left[0,1\right]⟼\left({i}\in {A}⟼{g}\left({i}\right)\left({z}\right)\right)\right)\left(0\right)={x}\wedge \left({z}\in \left[0,1\right]⟼\left({i}\in {A}⟼{g}\left({i}\right)\left({z}\right)\right)\right)\left(1\right)={y}\right)\right)$
115 114 rspcev ${⊢}\left(\left({z}\in \left[0,1\right]⟼\left({i}\in {A}⟼{g}\left({i}\right)\left({z}\right)\right)\right)\in \left(\mathrm{II}\mathrm{Cn}{\prod }_{𝑡}\left({F}\right)\right)\wedge \left(\left({z}\in \left[0,1\right]⟼\left({i}\in {A}⟼{g}\left({i}\right)\left({z}\right)\right)\right)\left(0\right)={x}\wedge \left({z}\in \left[0,1\right]⟼\left({i}\in {A}⟼{g}\left({i}\right)\left({z}\right)\right)\right)\left(1\right)={y}\right)\right)\to \exists {f}\in \left(\mathrm{II}\mathrm{Cn}{\prod }_{𝑡}\left({F}\right)\right)\phantom{\rule{.4em}{0ex}}\left({f}\left(0\right)={x}\wedge {f}\left(1\right)={y}\right)$
116 79 95 109 115 syl12anc ${⊢}\left(\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\wedge \left({g}Fn\mathrm{I}\left({A}\right)\wedge \forall {t}\in \mathrm{I}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({g}\left({t}\right)\in \left(\mathrm{II}\mathrm{Cn}{F}\left({t}\right)\right)\wedge \left({g}\left({t}\right)\left(0\right)={x}\left({t}\right)\wedge {g}\left({t}\right)\left(1\right)={y}\left({t}\right)\right)\right)\right)\right)\to \exists {f}\in \left(\mathrm{II}\mathrm{Cn}{\prod }_{𝑡}\left({F}\right)\right)\phantom{\rule{.4em}{0ex}}\left({f}\left(0\right)={x}\wedge {f}\left(1\right)={y}\right)$
117 47 116 exlimddv ${⊢}\left(\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\wedge \left({x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\wedge {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\right)\right)\to \exists {f}\in \left(\mathrm{II}\mathrm{Cn}{\prod }_{𝑡}\left({F}\right)\right)\phantom{\rule{.4em}{0ex}}\left({f}\left(0\right)={x}\wedge {f}\left(1\right)={y}\right)$
118 117 ralrimivva ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\to \forall {x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\in \left(\mathrm{II}\mathrm{Cn}{\prod }_{𝑡}\left({F}\right)\right)\phantom{\rule{.4em}{0ex}}\left({f}\left(0\right)={x}\wedge {f}\left(1\right)={y}\right)$
119 eqid ${⊢}\bigcup {\prod }_{𝑡}\left({F}\right)=\bigcup {\prod }_{𝑡}\left({F}\right)$
120 119 ispconn ${⊢}{\prod }_{𝑡}\left({F}\right)\in \mathrm{PConn}↔\left({\prod }_{𝑡}\left({F}\right)\in \mathrm{Top}\wedge \forall {x}\in \bigcup {\prod }_{𝑡}\left({F}\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in \bigcup {\prod }_{𝑡}\left({F}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\in \left(\mathrm{II}\mathrm{Cn}{\prod }_{𝑡}\left({F}\right)\right)\phantom{\rule{.4em}{0ex}}\left({f}\left(0\right)={x}\wedge {f}\left(1\right)={y}\right)\right)$
121 6 118 120 sylanbrc ${⊢}\left({A}\in {V}\wedge {F}:{A}⟶\mathrm{PConn}\right)\to {\prod }_{𝑡}\left({F}\right)\in \mathrm{PConn}$