Theorem htpycn

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

	Ref	Expression
Hypotheses	ishtpy.1	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
	ishtpy.3	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
	ishtpy.4	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐽 Cn 𝐾 ) )
Assertion	htpycn	⊢ ( 𝜑 → ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐺 ) ⊆ ( ( 𝐽 ×t II ) Cn 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		ishtpy.1	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2		ishtpy.3	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
3		ishtpy.4	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐽 Cn 𝐾 ) )
4	1 2 3	ishtpy	⊢ ( 𝜑 → ( ℎ ∈ ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐺 ) ↔ ( ℎ ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) ∧ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 ℎ 0 ) = ( 𝐹 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝐺 ‘ 𝑠 ) ) ) ) )
5		simpl	⊢ ( ( ℎ ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) ∧ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 ℎ 0 ) = ( 𝐹 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝐺 ‘ 𝑠 ) ) ) → ℎ ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) )
6	4 5	biimtrdi	⊢ ( 𝜑 → ( ℎ ∈ ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐺 ) → ℎ ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) ) )
7	6	ssrdv	⊢ ( 𝜑 → ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐺 ) ⊆ ( ( 𝐽 ×t II ) Cn 𝐾 ) )