Theorem reldmcmd2

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

	Ref	Expression
Assertion	reldmcmd2	Could not format assertion : No typesetting found for |- Rel dom ( C Colimit D ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		relfunc	$$⊢\mathrm{Rel}\left(D\mathrm{Func}C\right)$$
2		ovex	Could not format ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) e. _V : No typesetting found for |- ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) e. _V with typecode |-
3		cmdfval	Could not format ( C Colimit D ) = ( f e. ( D Func C ) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) ) : No typesetting found for |- ( C Colimit D ) = ( f e. ( D Func C ) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) ) with typecode |-
4	2 3	dmmpti	Could not format dom ( C Colimit D ) = ( D Func C ) : No typesetting found for |- dom ( C Colimit D ) = ( D Func C ) with typecode |-
5	4	releqi	Could not format ( Rel dom ( C Colimit D ) <-> Rel ( D Func C ) ) : No typesetting found for |- ( Rel dom ( C Colimit D ) <-> Rel ( D Func C ) ) with typecode |-
6	1 5	mpbir	Could not format Rel dom ( C Colimit D ) : No typesetting found for |- Rel dom ( C Colimit D ) with typecode |-