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

Definition df-phtpy 18469
 Description: Define the class of path homotopies between two paths ; these are homotopies (in the sense of df-htpy 18468) 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 Htpy
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-phtpy
StepHypRef Expression
1 cphtpy 18466 . 2
2 vx . . 3
3 ctop 16631 . . 3
4 vf . . . 4
5 vg . . . 4
6 cii 18379 . . . . 5
72cv 1622 . . . . 5
8 ccn 16954 . . . . 5
96, 7, 8co 5858 . . . 4
10 cc0 8737 . . . . . . . . 9
11 vs . . . . . . . . . 10
1211cv 1622 . . . . . . . . 9
13 vh . . . . . . . . . 10
1413cv 1622 . . . . . . . . 9
1510, 12, 14co 5858 . . . . . . . 8
164cv 1622 . . . . . . . . 9
1710, 16cfv 5255 . . . . . . . 8
1815, 17wceq 1623 . . . . . . 7
19 c1 8738 . . . . . . . . 9
2019, 12, 14co 5858 . . . . . . . 8
2119, 16cfv 5255 . . . . . . . 8
2220, 21wceq 1623 . . . . . . 7
2318, 22wa 358 . . . . . 6
24 cicc 10659 . . . . . . 7
2510, 19, 24co 5858 . . . . . 6
2623, 11, 25wral 2543 . . . . 5
275cv 1622 . . . . . 6
28 chtpy 18465 . . . . . . 7 Htpy
296, 7, 28co 5858 . . . . . 6 Htpy
3016, 27, 29co 5858 . . . . 5 Htpy
3126, 13, 30crab 2547 . . . 4 Htpy
324, 5, 9, 9, 31cmpt2 5860 . . 3 Htpy
332, 3, 32cmpt 4077 . 2 Htpy
341, 33wceq 1623 1 Htpy
 Colors of variables: wff set class This definition is referenced by:  isphtpy  18479
 Copyright terms: Public domain W3C validator