Metamath Proof Explorer

Theorem cmdfval2

Description: The set of colimits of a diagram. (Contributed by Zhi Wang, 12-Nov-2025)

Ref Expression
Assertion cmdfval2 
|- ( ( C Colimit D ) ` F ) = ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F )

Proof

Step Hyp Ref Expression
1 cmdfval 
 |-  ( C Colimit D ) = ( f e. ( D Func C ) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) )
2 1 mptrcl 
 |-  ( f e. ( ( C Colimit D ) ` F ) -> F e. ( D Func C ) )
3 eqid 
 |-  ( D FuncCat C ) = ( D FuncCat C )
4 3 fucbas 
 |-  ( D Func C ) = ( Base ` ( D FuncCat C ) )
5 4 uprcl 
 |-  ( f e. ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) -> ( ( C DiagFunc D ) e. ( C Func ( D FuncCat C ) ) /\ F e. ( D Func C ) ) )
6 5 simprd 
 |-  ( f e. ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) -> F e. ( D Func C ) )
7 oveq2 
 |-  ( f = F -> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) = ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) )
8 ovex 
 |-  ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) e. _V
9 7 1 8 fvmpt 
 |-  ( F e. ( D Func C ) -> ( ( C Colimit D ) ` F ) = ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) )
10 9 eleq2d 
 |-  ( F e. ( D Func C ) -> ( f e. ( ( C Colimit D ) ` F ) <-> f e. ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) ) )
11 2 6 10 pm5.21nii 
 |-  ( f e. ( ( C Colimit D ) ` F ) <-> f e. ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) )
12 11 eqriv 
 |-  ( ( C Colimit D ) ` F ) = ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F )