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 Could not format assertion : No typesetting found for |- Rel ( ( C Limit D ) ` F ) with typecode |-

Proof

Step Hyp Ref Expression
1 relup Could not format Rel ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) : No typesetting found for |- Rel ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) with typecode |-
2 lmdfval2 Could not format ( ( C Limit D ) ` F ) = ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) : No typesetting found for |- ( ( C Limit D ) ` F ) = ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) with typecode |-
3 2 releqi Could not format ( Rel ( ( C Limit D ) ` F ) <-> Rel ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) ) : No typesetting found for |- ( Rel ( ( C Limit D ) ` F ) <-> Rel ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) ) with typecode |-
4 1 3 mpbir Could not format Rel ( ( C Limit D ) ` F ) : No typesetting found for |- Rel ( ( C Limit D ) ` F ) with typecode |-