Metamath Proof Explorer

Definition df-htpy

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)

Ref Expression
Assertion 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 ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 chtpy 
 |-  Htpy
1 vx 
 |-  x
2 ctop 
 |-  Top
3 vy 
 |-  y
4 vf 
 |-  f
5 1 cv 
 |-  x
6 ccn 
 |-  Cn
7 3 cv 
 |-  y
8 5 7 6 co 
 |-  ( x Cn y )
9 vg 
 |-  g
10 vh 
 |-  h
11 ctx 
 |-  tX
12 cii 
 |-  II
13 5 12 11 co 
 |-  ( x tX II )
14 13 7 6 co 
 |-  ( ( x tX II ) Cn y )
15 vs 
 |-  s
16 5 cuni 
 |-  U. x
17 15 cv 
 |-  s
18 10 cv 
 |-  h
19 cc0 
 |-  0
20 17 19 18 co 
 |-  ( s h 0 )
21 4 cv 
 |-  f
22 17 21 cfv 
 |-  ( f ` s )
23 20 22 wceq 
 |-  ( s h 0 ) = ( f ` s )
24 c1 
 |-  1
25 17 24 18 co 
 |-  ( s h 1 )
26 9 cv 
 |-  g
27 17 26 cfv 
 |-  ( g ` s )
28 25 27 wceq 
 |-  ( s h 1 ) = ( g ` s )
29 23 28 wa 
 |-  ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) )
30 29 15 16 wral 
 |-  A. s e. U. x ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) )
31 30 10 14 crab 
 |-  { h e. ( ( x tX II ) Cn y ) | A. s e. U. x ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) ) }
32 4 9 8 8 31 cmpo 
 |-  ( 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 ) ) } )
33 1 3 2 2 32 cmpo 
 |-  ( 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 ) ) } ) )
34 0 33 wceq 
 |-  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 ) ) } ) )