Theorem pcofval

Description: The value of the path concatenation function on a topological space. (Contributed by Jeff Madsen, 15-Jun-2010) (Revised by Mario Carneiro, 7-Jun-2014) (Proof shortened by AV, 2-Mar-2024)

	Ref	Expression
Assertion	pcofval	⊢ ( *𝑝 ‘ 𝐽 ) = ( 𝑓 ∈ ( II Cn 𝐽 ) , 𝑔 ∈ ( II Cn 𝐽 ) ↦ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝑓 ‘ ( 2 · 𝑥 ) ) , ( 𝑔 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑗 = 𝐽 → ( II Cn 𝑗 ) = ( II Cn 𝐽 ) )
2		eqidd	⊢ ( 𝑗 = 𝐽 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝑓 ‘ ( 2 · 𝑥 ) ) , ( 𝑔 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝑓 ‘ ( 2 · 𝑥 ) ) , ( 𝑔 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) )
3	1 1 2	mpoeq123dv	⊢ ( 𝑗 = 𝐽 → ( 𝑓 ∈ ( II Cn 𝑗 ) , 𝑔 ∈ ( II Cn 𝑗 ) ↦ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝑓 ‘ ( 2 · 𝑥 ) ) , ( 𝑔 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) ) = ( 𝑓 ∈ ( II Cn 𝐽 ) , 𝑔 ∈ ( II Cn 𝐽 ) ↦ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝑓 ‘ ( 2 · 𝑥 ) ) , ( 𝑔 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) ) )
4		df-pco	⊢ *𝑝 = ( 𝑗 ∈ Top ↦ ( 𝑓 ∈ ( II Cn 𝑗 ) , 𝑔 ∈ ( II Cn 𝑗 ) ↦ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝑓 ‘ ( 2 · 𝑥 ) ) , ( 𝑔 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) ) )
5		ovex	⊢ ( II Cn 𝐽 ) ∈ V
6	5 5	mpoex	⊢ ( 𝑓 ∈ ( II Cn 𝐽 ) , 𝑔 ∈ ( II Cn 𝐽 ) ↦ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝑓 ‘ ( 2 · 𝑥 ) ) , ( 𝑔 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) ) ∈ V
7	3 4 6	fvmpt	⊢ ( 𝐽 ∈ Top → ( *𝑝 ‘ 𝐽 ) = ( 𝑓 ∈ ( II Cn 𝐽 ) , 𝑔 ∈ ( II Cn 𝐽 ) ↦ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝑓 ‘ ( 2 · 𝑥 ) ) , ( 𝑔 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) ) )
8	4	fvmptndm	⊢ ( ¬ 𝐽 ∈ Top → ( *𝑝 ‘ 𝐽 ) = ∅ )
9		cntop2	⊢ ( 𝑓 ∈ ( II Cn 𝐽 ) → 𝐽 ∈ Top )
10	9	con3i	⊢ ( ¬ 𝐽 ∈ Top → ¬ 𝑓 ∈ ( II Cn 𝐽 ) )
11	10	eq0rdv	⊢ ( ¬ 𝐽 ∈ Top → ( II Cn 𝐽 ) = ∅ )
12	11	olcd	⊢ ( ¬ 𝐽 ∈ Top → ( ( II Cn 𝐽 ) = ∅ ∨ ( II Cn 𝐽 ) = ∅ ) )
13		0mpo0	⊢ ( ( ( II Cn 𝐽 ) = ∅ ∨ ( II Cn 𝐽 ) = ∅ ) → ( 𝑓 ∈ ( II Cn 𝐽 ) , 𝑔 ∈ ( II Cn 𝐽 ) ↦ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝑓 ‘ ( 2 · 𝑥 ) ) , ( 𝑔 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) ) = ∅ )
14	12 13	syl	⊢ ( ¬ 𝐽 ∈ Top → ( 𝑓 ∈ ( II Cn 𝐽 ) , 𝑔 ∈ ( II Cn 𝐽 ) ↦ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝑓 ‘ ( 2 · 𝑥 ) ) , ( 𝑔 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) ) = ∅ )
15	8 14	eqtr4d	⊢ ( ¬ 𝐽 ∈ Top → ( *𝑝 ‘ 𝐽 ) = ( 𝑓 ∈ ( II Cn 𝐽 ) , 𝑔 ∈ ( II Cn 𝐽 ) ↦ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝑓 ‘ ( 2 · 𝑥 ) ) , ( 𝑔 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) ) )
16	7 15	pm2.61i	⊢ ( *𝑝 ‘ 𝐽 ) = ( 𝑓 ∈ ( II Cn 𝐽 ) , 𝑔 ∈ ( II Cn 𝐽 ) ↦ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝑓 ‘ ( 2 · 𝑥 ) ) , ( 𝑔 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) )