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 22509
Description: Define the class of path homotopies between two paths 𝐹, 𝐺:II⟶𝑋; these are homotopies (in the sense of df-htpy 22508) 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 22506 . 2 class PHtpy
2 vx . . 3 setvar 𝑥
3 ctop 20459 . . 3 class Top
4 vf . . . 4 setvar 𝑓
5 vg . . . 4 setvar 𝑔
6 cii 22417 . . . . 5 class II
72cv 1473 . . . . 5 class 𝑥
8 ccn 20780 . . . . 5 class Cn
96, 7, 8co 6527 . . . 4 class (II Cn 𝑥)
10 cc0 9792 . . . . . . . . 9 class 0
11 vs . . . . . . . . . 10 setvar 𝑠
1211cv 1473 . . . . . . . . 9 class 𝑠
13 vh . . . . . . . . . 10 setvar
1413cv 1473 . . . . . . . . 9 class
1510, 12, 14co 6527 . . . . . . . 8 class (0𝑠)
164cv 1473 . . . . . . . . 9 class 𝑓
1710, 16cfv 5790 . . . . . . . 8 class (𝑓‘0)
1815, 17wceq 1474 . . . . . . 7 wff (0𝑠) = (𝑓‘0)
19 c1 9793 . . . . . . . . 9 class 1
2019, 12, 14co 6527 . . . . . . . 8 class (1𝑠)
2119, 16cfv 5790 . . . . . . . 8 class (𝑓‘1)
2220, 21wceq 1474 . . . . . . 7 wff (1𝑠) = (𝑓‘1)
2318, 22wa 382 . . . . . 6 wff ((0𝑠) = (𝑓‘0) ∧ (1𝑠) = (𝑓‘1))
24 cicc 12005 . . . . . . 7 class [,]
2510, 19, 24co 6527 . . . . . 6 class (0[,]1)
2623, 11, 25wral 2895 . . . . 5 wff 𝑠 ∈ (0[,]1)((0𝑠) = (𝑓‘0) ∧ (1𝑠) = (𝑓‘1))
275cv 1473 . . . . . 6 class 𝑔
28 chtpy 22505 . . . . . . 7 class Htpy
296, 7, 28co 6527 . . . . . 6 class (II Htpy 𝑥)
3016, 27, 29co 6527 . . . . 5 class (𝑓(II Htpy 𝑥)𝑔)
3126, 13, 30crab 2899 . . . 4 class { ∈ (𝑓(II Htpy 𝑥)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0𝑠) = (𝑓‘0) ∧ (1𝑠) = (𝑓‘1))}
324, 5, 9, 9, 31cmpt2 6529 . . 3 class (𝑓 ∈ (II Cn 𝑥), 𝑔 ∈ (II Cn 𝑥) ↦ { ∈ (𝑓(II Htpy 𝑥)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0𝑠) = (𝑓‘0) ∧ (1𝑠) = (𝑓‘1))})
332, 3, 32cmpt 4637 . 2 class (𝑥 ∈ Top ↦ (𝑓 ∈ (II Cn 𝑥), 𝑔 ∈ (II Cn 𝑥) ↦ { ∈ (𝑓(II Htpy 𝑥)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0𝑠) = (𝑓‘0) ∧ (1𝑠) = (𝑓‘1))}))
341, 33wceq 1474 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  22519
  Copyright terms: Public domain W3C validator