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 ( 𝐶 Colimit 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		relfunc	⊢ Rel ( 𝐷 Func 𝐶 )
2		ovex	⊢ ( ( 𝐶 Δfunc 𝐷 ) ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝑓 ) ∈ V
3		cmdfval	⊢ ( 𝐶 Colimit 𝐷 ) = ( 𝑓 ∈ ( 𝐷 Func 𝐶 ) ↦ ( ( 𝐶 Δfunc 𝐷 ) ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝑓 ) )
4	2 3	dmmpti	⊢ dom ( 𝐶 Colimit 𝐷 ) = ( 𝐷 Func 𝐶 )
5	4	releqi	⊢ ( Rel dom ( 𝐶 Colimit 𝐷 ) ↔ Rel ( 𝐷 Func 𝐶 ) )
6	1 5	mpbir	⊢ Rel dom ( 𝐶 Colimit 𝐷 )