Theorem phtpycn

Description: A path homotopy is a continuous function. (Contributed by Mario Carneiro, 23-Feb-2015)

	Ref	Expression
Hypotheses	isphtpy.2	⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
	isphtpy.3	⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
Assertion	phtpycn	⊢ ( 𝜑 → ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ⊆ ( ( II ×t II ) Cn 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		isphtpy.2	⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
2		isphtpy.3	⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
3	1 2	phtpyhtpy	⊢ ( 𝜑 → ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ⊆ ( 𝐹 ( II Htpy 𝐽 ) 𝐺 ) )
4		iitopon	⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
5	4	a1i	⊢ ( 𝜑 → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
6	5 1 2	htpycn	⊢ ( 𝜑 → ( 𝐹 ( II Htpy 𝐽 ) 𝐺 ) ⊆ ( ( II ×t II ) Cn 𝐽 ) )
7	3 6	sstrd	⊢ ( 𝜑 → ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ⊆ ( ( II ×t II ) Cn 𝐽 ) )