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

Definition df-phtpy 18431
Description: Define the class of path homotopies between two paths  F ,  G : II --> X; these are homotopies (in the sense of df-htpy 18430) 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  =  ( x  e.  Top  |->  ( f  e.  ( II 
Cn  x ) ,  g  e.  ( II 
Cn  x )  |->  { h  e.  ( f ( II Htpy  x ) g )  |  A. s  e.  ( 0 [,] 1 ) ( ( 0 h s )  =  ( f `
 0 )  /\  ( 1 h s )  =  ( f `
 1 ) ) } ) )
Distinct variable group:    f, g, h, s, x

Detailed syntax breakdown of Definition df-phtpy
StepHypRef Expression
1 cphtpy 18428 . 2  class  PHtpy
2 vx . . 3  set  x
3 ctop 16593 . . 3  class  Top
4 vf . . . 4  set  f
5 vg . . . 4  set  g
6 cii 18341 . . . . 5  class  II
72cv 1618 . . . . 5  class  x
8 ccn 16916 . . . . 5  class  Cn
96, 7, 8co 5792 . . . 4  class  ( II 
Cn  x )
10 cc0 8705 . . . . . . . . 9  class  0
11 vs . . . . . . . . . 10  set  s
1211cv 1618 . . . . . . . . 9  class  s
13 vh . . . . . . . . . 10  set  h
1413cv 1618 . . . . . . . . 9  class  h
1510, 12, 14co 5792 . . . . . . . 8  class  ( 0 h s )
164cv 1618 . . . . . . . . 9  class  f
1710, 16cfv 4673 . . . . . . . 8  class  ( f `
 0 )
1815, 17wceq 1619 . . . . . . 7  wff  ( 0 h s )  =  ( f `  0
)
19 c1 8706 . . . . . . . . 9  class  1
2019, 12, 14co 5792 . . . . . . . 8  class  ( 1 h s )
2119, 16cfv 4673 . . . . . . . 8  class  ( f `
 1 )
2220, 21wceq 1619 . . . . . . 7  wff  ( 1 h s )  =  ( f `  1
)
2318, 22wa 360 . . . . . 6  wff  ( ( 0 h s )  =  ( f ` 
0 )  /\  (
1 h s )  =  ( f ` 
1 ) )
24 cicc 10625 . . . . . . 7  class  [,]
2510, 19, 24co 5792 . . . . . 6  class  ( 0 [,] 1 )
2623, 11, 25wral 2518 . . . . 5  wff  A. s  e.  ( 0 [,] 1
) ( ( 0 h s )  =  ( f `  0
)  /\  ( 1 h s )  =  ( f `  1
) )
275cv 1618 . . . . . 6  class  g
28 chtpy 18427 . . . . . . 7  class Htpy
296, 7, 28co 5792 . . . . . 6  class  ( II Htpy 
x )
3016, 27, 29co 5792 . . . . 5  class  ( f ( II Htpy  x ) g )
3126, 13, 30crab 2522 . . . 4  class  { h  e.  ( f ( II Htpy 
x ) g )  |  A. s  e.  ( 0 [,] 1
) ( ( 0 h s )  =  ( f `  0
)  /\  ( 1 h s )  =  ( f `  1
) ) }
324, 5, 9, 9, 31cmpt2 5794 . . 3  class  ( f  e.  ( II  Cn  x ) ,  g  e.  ( II  Cn  x )  |->  { h  e.  ( f ( II Htpy 
x ) g )  |  A. s  e.  ( 0 [,] 1
) ( ( 0 h s )  =  ( f `  0
)  /\  ( 1 h s )  =  ( f `  1
) ) } )
332, 3, 32cmpt 4051 . 2  class  ( x  e.  Top  |->  ( f  e.  ( II  Cn  x ) ,  g  e.  ( II  Cn  x )  |->  { h  e.  ( f ( II Htpy 
x ) g )  |  A. s  e.  ( 0 [,] 1
) ( ( 0 h s )  =  ( f `  0
)  /\  ( 1 h s )  =  ( f `  1
) ) } ) )
341, 33wceq 1619 1  wff  PHtpy  =  ( x  e.  Top  |->  ( f  e.  ( II 
Cn  x ) ,  g  e.  ( II 
Cn  x )  |->  { h  e.  ( f ( II Htpy  x ) g )  |  A. s  e.  ( 0 [,] 1 ) ( ( 0 h s )  =  ( f `
 0 )  /\  ( 1 h s )  =  ( f `
 1 ) ) } ) )
Colors of variables: wff set class
This definition is referenced by:  isphtpy  18441
  Copyright terms: Public domain W3C validator