htpyid

Description: A homotopy from a function to itself. (Contributed by Mario Carneiro, 23-Feb-2015)

Step	Hyp	Ref	Expression
1		htpyid.1	$⊢ G = (x \in X, y \in [0, 1] ⟼ F (x))$
2		htpyid.2	$⊢ φ \to J \in TopOn (X)$
3		htpyid.4	$⊢ φ \to F \in (J Cn K)$
4		iitopon	$⊢ II \in TopOn ([0, 1])$
5	4	a1i	$⊢ φ \to II \in TopOn ([0, 1])$
6	2 5	cnmpt1st	$⊢ φ \to (x \in X, y \in [0, 1] ⟼ x) \in ((J \times_{t} II) Cn J)$
7	2 5 6 3	cnmpt21f	$⊢ φ \to (x \in X, y \in [0, 1] ⟼ F (x)) \in ((J \times_{t} II) Cn K)$
8	1 7	eqeltrid	$⊢ φ \to G \in ((J \times_{t} II) Cn K)$
9		simpr	$⊢ (φ \land s \in X) \to s \in X$
10		0elunit	$⊢ 0 \in [0, 1]$
11		fveq2	$⊢ x = s \to F (x) = F (s)$
12		eqidd	$⊢ y = 0 \to F (s) = F (s)$
13		fvex	$⊢ F (s) \in V$
14	11 12 1 13	ovmpo	$⊢ (s \in X \land 0 \in [0, 1]) \to s G 0 = F (s)$
15	9 10 14	sylancl	$⊢ (φ \land s \in X) \to s G 0 = F (s)$
16		1elunit	$⊢ 1 \in [0, 1]$
17		eqidd	$⊢ y = 1 \to F (s) = F (s)$
18	11 17 1 13	ovmpo	$⊢ (s \in X \land 1 \in [0, 1]) \to s G 1 = F (s)$
19	9 16 18	sylancl	$⊢ (φ \land s \in X) \to s G 1 = F (s)$
20	2 3 3 8 15 19	ishtpyd	$⊢ φ \to G \in (F (J Htpy K) F)$

Metamath Proof Explorer