# Metamath Proof Explorer

## Theorem htpyid

Description: A homotopy from a function to itself. (Contributed by Mario Carneiro, 23-Feb-2015)

Ref Expression
Hypotheses htpyid.1 ${⊢}{G}=\left({x}\in {X},{y}\in \left[0,1\right]⟼{F}\left({x}\right)\right)$
htpyid.2 ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
htpyid.4 ${⊢}{\phi }\to {F}\in \left({J}\mathrm{Cn}{K}\right)$
Assertion htpyid ${⊢}{\phi }\to {G}\in \left({F}\left({J}\mathrm{Htpy}{K}\right){F}\right)$

### Proof

Step Hyp Ref Expression
1 htpyid.1 ${⊢}{G}=\left({x}\in {X},{y}\in \left[0,1\right]⟼{F}\left({x}\right)\right)$
2 htpyid.2 ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
3 htpyid.4 ${⊢}{\phi }\to {F}\in \left({J}\mathrm{Cn}{K}\right)$
4 iitopon ${⊢}\mathrm{II}\in \mathrm{TopOn}\left(\left[0,1\right]\right)$
5 4 a1i ${⊢}{\phi }\to \mathrm{II}\in \mathrm{TopOn}\left(\left[0,1\right]\right)$
6 2 5 cnmpt1st ${⊢}{\phi }\to \left({x}\in {X},{y}\in \left[0,1\right]⟼{x}\right)\in \left(\left({J}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{J}\right)$
7 2 5 6 3 cnmpt21f ${⊢}{\phi }\to \left({x}\in {X},{y}\in \left[0,1\right]⟼{F}\left({x}\right)\right)\in \left(\left({J}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{K}\right)$
8 1 7 eqeltrid ${⊢}{\phi }\to {G}\in \left(\left({J}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{K}\right)$
9 simpr ${⊢}\left({\phi }\wedge {s}\in {X}\right)\to {s}\in {X}$
10 0elunit ${⊢}0\in \left[0,1\right]$
11 fveq2 ${⊢}{x}={s}\to {F}\left({x}\right)={F}\left({s}\right)$
12 eqidd ${⊢}{y}=0\to {F}\left({s}\right)={F}\left({s}\right)$
13 fvex ${⊢}{F}\left({s}\right)\in \mathrm{V}$
14 11 12 1 13 ovmpo ${⊢}\left({s}\in {X}\wedge 0\in \left[0,1\right]\right)\to {s}{G}0={F}\left({s}\right)$
15 9 10 14 sylancl ${⊢}\left({\phi }\wedge {s}\in {X}\right)\to {s}{G}0={F}\left({s}\right)$
16 1elunit ${⊢}1\in \left[0,1\right]$
17 eqidd ${⊢}{y}=1\to {F}\left({s}\right)={F}\left({s}\right)$
18 11 17 1 13 ovmpo ${⊢}\left({s}\in {X}\wedge 1\in \left[0,1\right]\right)\to {s}{G}1={F}\left({s}\right)$
19 9 16 18 sylancl ${⊢}\left({\phi }\wedge {s}\in {X}\right)\to {s}{G}1={F}\left({s}\right)$
20 2 3 3 8 15 19 ishtpyd ${⊢}{\phi }\to {G}\in \left({F}\left({J}\mathrm{Htpy}{K}\right){F}\right)$