# Metamath Proof Explorer

## Theorem isphtpy

Description: Membership in the class of path homotopies between two continuous functions. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 23-Feb-2015)

Ref Expression
Hypotheses isphtpy.2 ${⊢}{\phi }\to {F}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
isphtpy.3 ${⊢}{\phi }\to {G}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
Assertion isphtpy ${⊢}{\phi }\to \left({H}\in \left({F}\mathrm{PHtpy}\left({J}\right){G}\right)↔\left({H}\in \left({F}\left(\mathrm{II}\mathrm{Htpy}{J}\right){G}\right)\wedge \forall {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(0{H}{s}={F}\left(0\right)\wedge 1{H}{s}={F}\left(1\right)\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 isphtpy.2 ${⊢}{\phi }\to {F}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
2 isphtpy.3 ${⊢}{\phi }\to {G}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
3 cntop2 ${⊢}{F}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\to {J}\in \mathrm{Top}$
4 oveq2 ${⊢}{j}={J}\to \mathrm{II}\mathrm{Cn}{j}=\mathrm{II}\mathrm{Cn}{J}$
5 oveq2 ${⊢}{j}={J}\to \mathrm{II}\mathrm{Htpy}{j}=\mathrm{II}\mathrm{Htpy}{J}$
6 5 oveqd ${⊢}{j}={J}\to {f}\left(\mathrm{II}\mathrm{Htpy}{j}\right){g}={f}\left(\mathrm{II}\mathrm{Htpy}{J}\right){g}$
7 6 rabeqdv ${⊢}{j}={J}\to \left\{{h}\in \left({f}\left(\mathrm{II}\mathrm{Htpy}{j}\right){g}\right)|\forall {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(0{h}{s}={f}\left(0\right)\wedge 1{h}{s}={f}\left(1\right)\right)\right\}=\left\{{h}\in \left({f}\left(\mathrm{II}\mathrm{Htpy}{J}\right){g}\right)|\forall {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(0{h}{s}={f}\left(0\right)\wedge 1{h}{s}={f}\left(1\right)\right)\right\}$
8 4 4 7 mpoeq123dv ${⊢}{j}={J}\to \left({f}\in \left(\mathrm{II}\mathrm{Cn}{j}\right),{g}\in \left(\mathrm{II}\mathrm{Cn}{j}\right)⟼\left\{{h}\in \left({f}\left(\mathrm{II}\mathrm{Htpy}{j}\right){g}\right)|\forall {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(0{h}{s}={f}\left(0\right)\wedge 1{h}{s}={f}\left(1\right)\right)\right\}\right)=\left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right),{g}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)⟼\left\{{h}\in \left({f}\left(\mathrm{II}\mathrm{Htpy}{J}\right){g}\right)|\forall {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(0{h}{s}={f}\left(0\right)\wedge 1{h}{s}={f}\left(1\right)\right)\right\}\right)$
9 df-phtpy ${⊢}\mathrm{PHtpy}=\left({j}\in \mathrm{Top}⟼\left({f}\in \left(\mathrm{II}\mathrm{Cn}{j}\right),{g}\in \left(\mathrm{II}\mathrm{Cn}{j}\right)⟼\left\{{h}\in \left({f}\left(\mathrm{II}\mathrm{Htpy}{j}\right){g}\right)|\forall {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(0{h}{s}={f}\left(0\right)\wedge 1{h}{s}={f}\left(1\right)\right)\right\}\right)\right)$
10 ovex ${⊢}\mathrm{II}\mathrm{Cn}{J}\in \mathrm{V}$
11 10 10 mpoex ${⊢}\left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right),{g}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)⟼\left\{{h}\in \left({f}\left(\mathrm{II}\mathrm{Htpy}{J}\right){g}\right)|\forall {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(0{h}{s}={f}\left(0\right)\wedge 1{h}{s}={f}\left(1\right)\right)\right\}\right)\in \mathrm{V}$
12 8 9 11 fvmpt ${⊢}{J}\in \mathrm{Top}\to \mathrm{PHtpy}\left({J}\right)=\left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right),{g}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)⟼\left\{{h}\in \left({f}\left(\mathrm{II}\mathrm{Htpy}{J}\right){g}\right)|\forall {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(0{h}{s}={f}\left(0\right)\wedge 1{h}{s}={f}\left(1\right)\right)\right\}\right)$
13 1 3 12 3syl ${⊢}{\phi }\to \mathrm{PHtpy}\left({J}\right)=\left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right),{g}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)⟼\left\{{h}\in \left({f}\left(\mathrm{II}\mathrm{Htpy}{J}\right){g}\right)|\forall {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(0{h}{s}={f}\left(0\right)\wedge 1{h}{s}={f}\left(1\right)\right)\right\}\right)$
14 oveq12 ${⊢}\left({f}={F}\wedge {g}={G}\right)\to {f}\left(\mathrm{II}\mathrm{Htpy}{J}\right){g}={F}\left(\mathrm{II}\mathrm{Htpy}{J}\right){G}$
15 simpl ${⊢}\left({f}={F}\wedge {g}={G}\right)\to {f}={F}$
16 15 fveq1d ${⊢}\left({f}={F}\wedge {g}={G}\right)\to {f}\left(0\right)={F}\left(0\right)$
17 16 eqeq2d ${⊢}\left({f}={F}\wedge {g}={G}\right)\to \left(0{h}{s}={f}\left(0\right)↔0{h}{s}={F}\left(0\right)\right)$
18 15 fveq1d ${⊢}\left({f}={F}\wedge {g}={G}\right)\to {f}\left(1\right)={F}\left(1\right)$
19 18 eqeq2d ${⊢}\left({f}={F}\wedge {g}={G}\right)\to \left(1{h}{s}={f}\left(1\right)↔1{h}{s}={F}\left(1\right)\right)$
20 17 19 anbi12d ${⊢}\left({f}={F}\wedge {g}={G}\right)\to \left(\left(0{h}{s}={f}\left(0\right)\wedge 1{h}{s}={f}\left(1\right)\right)↔\left(0{h}{s}={F}\left(0\right)\wedge 1{h}{s}={F}\left(1\right)\right)\right)$
21 20 ralbidv ${⊢}\left({f}={F}\wedge {g}={G}\right)\to \left(\forall {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(0{h}{s}={f}\left(0\right)\wedge 1{h}{s}={f}\left(1\right)\right)↔\forall {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(0{h}{s}={F}\left(0\right)\wedge 1{h}{s}={F}\left(1\right)\right)\right)$
22 14 21 rabeqbidv ${⊢}\left({f}={F}\wedge {g}={G}\right)\to \left\{{h}\in \left({f}\left(\mathrm{II}\mathrm{Htpy}{J}\right){g}\right)|\forall {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(0{h}{s}={f}\left(0\right)\wedge 1{h}{s}={f}\left(1\right)\right)\right\}=\left\{{h}\in \left({F}\left(\mathrm{II}\mathrm{Htpy}{J}\right){G}\right)|\forall {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(0{h}{s}={F}\left(0\right)\wedge 1{h}{s}={F}\left(1\right)\right)\right\}$
23 22 adantl ${⊢}\left({\phi }\wedge \left({f}={F}\wedge {g}={G}\right)\right)\to \left\{{h}\in \left({f}\left(\mathrm{II}\mathrm{Htpy}{J}\right){g}\right)|\forall {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(0{h}{s}={f}\left(0\right)\wedge 1{h}{s}={f}\left(1\right)\right)\right\}=\left\{{h}\in \left({F}\left(\mathrm{II}\mathrm{Htpy}{J}\right){G}\right)|\forall {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(0{h}{s}={F}\left(0\right)\wedge 1{h}{s}={F}\left(1\right)\right)\right\}$
24 ovex ${⊢}{F}\left(\mathrm{II}\mathrm{Htpy}{J}\right){G}\in \mathrm{V}$
25 24 rabex ${⊢}\left\{{h}\in \left({F}\left(\mathrm{II}\mathrm{Htpy}{J}\right){G}\right)|\forall {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(0{h}{s}={F}\left(0\right)\wedge 1{h}{s}={F}\left(1\right)\right)\right\}\in \mathrm{V}$
26 25 a1i ${⊢}{\phi }\to \left\{{h}\in \left({F}\left(\mathrm{II}\mathrm{Htpy}{J}\right){G}\right)|\forall {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(0{h}{s}={F}\left(0\right)\wedge 1{h}{s}={F}\left(1\right)\right)\right\}\in \mathrm{V}$
27 13 23 1 2 26 ovmpod ${⊢}{\phi }\to {F}\mathrm{PHtpy}\left({J}\right){G}=\left\{{h}\in \left({F}\left(\mathrm{II}\mathrm{Htpy}{J}\right){G}\right)|\forall {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(0{h}{s}={F}\left(0\right)\wedge 1{h}{s}={F}\left(1\right)\right)\right\}$
28 27 eleq2d ${⊢}{\phi }\to \left({H}\in \left({F}\mathrm{PHtpy}\left({J}\right){G}\right)↔{H}\in \left\{{h}\in \left({F}\left(\mathrm{II}\mathrm{Htpy}{J}\right){G}\right)|\forall {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(0{h}{s}={F}\left(0\right)\wedge 1{h}{s}={F}\left(1\right)\right)\right\}\right)$
29 oveq ${⊢}{h}={H}\to 0{h}{s}=0{H}{s}$
30 29 eqeq1d ${⊢}{h}={H}\to \left(0{h}{s}={F}\left(0\right)↔0{H}{s}={F}\left(0\right)\right)$
31 oveq ${⊢}{h}={H}\to 1{h}{s}=1{H}{s}$
32 31 eqeq1d ${⊢}{h}={H}\to \left(1{h}{s}={F}\left(1\right)↔1{H}{s}={F}\left(1\right)\right)$
33 30 32 anbi12d ${⊢}{h}={H}\to \left(\left(0{h}{s}={F}\left(0\right)\wedge 1{h}{s}={F}\left(1\right)\right)↔\left(0{H}{s}={F}\left(0\right)\wedge 1{H}{s}={F}\left(1\right)\right)\right)$
34 33 ralbidv ${⊢}{h}={H}\to \left(\forall {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(0{h}{s}={F}\left(0\right)\wedge 1{h}{s}={F}\left(1\right)\right)↔\forall {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(0{H}{s}={F}\left(0\right)\wedge 1{H}{s}={F}\left(1\right)\right)\right)$
35 34 elrab ${⊢}{H}\in \left\{{h}\in \left({F}\left(\mathrm{II}\mathrm{Htpy}{J}\right){G}\right)|\forall {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(0{h}{s}={F}\left(0\right)\wedge 1{h}{s}={F}\left(1\right)\right)\right\}↔\left({H}\in \left({F}\left(\mathrm{II}\mathrm{Htpy}{J}\right){G}\right)\wedge \forall {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(0{H}{s}={F}\left(0\right)\wedge 1{H}{s}={F}\left(1\right)\right)\right)$
36 28 35 syl6bb ${⊢}{\phi }\to \left({H}\in \left({F}\mathrm{PHtpy}\left({J}\right){G}\right)↔\left({H}\in \left({F}\left(\mathrm{II}\mathrm{Htpy}{J}\right){G}\right)\wedge \forall {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(0{H}{s}={F}\left(0\right)\wedge 1{H}{s}={F}\left(1\right)\right)\right)\right)$