phtpyhtpy

Description: A path homotopy is a homotopy. (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	phtpyhtpy	$⊢ φ \to F PHtpy (J) G \subseteq F (II Htpy J) G$

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	isphtpy	$⊢ φ \to (h \in (F PHtpy (J) G) \leftrightarrow (h \in (F (II Htpy J) G) \land \forall s \in [0, 1] (0 h s = F (0) \land 1 h s = F (1))))$
4		simpl	$⊢ (h \in (F (II Htpy J) G) \land \forall s \in [0, 1] (0 h s = F (0) \land 1 h s = F (1))) \to h \in (F (II Htpy J) G)$
5	3 4	syl6bi	$⊢ φ \to (h \in (F PHtpy (J) G) \to h \in (F (II Htpy J) G))$
6	5	ssrdv	$⊢ φ \to F PHtpy (J) G \subseteq F (II Htpy J) G$

Metamath Proof Explorer