Metamath Proof Explorer

Theorem lmdfval2

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

Ref Expression
Assertion lmdfval2 
|- ( ( C Limit D ) ` F ) = ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F )

Proof

Step Hyp Ref Expression
1 lmdfval 
 |-  ( C Limit D ) = ( f e. ( D Func C ) |-> ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) f ) )
2 1 mptrcl 
 |-  ( f e. ( ( C Limit D ) ` F ) -> F e. ( D Func C ) )
3 eqid 
 |-  ( oppCat ` ( D FuncCat C ) ) = ( oppCat ` ( D FuncCat C ) )
4 eqid 
 |-  ( D FuncCat C ) = ( D FuncCat C )
5 4 fucbas 
 |-  ( D Func C ) = ( Base ` ( D FuncCat C ) )
6 3 5 oppcbas 
 |-  ( D Func C ) = ( Base ` ( oppCat ` ( D FuncCat C ) ) )
7 6 uprcl 
 |-  ( f e. ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) -> ( ( oppFunc ` ( C DiagFunc D ) ) e. ( ( oppCat ` C ) Func ( oppCat ` ( D FuncCat C ) ) ) /\ F e. ( D Func C ) ) )
8 7 simprd 
 |-  ( f e. ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) -> F e. ( D Func C ) )
9 oveq2 
 |-  ( f = F -> ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) f ) = ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) )
10 ovex 
 |-  ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) e. _V
11 9 1 10 fvmpt 
 |-  ( F e. ( D Func C ) -> ( ( C Limit D ) ` F ) = ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) )
12 11 eleq2d 
 |-  ( F e. ( D Func C ) -> ( f e. ( ( C Limit D ) ` F ) <-> f e. ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) ) )
13 2 8 12 pm5.21nii 
 |-  ( f e. ( ( C Limit D ) ` F ) <-> f e. ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) )
14 13 eqriv 
 |-  ( ( C Limit D ) ` F ) = ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F )