Metamath Proof Explorer

Theorem rellmd

Description: The set of limits of a diagram is a relation. (Contributed by Zhi Wang, 14-Nov-2025)

Ref Expression
Assertion rellmd 
|- Rel ( ( C Limit D ) ` F )

Proof

Step Hyp Ref Expression
1 relup 
 |-  Rel ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F )
2 lmdfval2 
 |-  ( ( C Limit D ) ` F ) = ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F )
3 2 releqi 
 |-  ( Rel ( ( C Limit D ) ` F ) <-> Rel ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) )
4 1 3 mpbir 
 |-  Rel ( ( C Limit D ) ` F )