pcorevcl

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

		Ref	Expression
	Hypothesis	pcorev.1	$⊢ G = (x \in [0, 1] ⟼ F (1 - x))$
	Assertion	pcorevcl	$⊢ F \in (II Cn J) \to (G \in (II Cn J) \land G (0) = F (1) \land G (1) = F (0))$

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

Metamath Proof Explorer