Theorem htpyid

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

	Ref	Expression
Hypotheses	htpyid.1	⊢ 𝐺 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ 𝑥 ) )
	htpyid.2	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
	htpyid.4	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
Assertion	htpyid	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		htpyid.1	⊢ 𝐺 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ 𝑥 ) )
2		htpyid.2	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3		htpyid.4	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
4		iitopon	⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
5	4	a1i	⊢ ( 𝜑 → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
6	2 5	cnmpt1st	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 0 [,] 1 ) ↦ 𝑥 ) ∈ ( ( 𝐽 ×t II ) Cn 𝐽 ) )
7	2 5 6 3	cnmpt21f	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) )
8	1 7	eqeltrid	⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) )
9		simpr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → 𝑠 ∈ 𝑋 )
10		0elunit	⊢ 0 ∈ ( 0 [,] 1 )
11		fveq2	⊢ ( 𝑥 = 𝑠 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑠 ) )
12		eqidd	⊢ ( 𝑦 = 0 → ( 𝐹 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑠 ) )
13		fvex	⊢ ( 𝐹 ‘ 𝑠 ) ∈ V
14	11 12 1 13	ovmpo	⊢ ( ( 𝑠 ∈ 𝑋 ∧ 0 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝐺 0 ) = ( 𝐹 ‘ 𝑠 ) )
15	9 10 14	sylancl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑠 𝐺 0 ) = ( 𝐹 ‘ 𝑠 ) )
16		1elunit	⊢ 1 ∈ ( 0 [,] 1 )
17		eqidd	⊢ ( 𝑦 = 1 → ( 𝐹 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑠 ) )
18	11 17 1 13	ovmpo	⊢ ( ( 𝑠 ∈ 𝑋 ∧ 1 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝐺 1 ) = ( 𝐹 ‘ 𝑠 ) )
19	9 16 18	sylancl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑠 𝐺 1 ) = ( 𝐹 ‘ 𝑠 ) )
20	2 3 3 8 15 19	ishtpyd	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐹 ) )