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

Definition df-htpy 19026
 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 19023 . 2 Htpy
2 vx . . 3
3 vy . . 3
4 ctop 16989 . . 3
5 vf . . . 4
6 vg . . . 4
72cv 1652 . . . . 5
83cv 1652 . . . . 5
9 ccn 17319 . . . . 5
107, 8, 9co 6110 . . . 4
11 vs . . . . . . . . . 10
1211cv 1652 . . . . . . . . 9
13 cc0 9021 . . . . . . . . 9
14 vh . . . . . . . . . 10
1514cv 1652 . . . . . . . . 9
1612, 13, 15co 6110 . . . . . . . 8
175cv 1652 . . . . . . . . 9
1812, 17cfv 5483 . . . . . . . 8
1916, 18wceq 1653 . . . . . . 7
20 c1 9022 . . . . . . . . 9
2112, 20, 15co 6110 . . . . . . . 8
226cv 1652 . . . . . . . . 9
2312, 22cfv 5483 . . . . . . . 8
2421, 23wceq 1653 . . . . . . 7
2519, 24wa 360 . . . . . 6
267cuni 4039 . . . . . 6
2725, 11, 26wral 2711 . . . . 5
28 cii 18936 . . . . . . 7
29 ctx 17623 . . . . . . 7
307, 28, 29co 6110 . . . . . 6
3130, 8, 9co 6110 . . . . 5
3227, 14, 31crab 2715 . . . 4
335, 6, 10, 10, 32cmpt2 6112 . . 3
342, 3, 4, 4, 33cmpt2 6112 . 2
351, 34wceq 1653 1 Htpy
 Colors of variables: wff set class This definition is referenced by:  ishtpy  19028
 Copyright terms: Public domain W3C validator