Theorem reldmlmd

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

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

Proof

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