MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-phtpy Structured version   Visualization version   GIF version

Definition df-phtpy 23502
Description: Define the class of path homotopies between two paths 𝐹, 𝐺:II⟶𝑋; these are homotopies (in the sense of df-htpy 23501) which also preserve both endpoints of the paths throughout the homotopy. Definition of [Hatcher] p. 25. (Contributed by Jeff Madsen, 2-Sep-2009.)
Assertion
Ref Expression
df-phtpy PHtpy = (𝑥 ∈ Top ↦ (𝑓 ∈ (II Cn 𝑥), 𝑔 ∈ (II Cn 𝑥) ↦ { ∈ (𝑓(II Htpy 𝑥)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0𝑠) = (𝑓‘0) ∧ (1𝑠) = (𝑓‘1))}))
Distinct variable group:   𝑓,𝑔,,𝑠,𝑥

Detailed syntax breakdown of Definition df-phtpy
StepHypRef Expression
1 cphtpy 23499 . 2 class PHtpy
2 vx . . 3 setvar 𝑥
3 ctop 21429 . . 3 class Top
4 vf . . . 4 setvar 𝑓
5 vg . . . 4 setvar 𝑔
6 cii 23410 . . . . 5 class II
72cv 1527 . . . . 5 class 𝑥
8 ccn 21760 . . . . 5 class Cn
96, 7, 8co 7145 . . . 4 class (II Cn 𝑥)
10 cc0 10525 . . . . . . . . 9 class 0
11 vs . . . . . . . . . 10 setvar 𝑠
1211cv 1527 . . . . . . . . 9 class 𝑠
13 vh . . . . . . . . . 10 setvar
1413cv 1527 . . . . . . . . 9 class
1510, 12, 14co 7145 . . . . . . . 8 class (0𝑠)
164cv 1527 . . . . . . . . 9 class 𝑓
1710, 16cfv 6348 . . . . . . . 8 class (𝑓‘0)
1815, 17wceq 1528 . . . . . . 7 wff (0𝑠) = (𝑓‘0)
19 c1 10526 . . . . . . . . 9 class 1
2019, 12, 14co 7145 . . . . . . . 8 class (1𝑠)
2119, 16cfv 6348 . . . . . . . 8 class (𝑓‘1)
2220, 21wceq 1528 . . . . . . 7 wff (1𝑠) = (𝑓‘1)
2318, 22wa 396 . . . . . 6 wff ((0𝑠) = (𝑓‘0) ∧ (1𝑠) = (𝑓‘1))
24 cicc 12729 . . . . . . 7 class [,]
2510, 19, 24co 7145 . . . . . 6 class (0[,]1)
2623, 11, 25wral 3135 . . . . 5 wff 𝑠 ∈ (0[,]1)((0𝑠) = (𝑓‘0) ∧ (1𝑠) = (𝑓‘1))
275cv 1527 . . . . . 6 class 𝑔
28 chtpy 23498 . . . . . . 7 class Htpy
296, 7, 28co 7145 . . . . . 6 class (II Htpy 𝑥)
3016, 27, 29co 7145 . . . . 5 class (𝑓(II Htpy 𝑥)𝑔)
3126, 13, 30crab 3139 . . . 4 class { ∈ (𝑓(II Htpy 𝑥)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0𝑠) = (𝑓‘0) ∧ (1𝑠) = (𝑓‘1))}
324, 5, 9, 9, 31cmpo 7147 . . 3 class (𝑓 ∈ (II Cn 𝑥), 𝑔 ∈ (II Cn 𝑥) ↦ { ∈ (𝑓(II Htpy 𝑥)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0𝑠) = (𝑓‘0) ∧ (1𝑠) = (𝑓‘1))})
332, 3, 32cmpt 5137 . 2 class (𝑥 ∈ Top ↦ (𝑓 ∈ (II Cn 𝑥), 𝑔 ∈ (II Cn 𝑥) ↦ { ∈ (𝑓(II Htpy 𝑥)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0𝑠) = (𝑓‘0) ∧ (1𝑠) = (𝑓‘1))}))
341, 33wceq 1528 1 wff PHtpy = (𝑥 ∈ Top ↦ (𝑓 ∈ (II Cn 𝑥), 𝑔 ∈ (II Cn 𝑥) ↦ { ∈ (𝑓(II Htpy 𝑥)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0𝑠) = (𝑓‘0) ∧ (1𝑠) = (𝑓‘1))}))
Colors of variables: wff setvar class
This definition is referenced by:  isphtpy  23512
  Copyright terms: Public domain W3C validator