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

Definition df-htpy 22989
Description: Define the function which takes topological spaces 𝑋, 𝑌 and two continuous functions 𝐹, 𝐺:𝑋𝑌 and returns the class of homotopies from 𝐹 to 𝐺. (Contributed by Mario Carneiro, 22-Feb-2015.)
Assertion
Ref Expression
df-htpy Htpy = (𝑥 ∈ Top, 𝑦 ∈ Top ↦ (𝑓 ∈ (𝑥 Cn 𝑦), 𝑔 ∈ (𝑥 Cn 𝑦) ↦ { ∈ ((𝑥 ×t II) Cn 𝑦) ∣ ∀𝑠 𝑥((𝑠0) = (𝑓𝑠) ∧ (𝑠1) = (𝑔𝑠))}))
Distinct variable group:   𝑓,𝑔,,𝑠,𝑥,𝑦

Detailed syntax breakdown of Definition df-htpy
StepHypRef Expression
1 chtpy 22986 . 2 class Htpy
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 ctop 20918 . . 3 class Top
5 vf . . . 4 setvar 𝑓
6 vg . . . 4 setvar 𝑔
72cv 1630 . . . . 5 class 𝑥
83cv 1630 . . . . 5 class 𝑦
9 ccn 21249 . . . . 5 class Cn
107, 8, 9co 6793 . . . 4 class (𝑥 Cn 𝑦)
11 vs . . . . . . . . . 10 setvar 𝑠
1211cv 1630 . . . . . . . . 9 class 𝑠
13 cc0 10138 . . . . . . . . 9 class 0
14 vh . . . . . . . . . 10 setvar
1514cv 1630 . . . . . . . . 9 class
1612, 13, 15co 6793 . . . . . . . 8 class (𝑠0)
175cv 1630 . . . . . . . . 9 class 𝑓
1812, 17cfv 6031 . . . . . . . 8 class (𝑓𝑠)
1916, 18wceq 1631 . . . . . . 7 wff (𝑠0) = (𝑓𝑠)
20 c1 10139 . . . . . . . . 9 class 1
2112, 20, 15co 6793 . . . . . . . 8 class (𝑠1)
226cv 1630 . . . . . . . . 9 class 𝑔
2312, 22cfv 6031 . . . . . . . 8 class (𝑔𝑠)
2421, 23wceq 1631 . . . . . . 7 wff (𝑠1) = (𝑔𝑠)
2519, 24wa 382 . . . . . 6 wff ((𝑠0) = (𝑓𝑠) ∧ (𝑠1) = (𝑔𝑠))
267cuni 4574 . . . . . 6 class 𝑥
2725, 11, 26wral 3061 . . . . 5 wff 𝑠 𝑥((𝑠0) = (𝑓𝑠) ∧ (𝑠1) = (𝑔𝑠))
28 cii 22898 . . . . . . 7 class II
29 ctx 21584 . . . . . . 7 class ×t
307, 28, 29co 6793 . . . . . 6 class (𝑥 ×t II)
3130, 8, 9co 6793 . . . . 5 class ((𝑥 ×t II) Cn 𝑦)
3227, 14, 31crab 3065 . . . 4 class { ∈ ((𝑥 ×t II) Cn 𝑦) ∣ ∀𝑠 𝑥((𝑠0) = (𝑓𝑠) ∧ (𝑠1) = (𝑔𝑠))}
335, 6, 10, 10, 32cmpt2 6795 . . 3 class (𝑓 ∈ (𝑥 Cn 𝑦), 𝑔 ∈ (𝑥 Cn 𝑦) ↦ { ∈ ((𝑥 ×t II) Cn 𝑦) ∣ ∀𝑠 𝑥((𝑠0) = (𝑓𝑠) ∧ (𝑠1) = (𝑔𝑠))})
342, 3, 4, 4, 33cmpt2 6795 . 2 class (𝑥 ∈ Top, 𝑦 ∈ Top ↦ (𝑓 ∈ (𝑥 Cn 𝑦), 𝑔 ∈ (𝑥 Cn 𝑦) ↦ { ∈ ((𝑥 ×t II) Cn 𝑦) ∣ ∀𝑠 𝑥((𝑠0) = (𝑓𝑠) ∧ (𝑠1) = (𝑔𝑠))}))
351, 34wceq 1631 1 wff Htpy = (𝑥 ∈ Top, 𝑦 ∈ Top ↦ (𝑓 ∈ (𝑥 Cn 𝑦), 𝑔 ∈ (𝑥 Cn 𝑦) ↦ { ∈ ((𝑥 ×t II) Cn 𝑦) ∣ ∀𝑠 𝑥((𝑠0) = (𝑓𝑠) ∧ (𝑠1) = (𝑔𝑠))}))
Colors of variables: wff setvar class
This definition is referenced by:  ishtpy  22991
  Copyright terms: Public domain W3C validator