htpyi

Description: A homotopy evaluated at its endpoints. (Contributed by Mario Carneiro, 22-Feb-2015)

Step	Hyp	Ref	Expression
1		ishtpy.1	$⊢ φ \to J \in TopOn (X)$
2		ishtpy.3	$⊢ φ \to F \in (J Cn K)$
3		ishtpy.4	$⊢ φ \to G \in (J Cn K)$
4		htpyi.1	$⊢ φ \to H \in (F (J Htpy K) G)$
5	1 2 3	ishtpy	$⊢ φ \to (H \in (F (J Htpy K) G) \leftrightarrow (H \in ((J \times_{t} II) Cn K) \land \forall s \in X (s H 0 = F (s) \land s H 1 = G (s))))$
6	4 5	mpbid	$⊢ φ \to (H \in ((J \times_{t} II) Cn K) \land \forall s \in X (s H 0 = F (s) \land s H 1 = G (s)))$
7	6	simprd	$⊢ φ \to \forall s \in X (s H 0 = F (s) \land s H 1 = G (s))$
8		oveq1	$⊢ s = A \to s H 0 = A H 0$
9		fveq2	$⊢ s = A \to F (s) = F (A)$
10	8 9	eqeq12d	$⊢ s = A \to (s H 0 = F (s) \leftrightarrow A H 0 = F (A))$
11		oveq1	$⊢ s = A \to s H 1 = A H 1$
12		fveq2	$⊢ s = A \to G (s) = G (A)$
13	11 12	eqeq12d	$⊢ s = A \to (s H 1 = G (s) \leftrightarrow A H 1 = G (A))$
14	10 13	anbi12d	$⊢ s = A \to ((s H 0 = F (s) \land s H 1 = G (s)) \leftrightarrow (A H 0 = F (A) \land A H 1 = G (A)))$
15	14	rspccva	$⊢ (\forall s \in X (s H 0 = F (s) \land s H 1 = G (s)) \land A \in X) \to (A H 0 = F (A) \land A H 1 = G (A))$
16	7 15	sylan	$⊢ (φ \land A \in X) \to (A H 0 = F (A) \land A H 1 = G (A))$

Metamath Proof Explorer