Metamath Proof Explorer


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 *𝑝J=fIICnJ,gIICnJx01ifx12f2xg2x1

Proof

Step Hyp Ref Expression
1 oveq2 j=JIICnj=IICnJ
2 eqidd j=Jx01ifx12f2xg2x1=x01ifx12f2xg2x1
3 1 1 2 mpoeq123dv j=JfIICnj,gIICnjx01ifx12f2xg2x1=fIICnJ,gIICnJx01ifx12f2xg2x1
4 df-pco *𝑝=jTopfIICnj,gIICnjx01ifx12f2xg2x1
5 ovex IICnJV
6 5 5 mpoex fIICnJ,gIICnJx01ifx12f2xg2x1V
7 3 4 6 fvmpt JTop*𝑝J=fIICnJ,gIICnJx01ifx12f2xg2x1
8 4 fvmptndm ¬JTop*𝑝J=
9 cntop2 fIICnJJTop
10 9 con3i ¬JTop¬fIICnJ
11 10 eq0rdv ¬JTopIICnJ=
12 11 olcd ¬JTopIICnJ=IICnJ=
13 0mpo0 IICnJ=IICnJ=fIICnJ,gIICnJx01ifx12f2xg2x1=
14 12 13 syl ¬JTopfIICnJ,gIICnJx01ifx12f2xg2x1=
15 8 14 eqtr4d ¬JTop*𝑝J=fIICnJ,gIICnJx01ifx12f2xg2x1
16 7 15 pm2.61i *𝑝J=fIICnJ,gIICnJx01ifx12f2xg2x1