Metamath Proof Explorer

Theorem phtpycn

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

	Ref	Expression
Hypotheses	isphtpy.2	$⊢ φ \to F \in (II Cn J)$
	isphtpy.3	$⊢ φ \to G \in (II Cn J)$
Assertion	phtpycn	$⊢ φ \to F PHtpy (J) G \subseteq (II \times_{t} II) Cn J$

Step	Hyp	Ref	Expression
1		isphtpy.2	$⊢ φ \to F \in (II Cn J)$
2		isphtpy.3	$⊢ φ \to G \in (II Cn J)$
3	1 2	phtpyhtpy	$⊢ φ \to F PHtpy (J) G \subseteq F (II Htpy J) G$
4		iitopon	$⊢ II \in TopOn ([0, 1])$
5	4	a1i	$⊢ φ \to II \in TopOn ([0, 1])$
6	5 1 2	htpycn	$⊢ φ \to F (II Htpy J) G \subseteq (II \times_{t} II) Cn J$
7	3 6	sstrd	$⊢ φ \to F PHtpy (J) G \subseteq (II \times_{t} II) Cn J$