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