Metamath Proof Explorer

Theorem htpyid

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

Ref Expression
Hypotheses htpyid.1 ⊢ G = x ∈ X , y ∈ 0 1 ⟼ F ⁡ x
htpyid.2 ⊢ φ → J ∈ TopOn ⁡ X
htpyid.4 ⊢ φ → F ∈ J Cn K
Assertion htpyid ⊢ φ → G ∈ F J Htpy K F

Proof

Step Hyp Ref Expression
1 htpyid.1 ⊢ G = x ∈ X , y ∈ 0 1 ⟼ F ⁡ x
2 htpyid.2 ⊢ φ → J ∈ TopOn ⁡ X
3 htpyid.4 ⊢ φ → F ∈ J Cn K
4 iitopon ⊢ II ∈ TopOn ⁡ 0 1
5 4 a1i ⊢ φ → II ∈ TopOn ⁡ 0 1
6 2 5 cnmpt1st ⊢ φ → x ∈ X , y ∈ 0 1 ⟼ x ∈ J × t II Cn J
7 2 5 6 3 cnmpt21f ⊢ φ → x ∈ X , y ∈ 0 1 ⟼ F ⁡ x ∈ J × t II Cn K
8 1 7 eqeltrid ⊢ φ → G ∈ J × t II Cn K
9 simpr ⊢ φ ∧ s ∈ X → s ∈ X
10 0elunit ⊢ 0 ∈ 0 1
11 fveq2 ⊢ x = s → F ⁡ x = F ⁡ s
12 eqidd ⊢ y = 0 → F ⁡ s = F ⁡ s
13 fvex ⊢ F ⁡ s ∈ V
14 11 12 1 13 ovmpo ⊢ s ∈ X ∧ 0 ∈ 0 1 → s G 0 = F ⁡ s
15 9 10 14 sylancl ⊢ φ ∧ s ∈ X → s G 0 = F ⁡ s
16 1elunit ⊢ 1 ∈ 0 1
17 eqidd ⊢ y = 1 → F ⁡ s = F ⁡ s
18 11 17 1 13 ovmpo ⊢ s ∈ X ∧ 1 ∈ 0 1 → s G 1 = F ⁡ s
19 9 16 18 sylancl ⊢ φ ∧ s ∈ X → s G 1 = F ⁡ s
20 2 3 3 8 15 19 ishtpyd ⊢ φ → G ∈ F J Htpy K F