Metamath Proof Explorer

Theorem pcorevcl

Description: Closure for a reversed path. (Contributed by Mario Carneiro, 12-Feb-2015)

Ref Expression
Hypothesis pcorev.1 
|- G = ( x e. ( 0 [,] 1 ) |-> ( F ` ( 1 - x ) ) )
Assertion pcorevcl 
|- ( F e. ( II Cn J ) -> ( G e. ( II Cn J ) /\ ( G ` 0 ) = ( F ` 1 ) /\ ( G ` 1 ) = ( F ` 0 ) ) )

Proof

Step Hyp Ref Expression
1 pcorev.1 
 |-  G = ( x e. ( 0 [,] 1 ) |-> ( F ` ( 1 - x ) ) )
2 iitopon 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )
3 2 a1i 
 |-  ( F e. ( II Cn J ) -> II e. ( TopOn ` ( 0 [,] 1 ) ) )
4 iirevcn 
 |-  ( x e. ( 0 [,] 1 ) |-> ( 1 - x ) ) e. ( II Cn II )
5 4 a1i 
 |-  ( F e. ( II Cn J ) -> ( x e. ( 0 [,] 1 ) |-> ( 1 - x ) ) e. ( II Cn II ) )
6 id 
 |-  ( F e. ( II Cn J ) -> F e. ( II Cn J ) )
7 3 5 6 cnmpt11f 
 |-  ( F e. ( II Cn J ) -> ( x e. ( 0 [,] 1 ) |-> ( F ` ( 1 - x ) ) ) e. ( II Cn J ) )
8 1 7 eqeltrid 
 |-  ( F e. ( II Cn J ) -> G e. ( II Cn J ) )
9 0elunit 
 |-  0 e. ( 0 [,] 1 )
10 oveq2 
 |-  ( x = 0 -> ( 1 - x ) = ( 1 - 0 ) )
11 1m0e1 
 |-  ( 1 - 0 ) = 1
12 10 11 eqtrdi 
 |-  ( x = 0 -> ( 1 - x ) = 1 )
13 12 fveq2d 
 |-  ( x = 0 -> ( F ` ( 1 - x ) ) = ( F ` 1 ) )
14 fvex 
 |-  ( F ` 1 ) e. _V
15 13 1 14 fvmpt 
 |-  ( 0 e. ( 0 [,] 1 ) -> ( G ` 0 ) = ( F ` 1 ) )
16 9 15 mp1i 
 |-  ( F e. ( II Cn J ) -> ( G ` 0 ) = ( F ` 1 ) )
17 1elunit 
 |-  1 e. ( 0 [,] 1 )
18 oveq2 
 |-  ( x = 1 -> ( 1 - x ) = ( 1 - 1 ) )
19 1m1e0 
 |-  ( 1 - 1 ) = 0
20 18 19 eqtrdi 
 |-  ( x = 1 -> ( 1 - x ) = 0 )
21 20 fveq2d 
 |-  ( x = 1 -> ( F ` ( 1 - x ) ) = ( F ` 0 ) )
22 fvex 
 |-  ( F ` 0 ) e. _V
23 21 1 22 fvmpt 
 |-  ( 1 e. ( 0 [,] 1 ) -> ( G ` 1 ) = ( F ` 0 ) )
24 17 23 mp1i 
 |-  ( F e. ( II Cn J ) -> ( G ` 1 ) = ( F ` 0 ) )
25 8 16 24 3jca 
 |-  ( F e. ( II Cn J ) -> ( G e. ( II Cn J ) /\ ( G ` 0 ) = ( F ` 1 ) /\ ( G ` 1 ) = ( F ` 0 ) ) )