Theorem reldmlmd2

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

	Ref	Expression
Assertion	reldmlmd2	⊢ Rel dom ( 𝐶 Limit 𝐷 )

Proof

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