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 24718
Description: Define the class of path homotopies between two paths 𝐹, 𝐺:II⟶𝑋; these are homotopies (in the sense of df-htpy 24717) 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 24715 . 2 class PHtpy
2 vx . . 3 setvar 𝑥
3 ctop 22616 . . 3 class Top
4 vf . . . 4 setvar 𝑓
5 vg . . . 4 setvar 𝑔
6 cii 24616 . . . . 5 class II
72cv 1539 . . . . 5 class 𝑥
8 ccn 22949 . . . . 5 class Cn
96, 7, 8co 7412 . . . 4 class (II Cn 𝑥)
10 cc0 11113 . . . . . . . . 9 class 0
11 vs . . . . . . . . . 10 setvar 𝑠
1211cv 1539 . . . . . . . . 9 class 𝑠
13 vh . . . . . . . . . 10 setvar
1413cv 1539 . . . . . . . . 9 class
1510, 12, 14co 7412 . . . . . . . 8 class (0𝑠)
164cv 1539 . . . . . . . . 9 class 𝑓
1710, 16cfv 6544 . . . . . . . 8 class (𝑓‘0)
1815, 17wceq 1540 . . . . . . 7 wff (0𝑠) = (𝑓‘0)
19 c1 11114 . . . . . . . . 9 class 1
2019, 12, 14co 7412 . . . . . . . 8 class (1𝑠)
2119, 16cfv 6544 . . . . . . . 8 class (𝑓‘1)
2220, 21wceq 1540 . . . . . . 7 wff (1𝑠) = (𝑓‘1)
2318, 22wa 395 . . . . . 6 wff ((0𝑠) = (𝑓‘0) ∧ (1𝑠) = (𝑓‘1))
24 cicc 13332 . . . . . . 7 class [,]
2510, 19, 24co 7412 . . . . . 6 class (0[,]1)
2623, 11, 25wral 3060 . . . . 5 wff 𝑠 ∈ (0[,]1)((0𝑠) = (𝑓‘0) ∧ (1𝑠) = (𝑓‘1))
275cv 1539 . . . . . 6 class 𝑔
28 chtpy 24714 . . . . . . 7 class Htpy
296, 7, 28co 7412 . . . . . 6 class (II Htpy 𝑥)
3016, 27, 29co 7412 . . . . 5 class (𝑓(II Htpy 𝑥)𝑔)
3126, 13, 30crab 3431 . . . 4 class { ∈ (𝑓(II Htpy 𝑥)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0𝑠) = (𝑓‘0) ∧ (1𝑠) = (𝑓‘1))}
324, 5, 9, 9, 31cmpo 7414 . . 3 class (𝑓 ∈ (II Cn 𝑥), 𝑔 ∈ (II Cn 𝑥) ↦ { ∈ (𝑓(II Htpy 𝑥)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0𝑠) = (𝑓‘0) ∧ (1𝑠) = (𝑓‘1))})
332, 3, 32cmpt 5232 . 2 class (𝑥 ∈ Top ↦ (𝑓 ∈ (II Cn 𝑥), 𝑔 ∈ (II Cn 𝑥) ↦ { ∈ (𝑓(II Htpy 𝑥)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0𝑠) = (𝑓‘0) ∧ (1𝑠) = (𝑓‘1))}))
341, 33wceq 1540 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  24728
  Copyright terms: Public domain W3C validator