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

Definition df-htpy 18484
Description: Define the function which takes topological spaces  X ,  Y and two continuous functions  F ,  G : X
--> Y and returns the class of homotopies from  F to  G. (Contributed by Mario Carneiro, 22-Feb-2015.)
Assertion
Ref Expression
df-htpy  |- Htpy  =  ( x  e.  Top , 
y  e.  Top  |->  ( f  e.  ( x  Cn  y ) ,  g  e.  ( x  Cn  y )  |->  { h  e.  ( ( x  tX  II )  Cn  y )  | 
A. s  e.  U. x ( ( s h 0 )  =  ( f `  s
)  /\  ( s
h 1 )  =  ( g `  s
) ) } ) )
Distinct variable group:    f, g, h, s, x, y

Detailed syntax breakdown of Definition df-htpy
StepHypRef Expression
1 chtpy 18481 . 2  class Htpy
2 vx . . 3  set  x
3 vy . . 3  set  y
4 ctop 16647 . . 3  class  Top
5 vf . . . 4  set  f
6 vg . . . 4  set  g
72cv 1631 . . . . 5  class  x
83cv 1631 . . . . 5  class  y
9 ccn 16970 . . . . 5  class  Cn
107, 8, 9co 5874 . . . 4  class  ( x  Cn  y )
11 vs . . . . . . . . . 10  set  s
1211cv 1631 . . . . . . . . 9  class  s
13 cc0 8753 . . . . . . . . 9  class  0
14 vh . . . . . . . . . 10  set  h
1514cv 1631 . . . . . . . . 9  class  h
1612, 13, 15co 5874 . . . . . . . 8  class  ( s h 0 )
175cv 1631 . . . . . . . . 9  class  f
1812, 17cfv 5271 . . . . . . . 8  class  ( f `
 s )
1916, 18wceq 1632 . . . . . . 7  wff  ( s h 0 )  =  ( f `  s
)
20 c1 8754 . . . . . . . . 9  class  1
2112, 20, 15co 5874 . . . . . . . 8  class  ( s h 1 )
226cv 1631 . . . . . . . . 9  class  g
2312, 22cfv 5271 . . . . . . . 8  class  ( g `
 s )
2421, 23wceq 1632 . . . . . . 7  wff  ( s h 1 )  =  ( g `  s
)
2519, 24wa 358 . . . . . 6  wff  ( ( s h 0 )  =  ( f `  s )  /\  (
s h 1 )  =  ( g `  s ) )
267cuni 3843 . . . . . 6  class  U. x
2725, 11, 26wral 2556 . . . . 5  wff  A. s  e.  U. x ( ( s h 0 )  =  ( f `  s )  /\  (
s h 1 )  =  ( g `  s ) )
28 cii 18395 . . . . . . 7  class  II
29 ctx 17271 . . . . . . 7  class  tX
307, 28, 29co 5874 . . . . . 6  class  ( x 
tX  II )
3130, 8, 9co 5874 . . . . 5  class  ( ( x  tX  II )  Cn  y )
3227, 14, 31crab 2560 . . . 4  class  { h  e.  ( ( x  tX  II )  Cn  y
)  |  A. s  e.  U. x ( ( s h 0 )  =  ( f `  s )  /\  (
s h 1 )  =  ( g `  s ) ) }
335, 6, 10, 10, 32cmpt2 5876 . . 3  class  ( f  e.  ( x  Cn  y ) ,  g  e.  ( x  Cn  y )  |->  { h  e.  ( ( x  tX  II )  Cn  y
)  |  A. s  e.  U. x ( ( s h 0 )  =  ( f `  s )  /\  (
s h 1 )  =  ( g `  s ) ) } )
342, 3, 4, 4, 33cmpt2 5876 . 2  class  ( x  e.  Top ,  y  e.  Top  |->  ( f  e.  ( x  Cn  y ) ,  g  e.  ( x  Cn  y )  |->  { h  e.  ( ( x  tX  II )  Cn  y
)  |  A. s  e.  U. x ( ( s h 0 )  =  ( f `  s )  /\  (
s h 1 )  =  ( g `  s ) ) } ) )
351, 34wceq 1632 1  wff Htpy  =  ( x  e.  Top , 
y  e.  Top  |->  ( f  e.  ( x  Cn  y ) ,  g  e.  ( x  Cn  y )  |->  { h  e.  ( ( x  tX  II )  Cn  y )  | 
A. s  e.  U. x ( ( s h 0 )  =  ( f `  s
)  /\  ( s
h 1 )  =  ( g `  s
) ) } ) )
Colors of variables: wff set class
This definition is referenced by:  ishtpy  18486
  Copyright terms: Public domain W3C validator