# 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 ) )`
` |-  ( ( 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 ) )`
` |-  ( ( ph /\ s e. ( 0 [,] 1 ) ) -> ( 1 G s ) = ( F ` 1 ) )`
` |-  ( ph -> G e. ( F ( PHtpy ` J ) F ) )`