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 = ( 𝑐 ∈ V , 𝑑 ∈ V ↦ ( 𝑓 ∈ ( 𝑑 Func 𝑐 ) ↦ ( ( 𝑐 Δfunc 𝑑 ) ( 𝑐 UP ( 𝑑 FuncCat 𝑐 ) ) 𝑓 ) ) )
2	1	reldmmpo	⊢ Rel dom Colimit