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 ‘ 𝐽 ) 𝐹 ) )