Metamath Proof Explorer

Theorem phtpyid

Description: A homotopy from a path to itself. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 23-Feb-2015)

Ref Expression
Hypotheses phtpyid.1 ⊢ G = x ∈ 0 1 , y ∈ 0 1 ⟼ F ⁡ x
phtpyid.3 ⊢ φ → F ∈ II Cn J
Assertion phtpyid ⊢ φ → G ∈ F PHtpy ⁡ J F

Proof

Step Hyp Ref Expression
1 phtpyid.1 ⊢ G = x ∈ 0 1 , y ∈ 0 1 ⟼ F ⁡ x
2 phtpyid.3 ⊢ φ → F ∈ II Cn J
3 iitopon ⊢ II ∈ TopOn ⁡ 0 1
4 3 a1i ⊢ φ → II ∈ TopOn ⁡ 0 1
5 1 4 2 htpyid ⊢ φ → G ∈ F II Htpy J F
6 0elunit ⊢ 0 ∈ 0 1
7 fveq2 ⊢ x = 0 → F ⁡ x = F ⁡ 0
8 eqidd ⊢ y = s → F ⁡ 0 = F ⁡ 0
9 fvex ⊢ F ⁡ 0 ∈ V
10 7 8 1 9 ovmpo ⊢ 0 ∈ 0 1 ∧ s ∈ 0 1 → 0 G s = F ⁡ 0
11 6 10 mpan ⊢ s ∈ 0 1 → 0 G s = F ⁡ 0
12 11 adantl ⊢ φ ∧ s ∈ 0 1 → 0 G s = F ⁡ 0
13 1elunit ⊢ 1 ∈ 0 1
14 fveq2 ⊢ x = 1 → F ⁡ x = F ⁡ 1
15 eqidd ⊢ y = s → F ⁡ 1 = F ⁡ 1
16 fvex ⊢ F ⁡ 1 ∈ V
17 14 15 1 16 ovmpo ⊢ 1 ∈ 0 1 ∧ s ∈ 0 1 → 1 G s = F ⁡ 1
18 13 17 mpan ⊢ s ∈ 0 1 → 1 G s = F ⁡ 1
19 18 adantl ⊢ φ ∧ s ∈ 0 1 → 1 G s = F ⁡ 1
20 2 2 5 12 19 isphtpyd ⊢ φ → G ∈ F PHtpy ⁡ J F