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

Definition df-phtpy 22817
 Description: Define the class of path homotopies between two paths 𝐹, 𝐺:II⟶𝑋; these are homotopies (in the sense of df-htpy 22816) 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 22814 . 2 class PHtpy
2 vx . . 3 setvar 𝑥
3 ctop 20746 . . 3 class Top
4 vf . . . 4 setvar 𝑓
5 vg . . . 4 setvar 𝑔
6 cii 22725 . . . . 5 class II
72cv 1522 . . . . 5 class 𝑥
8 ccn 21076 . . . . 5 class Cn
96, 7, 8co 6690 . . . 4 class (II Cn 𝑥)
10 cc0 9974 . . . . . . . . 9 class 0
11 vs . . . . . . . . . 10 setvar 𝑠
1211cv 1522 . . . . . . . . 9 class 𝑠
13 vh . . . . . . . . . 10 setvar
1413cv 1522 . . . . . . . . 9 class
1510, 12, 14co 6690 . . . . . . . 8 class (0𝑠)
164cv 1522 . . . . . . . . 9 class 𝑓
1710, 16cfv 5926 . . . . . . . 8 class (𝑓‘0)
1815, 17wceq 1523 . . . . . . 7 wff (0𝑠) = (𝑓‘0)
19 c1 9975 . . . . . . . . 9 class 1
2019, 12, 14co 6690 . . . . . . . 8 class (1𝑠)
2119, 16cfv 5926 . . . . . . . 8 class (𝑓‘1)
2220, 21wceq 1523 . . . . . . 7 wff (1𝑠) = (𝑓‘1)
2318, 22wa 383 . . . . . 6 wff ((0𝑠) = (𝑓‘0) ∧ (1𝑠) = (𝑓‘1))
24 cicc 12216 . . . . . . 7 class [,]
2510, 19, 24co 6690 . . . . . 6 class (0[,]1)
2623, 11, 25wral 2941 . . . . 5 wff 𝑠 ∈ (0[,]1)((0𝑠) = (𝑓‘0) ∧ (1𝑠) = (𝑓‘1))
275cv 1522 . . . . . 6 class 𝑔
28 chtpy 22813 . . . . . . 7 class Htpy
296, 7, 28co 6690 . . . . . 6 class (II Htpy 𝑥)
3016, 27, 29co 6690 . . . . 5 class (𝑓(II Htpy 𝑥)𝑔)
3126, 13, 30crab 2945 . . . 4 class { ∈ (𝑓(II Htpy 𝑥)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0𝑠) = (𝑓‘0) ∧ (1𝑠) = (𝑓‘1))}
324, 5, 9, 9, 31cmpt2 6692 . . 3 class (𝑓 ∈ (II Cn 𝑥), 𝑔 ∈ (II Cn 𝑥) ↦ { ∈ (𝑓(II Htpy 𝑥)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0𝑠) = (𝑓‘0) ∧ (1𝑠) = (𝑓‘1))})
332, 3, 32cmpt 4762 . 2 class (𝑥 ∈ Top ↦ (𝑓 ∈ (II Cn 𝑥), 𝑔 ∈ (II Cn 𝑥) ↦ { ∈ (𝑓(II Htpy 𝑥)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0𝑠) = (𝑓‘0) ∧ (1𝑠) = (𝑓‘1))}))
341, 33wceq 1523 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  22827
 Copyright terms: Public domain W3C validator