Theorem pcorevcl

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

	Ref	Expression
Hypothesis	pcorev.1	⊢ 𝐺 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( 1 − 𝑥 ) ) )
Assertion	pcorevcl	⊢ ( 𝐹 ∈ ( II Cn 𝐽 ) → ( 𝐺 ∈ ( II Cn 𝐽 ) ∧ ( 𝐺 ‘ 0 ) = ( 𝐹 ‘ 1 ) ∧ ( 𝐺 ‘ 1 ) = ( 𝐹 ‘ 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pcorev.1	⊢ 𝐺 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( 1 − 𝑥 ) ) )
2		iitopon	⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
3	2	a1i	⊢ ( 𝐹 ∈ ( II Cn 𝐽 ) → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
4		iirevcn	⊢ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 1 − 𝑥 ) ) ∈ ( II Cn II )
5	4	a1i	⊢ ( 𝐹 ∈ ( II Cn 𝐽 ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 1 − 𝑥 ) ) ∈ ( II Cn II ) )
6		id	⊢ ( 𝐹 ∈ ( II Cn 𝐽 ) → 𝐹 ∈ ( II Cn 𝐽 ) )
7	3 5 6	cnmpt11f	⊢ ( 𝐹 ∈ ( II Cn 𝐽 ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( 1 − 𝑥 ) ) ) ∈ ( II Cn 𝐽 ) )
8	1 7	eqeltrid	⊢ ( 𝐹 ∈ ( II Cn 𝐽 ) → 𝐺 ∈ ( II Cn 𝐽 ) )
9		0elunit	⊢ 0 ∈ ( 0 [,] 1 )
10		oveq2	⊢ ( 𝑥 = 0 → ( 1 − 𝑥 ) = ( 1 − 0 ) )
11		1m0e1	⊢ ( 1 − 0 ) = 1
12	10 11	eqtrdi	⊢ ( 𝑥 = 0 → ( 1 − 𝑥 ) = 1 )
13	12	fveq2d	⊢ ( 𝑥 = 0 → ( 𝐹 ‘ ( 1 − 𝑥 ) ) = ( 𝐹 ‘ 1 ) )
14		fvex	⊢ ( 𝐹 ‘ 1 ) ∈ V
15	13 1 14	fvmpt	⊢ ( 0 ∈ ( 0 [,] 1 ) → ( 𝐺 ‘ 0 ) = ( 𝐹 ‘ 1 ) )
16	9 15	mp1i	⊢ ( 𝐹 ∈ ( II Cn 𝐽 ) → ( 𝐺 ‘ 0 ) = ( 𝐹 ‘ 1 ) )
17		1elunit	⊢ 1 ∈ ( 0 [,] 1 )
18		oveq2	⊢ ( 𝑥 = 1 → ( 1 − 𝑥 ) = ( 1 − 1 ) )
19		1m1e0	⊢ ( 1 − 1 ) = 0
20	18 19	eqtrdi	⊢ ( 𝑥 = 1 → ( 1 − 𝑥 ) = 0 )
21	20	fveq2d	⊢ ( 𝑥 = 1 → ( 𝐹 ‘ ( 1 − 𝑥 ) ) = ( 𝐹 ‘ 0 ) )
22		fvex	⊢ ( 𝐹 ‘ 0 ) ∈ V
23	21 1 22	fvmpt	⊢ ( 1 ∈ ( 0 [,] 1 ) → ( 𝐺 ‘ 1 ) = ( 𝐹 ‘ 0 ) )
24	17 23	mp1i	⊢ ( 𝐹 ∈ ( II Cn 𝐽 ) → ( 𝐺 ‘ 1 ) = ( 𝐹 ‘ 0 ) )
25	8 16 24	3jca	⊢ ( 𝐹 ∈ ( II Cn 𝐽 ) → ( 𝐺 ∈ ( II Cn 𝐽 ) ∧ ( 𝐺 ‘ 0 ) = ( 𝐹 ‘ 1 ) ∧ ( 𝐺 ‘ 1 ) = ( 𝐹 ‘ 0 ) ) )