Metamath Proof Explorer

Theorem reldmcmd2

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

Ref Expression
Assertion reldmcmd2 
|- Rel dom ( C Colimit D )

Proof

Step Hyp Ref Expression
1 relfunc 
 |-  Rel ( D Func C )
2 ovex 
 |-  ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) e. _V
3 cmdfval 
 |-  ( C Colimit D ) = ( f e. ( D Func C ) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) )
4 2 3 dmmpti 
 |-  dom ( C Colimit D ) = ( D Func C )
5 4 releqi 
 |-  ( Rel dom ( C Colimit D ) <-> Rel ( D Func C ) )
6 1 5 mpbir 
 |-  Rel dom ( C Colimit D )