Metamath Proof Explorer

Theorem htpyid

Description: A homotopy from a function to itself. (Contributed by Mario Carneiro, 23-Feb-2015)

Ref Expression
Hypotheses htpyid.1 
|- G = ( x e. X , y e. ( 0 [,] 1 ) |-> ( F ` x ) )
htpyid.2 
|- ( ph -> J e. ( TopOn ` X ) )
htpyid.4 
|- ( ph -> F e. ( J Cn K ) )
Assertion htpyid 
|- ( ph -> G e. ( F ( J Htpy K ) F ) )

Proof

Step Hyp Ref Expression
1 htpyid.1 
 |-  G = ( x e. X , y e. ( 0 [,] 1 ) |-> ( F ` x ) )
2 htpyid.2 
 |-  ( ph -> J e. ( TopOn ` X ) )
3 htpyid.4 
 |-  ( ph -> F e. ( J Cn K ) )
4 iitopon 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )
5 4 a1i 
 |-  ( ph -> II e. ( TopOn ` ( 0 [,] 1 ) ) )
6 2 5 cnmpt1st 
 |-  ( ph -> ( x e. X , y e. ( 0 [,] 1 ) |-> x ) e. ( ( J tX II ) Cn J ) )
7 2 5 6 3 cnmpt21f 
 |-  ( ph -> ( x e. X , y e. ( 0 [,] 1 ) |-> ( F ` x ) ) e. ( ( J tX II ) Cn K ) )
8 1 7 eqeltrid 
 |-  ( ph -> G e. ( ( J tX II ) Cn K ) )
9 simpr 
 |-  ( ( ph /\ s e. X ) -> s e. X )
10 0elunit 
 |-  0 e. ( 0 [,] 1 )
11 fveq2 
 |-  ( x = s -> ( F ` x ) = ( F ` s ) )
12 eqidd 
 |-  ( y = 0 -> ( F ` s ) = ( F ` s ) )
13 fvex 
 |-  ( F ` s ) e. _V
14 11 12 1 13 ovmpo 
 |-  ( ( s e. X /\ 0 e. ( 0 [,] 1 ) ) -> ( s G 0 ) = ( F ` s ) )
15 9 10 14 sylancl 
 |-  ( ( ph /\ s e. X ) -> ( s G 0 ) = ( F ` s ) )
16 1elunit 
 |-  1 e. ( 0 [,] 1 )
17 eqidd 
 |-  ( y = 1 -> ( F ` s ) = ( F ` s ) )
18 11 17 1 13 ovmpo 
 |-  ( ( s e. X /\ 1 e. ( 0 [,] 1 ) ) -> ( s G 1 ) = ( F ` s ) )
19 9 16 18 sylancl 
 |-  ( ( ph /\ s e. X ) -> ( s G 1 ) = ( F ` s ) )
20 2 3 3 8 15 19 ishtpyd 
 |-  ( ph -> G e. ( F ( J Htpy K ) F ) )