Theorem reldmlmd

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

	Ref	Expression
Assertion	reldmlmd	|- Rel dom Limit

Proof

Step	Hyp	Ref	Expression
1		df-lmd	|- Limit = ( c e. _V , d e. _V |-> ( f e. ( d Func c ) |-> ( ( oppFunc ` ( c DiagFunc d ) ) ( ( oppCat ` c ) UP ( oppCat ` ( d FuncCat c ) ) ) f ) ) )
2	1	reldmmpo	|- Rel dom Limit