Metamath Proof Explorer

Theorem relcmd

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

Ref Expression
Assertion relcmd 
|- Rel ( ( C Colimit D ) ` F )

Proof

Step Hyp Ref Expression
1 relup 
 |-  Rel ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F )
2 cmdfval2 
 |-  ( ( C Colimit D ) ` F ) = ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F )
3 2 releqi 
 |-  ( Rel ( ( C Colimit D ) ` F ) <-> Rel ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) )
4 1 3 mpbir 
 |-  Rel ( ( C Colimit D ) ` F )