Metamath Proof Explorer

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 ( C Limit D )

Proof

Step Hyp Ref Expression
1 relfunc 
 |-  Rel ( D Func C )
2 ovex 
 |-  ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) f ) e. _V
3 lmdfval 
 |-  ( C Limit D ) = ( f e. ( D Func C ) |-> ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) f ) )
4 2 3 dmmpti 
 |-  dom ( C Limit D ) = ( D Func C )
5 4 releqi 
 |-  ( Rel dom ( C Limit D ) <-> Rel ( D Func C ) )
6 1 5 mpbir 
 |-  Rel dom ( C Limit D )