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 0 1 F 1 x
Assertion pcorevcl F II Cn J G II Cn J G 0 = F 1 G 1 = F 0

Proof

Step Hyp Ref Expression
1 pcorev.1 G = x 0 1 F 1 x
2 iitopon II TopOn 0 1
3 2 a1i F II Cn J II TopOn 0 1
4 iirevcn x 0 1 1 x II Cn II
5 4 a1i F II Cn J x 0 1 1 x II Cn II
6 id F II Cn J F II Cn J
7 3 5 6 cnmpt11f F II Cn J x 0 1 F 1 x II Cn J
8 1 7 eqeltrid F II Cn J G II Cn J
9 0elunit 0 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 V
15 13 1 14 fvmpt 0 0 1 G 0 = F 1
16 9 15 mp1i F II Cn J G 0 = F 1
17 1elunit 1 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 V
23 21 1 22 fvmpt 1 0 1 G 1 = F 0
24 17 23 mp1i F II Cn J G 1 = F 0
25 8 16 24 3jca F II Cn J G II Cn J G 0 = F 1 G 1 = F 0