Metamath Proof Explorer

Theorem cmdfval

Description: Function value of Colimit . (Contributed by Zhi Wang, 12-Nov-2025)

Ref Expression
Assertion cmdfval 
|- ( C Colimit D ) = ( f e. ( D Func C ) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( c = C /\ d = D ) -> d = D )
2 simpl 
 |-  ( ( c = C /\ d = D ) -> c = C )
3 1 2 oveq12d 
 |-  ( ( c = C /\ d = D ) -> ( d Func c ) = ( D Func C ) )
4 1 2 oveq12d 
 |-  ( ( c = C /\ d = D ) -> ( d FuncCat c ) = ( D FuncCat C ) )
5 2 4 oveq12d 
 |-  ( ( c = C /\ d = D ) -> ( c UP ( d FuncCat c ) ) = ( C UP ( D FuncCat C ) ) )
6 oveq12 
 |-  ( ( c = C /\ d = D ) -> ( c DiagFunc d ) = ( C DiagFunc D ) )
7 eqidd 
 |-  ( ( c = C /\ d = D ) -> f = f )
8 5 6 7 oveq123d 
 |-  ( ( c = C /\ d = D ) -> ( ( c DiagFunc d ) ( c UP ( d FuncCat c ) ) f ) = ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) )
9 3 8 mpteq12dv 
 |-  ( ( c = C /\ d = D ) -> ( f e. ( d Func c ) |-> ( ( c DiagFunc d ) ( c UP ( d FuncCat c ) ) f ) ) = ( f e. ( D Func C ) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) ) )
10 df-cmd 
 |-  Colimit = ( c e. _V , d e. _V |-> ( f e. ( d Func c ) |-> ( ( c DiagFunc d ) ( c UP ( d FuncCat c ) ) f ) ) )
11 ovex 
 |-  ( D Func C ) e. _V
12 11 mptex 
 |-  ( f e. ( D Func C ) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) ) e. _V
13 9 10 12 ovmpoa 
 |-  ( ( C e. _V /\ D e. _V ) -> ( C Colimit D ) = ( f e. ( D Func C ) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) ) )
14 reldmcmd 
 |-  Rel dom Colimit
15 14 ovprc 
 |-  ( -. ( C e. _V /\ D e. _V ) -> ( C Colimit D ) = (/) )
16 ancom 
 |-  ( ( C e. _V /\ D e. _V ) <-> ( D e. _V /\ C e. _V ) )
17 reldmfunc 
 |-  Rel dom Func
18 17 ovprc 
 |-  ( -. ( D e. _V /\ C e. _V ) -> ( D Func C ) = (/) )
19 16 18 sylnbi 
 |-  ( -. ( C e. _V /\ D e. _V ) -> ( D Func C ) = (/) )
20 19 mpteq1d 
 |-  ( -. ( C e. _V /\ D e. _V ) -> ( f e. ( D Func C ) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) ) = ( f e. (/) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) ) )
21 mpt0 
 |-  ( f e. (/) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) ) = (/)
22 20 21 eqtrdi 
 |-  ( -. ( C e. _V /\ D e. _V ) -> ( f e. ( D Func C ) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) ) = (/) )
23 15 22 eqtr4d 
 |-  ( -. ( C e. _V /\ D e. _V ) -> ( C Colimit D ) = ( f e. ( D Func C ) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) ) )
24 13 23 pm2.61i 
 |-  ( C Colimit D ) = ( f e. ( D Func C ) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) )