# 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 𝐺 = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝐹𝑥 ) )
phtpyid.3 ( 𝜑𝐹 ∈ ( II Cn 𝐽 ) )
Assertion phtpyid ( 𝜑𝐺 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐹 ) )

### Proof

Step Hyp Ref Expression
1 phtpyid.1 𝐺 = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝐹𝑥 ) )
2 phtpyid.3 ( 𝜑𝐹 ∈ ( II Cn 𝐽 ) )
3 iitopon II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
4 3 a1i ( 𝜑 → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
5 1 4 2 htpyid ( 𝜑𝐺 ∈ ( 𝐹 ( II Htpy 𝐽 ) 𝐹 ) )
6 0elunit 0 ∈ ( 0 [,] 1 )
7 fveq2 ( 𝑥 = 0 → ( 𝐹𝑥 ) = ( 𝐹 ‘ 0 ) )
8 eqidd ( 𝑦 = 𝑠 → ( 𝐹 ‘ 0 ) = ( 𝐹 ‘ 0 ) )
9 fvex ( 𝐹 ‘ 0 ) ∈ V
10 7 8 1 9 ovmpo ( ( 0 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 0 𝐺 𝑠 ) = ( 𝐹 ‘ 0 ) )
11 6 10 mpan ( 𝑠 ∈ ( 0 [,] 1 ) → ( 0 𝐺 𝑠 ) = ( 𝐹 ‘ 0 ) )
12 11 adantl ( ( 𝜑𝑠 ∈ ( 0 [,] 1 ) ) → ( 0 𝐺 𝑠 ) = ( 𝐹 ‘ 0 ) )
13 1elunit 1 ∈ ( 0 [,] 1 )
14 fveq2 ( 𝑥 = 1 → ( 𝐹𝑥 ) = ( 𝐹 ‘ 1 ) )
15 eqidd ( 𝑦 = 𝑠 → ( 𝐹 ‘ 1 ) = ( 𝐹 ‘ 1 ) )
16 fvex ( 𝐹 ‘ 1 ) ∈ V
17 14 15 1 16 ovmpo ( ( 1 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 𝐺 𝑠 ) = ( 𝐹 ‘ 1 ) )
18 13 17 mpan ( 𝑠 ∈ ( 0 [,] 1 ) → ( 1 𝐺 𝑠 ) = ( 𝐹 ‘ 1 ) )
19 18 adantl ( ( 𝜑𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 𝐺 𝑠 ) = ( 𝐹 ‘ 1 ) )
20 2 2 5 12 19 isphtpyd ( 𝜑𝐺 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐹 ) )