Metamath Proof Explorer

Theorem phtpyid

Description: A homotopy from a path to itself. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 23-Feb-2015)

Ref Expression
Hypotheses phtpyid.1 
|- G = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( F ` x ) )
phtpyid.3 
|- ( ph -> F e. ( II Cn J ) )
Assertion phtpyid 
|- ( ph -> G e. ( F ( PHtpy ` J ) F ) )

Proof

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