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