Metamath Proof Explorer

Theorem lmdfval

Description: Function value of Limit . (Contributed by Zhi Wang, 14-Nov-2025)

Ref Expression
Assertion lmdfval 
|- ( C Limit D ) = ( f e. ( D Func C ) |-> ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) f ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( c = C /\ d = D ) -> d = D )
2 simpl 
 |-  ( ( c = C /\ d = D ) -> c = C )
3 1 2 oveq12d 
 |-  ( ( c = C /\ d = D ) -> ( d Func c ) = ( D Func C ) )
4 2 fveq2d 
 |-  ( ( c = C /\ d = D ) -> ( oppCat ` c ) = ( oppCat ` C ) )
5 1 2 oveq12d 
 |-  ( ( c = C /\ d = D ) -> ( d FuncCat c ) = ( D FuncCat C ) )
6 5 fveq2d 
 |-  ( ( c = C /\ d = D ) -> ( oppCat ` ( d FuncCat c ) ) = ( oppCat ` ( D FuncCat C ) ) )
7 4 6 oveq12d 
 |-  ( ( c = C /\ d = D ) -> ( ( oppCat ` c ) UP ( oppCat ` ( d FuncCat c ) ) ) = ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) )
8 oveq12 
 |-  ( ( c = C /\ d = D ) -> ( c DiagFunc d ) = ( C DiagFunc D ) )
9 8 fveq2d 
 |-  ( ( c = C /\ d = D ) -> ( oppFunc ` ( c DiagFunc d ) ) = ( oppFunc ` ( C DiagFunc D ) ) )
10 eqidd 
 |-  ( ( c = C /\ d = D ) -> f = f )
11 7 9 10 oveq123d 
 |-  ( ( c = C /\ d = D ) -> ( ( oppFunc ` ( c DiagFunc d ) ) ( ( oppCat ` c ) UP ( oppCat ` ( d FuncCat c ) ) ) f ) = ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) f ) )
12 3 11 mpteq12dv 
 |-  ( ( c = C /\ d = D ) -> ( f e. ( d Func c ) |-> ( ( oppFunc ` ( c DiagFunc d ) ) ( ( oppCat ` c ) UP ( oppCat ` ( d FuncCat c ) ) ) f ) ) = ( f e. ( D Func C ) |-> ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) f ) ) )
13 df-lmd 
 |-  Limit = ( c e. _V , d e. _V |-> ( f e. ( d Func c ) |-> ( ( oppFunc ` ( c DiagFunc d ) ) ( ( oppCat ` c ) UP ( oppCat ` ( d FuncCat c ) ) ) f ) ) )
14 ovex 
 |-  ( D Func C ) e. _V
15 14 mptex 
 |-  ( f e. ( D Func C ) |-> ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) f ) ) e. _V
16 12 13 15 ovmpoa 
 |-  ( ( C e. _V /\ D e. _V ) -> ( C Limit D ) = ( f e. ( D Func C ) |-> ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) f ) ) )
17 reldmlmd 
 |-  Rel dom Limit
18 17 ovprc 
 |-  ( -. ( C e. _V /\ D e. _V ) -> ( C Limit D ) = (/) )
19 ancom 
 |-  ( ( C e. _V /\ D e. _V ) <-> ( D e. _V /\ C e. _V ) )
20 reldmfunc 
 |-  Rel dom Func
21 20 ovprc 
 |-  ( -. ( D e. _V /\ C e. _V ) -> ( D Func C ) = (/) )
22 19 21 sylnbi 
 |-  ( -. ( C e. _V /\ D e. _V ) -> ( D Func C ) = (/) )
23 22 mpteq1d 
 |-  ( -. ( C e. _V /\ D e. _V ) -> ( f e. ( D Func C ) |-> ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) f ) ) = ( f e. (/) |-> ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) f ) ) )
24 mpt0 
 |-  ( f e. (/) |-> ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) f ) ) = (/)
25 23 24 eqtrdi 
 |-  ( -. ( C e. _V /\ D e. _V ) -> ( f e. ( D Func C ) |-> ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) f ) ) = (/) )
26 18 25 eqtr4d 
 |-  ( -. ( C e. _V /\ D e. _V ) -> ( C Limit D ) = ( f e. ( D Func C ) |-> ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) f ) ) )
27 16 26 pm2.61i 
 |-  ( C Limit D ) = ( f e. ( D Func C ) |-> ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) f ) )