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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq2 | |
|
2 | eqidd | |
|
3 | 1 1 2 | mpoeq123dv | |
4 | df-pco | |
|
5 | ovex | |
|
6 | 5 5 | mpoex | |
7 | 3 4 6 | fvmpt | |
8 | 4 | fvmptndm | |
9 | cntop2 | |
|
10 | 9 | con3i | |
11 | 10 | eq0rdv | |
12 | 11 | olcd | |
13 | 0mpo0 | |
|
14 | 12 13 | syl | |
15 | 8 14 | eqtr4d | |
16 | 7 15 | pm2.61i | |