Metamath Proof Explorer

Theorem phtpyid

Description: A homotopy from a path to itself. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 23-Feb-2015)

Ref Expression
Hypotheses phtpyid.1 ⊢G=x∈01,y∈01⟼F⁡x
phtpyid.3 ⊢φ→F∈IICnJ
Assertion phtpyid ⊢φ→G∈FPHtpy⁡JF

Proof

Step Hyp Ref Expression
1 phtpyid.1 ⊢G=x∈01,y∈01⟼F⁡x
2 phtpyid.3 ⊢φ→F∈IICnJ
3 iitopon ⊢II∈TopOn⁡01
4 3 a1i ⊢φ→II∈TopOn⁡01
5 1 4 2 htpyid ⊢φ→G∈FIIHtpyJF
6 0elunit ⊢0∈01
7 fveq2 ⊢x=0→F⁡x=F⁡0
8 eqidd ⊢y=s→F⁡0=F⁡0
9 fvex ⊢F⁡0∈V
10 7 8 1 9 ovmpo ⊢0∈01∧s∈01→0Gs=F⁡0
11 6 10 mpan ⊢s∈01→0Gs=F⁡0
12 11 adantl ⊢φ∧s∈01→0Gs=F⁡0
13 1elunit ⊢1∈01
14 fveq2 ⊢x=1→F⁡x=F⁡1
15 eqidd ⊢y=s→F⁡1=F⁡1
16 fvex ⊢F⁡1∈V
17 14 15 1 16 ovmpo ⊢1∈01∧s∈01→1Gs=F⁡1
18 13 17 mpan ⊢s∈01→1Gs=F⁡1
19 18 adantl ⊢φ∧s∈01→1Gs=F⁡1
20 2 2 5 12 19 isphtpyd ⊢φ→G∈FPHtpy⁡JF