Theorem reldmcmd

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

	Ref	Expression
Assertion	reldmcmd	Could not format assertion : No typesetting found for |- Rel dom Colimit with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-cmd	Could not format Colimit = ( c e. _V , d e. _V |-> ( f e. ( d Func c ) |-> ( ( c DiagFunc d ) ( c UP ( d FuncCat c ) ) f ) ) ) : No typesetting found for |- Colimit = ( c e. _V , d e. _V |-> ( f e. ( d Func c ) |-> ( ( c DiagFunc d ) ( c UP ( d FuncCat c ) ) f ) ) ) with typecode |-
2	1	reldmmpo	Could not format Rel dom Colimit : No typesetting found for |- Rel dom Colimit with typecode |-