Metamath Proof Explorer

Theorem reldmcmd

Description: The domain of Colimit is a relation. (Contributed by Zhi Wang, 12-Nov-2025)

Ref Expression
Assertion reldmcmd 
|- Rel dom Colimit

Proof

Step Hyp Ref Expression
1 df-cmd 
 |-  Colimit = ( c e. _V , d e. _V |-> ( f e. ( d Func c ) |-> ( ( c DiagFunc d ) ( c UP ( d FuncCat c ) ) f ) ) )
2 1 reldmmpo 
 |-  Rel dom Colimit