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

Definition df-htpy 21985
 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
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-htpy
StepHypRef Expression
1 chtpy 21982 . 2 Htpy
2 vx . . 3
3 vy . . 3
4 ctop 19901 . . 3
5 vf . . . 4
6 vg . . . 4
72cv 1436 . . . . 5
83cv 1436 . . . . 5
9 ccn 20224 . . . . 5
107, 8, 9co 6301 . . . 4
11 vs . . . . . . . . . 10
1211cv 1436 . . . . . . . . 9
13 cc0 9539 . . . . . . . . 9
14 vh . . . . . . . . . 10
1514cv 1436 . . . . . . . . 9
1612, 13, 15co 6301 . . . . . . . 8
175cv 1436 . . . . . . . . 9
1812, 17cfv 5597 . . . . . . . 8
1916, 18wceq 1437 . . . . . . 7
20 c1 9540 . . . . . . . . 9
2112, 20, 15co 6301 . . . . . . . 8
226cv 1436 . . . . . . . . 9
2312, 22cfv 5597 . . . . . . . 8
2421, 23wceq 1437 . . . . . . 7
2519, 24wa 370 . . . . . 6
267cuni 4216 . . . . . 6
2725, 11, 26wral 2775 . . . . 5
28 cii 21891 . . . . . . 7
29 ctx 20559 . . . . . . 7
307, 28, 29co 6301 . . . . . 6
3130, 8, 9co 6301 . . . . 5
3227, 14, 31crab 2779 . . . 4
335, 6, 10, 10, 32cmpt2 6303 . . 3
342, 3, 4, 4, 33cmpt2 6303 . 2
351, 34wceq 1437 1 Htpy
 Colors of variables: wff setvar class This definition is referenced by:  ishtpy  21987
 Copyright terms: Public domain W3C validator