Metamath Proof Explorer

Theorem lmdfval

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

Ref Expression
Assertion lmdfval ( 𝐶 Limit 𝐷 ) = ( 𝑓 ∈ ( 𝐷 Func 𝐶 ) ↦ ( ( oppFunc ‘ ( 𝐶 Δfunc 𝐷 ) ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝑓 ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → 𝑑 = 𝐷 )
2 simpl ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → 𝑐 = 𝐶 )
3 1 2 oveq12d ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( 𝑑 Func 𝑐 ) = ( 𝐷 Func 𝐶 ) )
4 2 fveq2d ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( oppCat ‘ 𝑐 ) = ( oppCat ‘ 𝐶 ) )
5 1 2 oveq12d ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( 𝑑 FuncCat 𝑐 ) = ( 𝐷 FuncCat 𝐶 ) )
6 5 fveq2d ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( oppCat ‘ ( 𝑑 FuncCat 𝑐 ) ) = ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) )
7 4 6 oveq12d ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( ( oppCat ‘ 𝑐 ) UP ( oppCat ‘ ( 𝑑 FuncCat 𝑐 ) ) ) = ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) )
8 oveq12 ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( 𝑐 Δfunc 𝑑 ) = ( 𝐶 Δfunc 𝐷 ) )
9 8 fveq2d ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( oppFunc ‘ ( 𝑐 Δfunc 𝑑 ) ) = ( oppFunc ‘ ( 𝐶 Δfunc 𝐷 ) ) )
10 eqidd ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → 𝑓 = 𝑓 )
11 7 9 10 oveq123d ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( ( oppFunc ‘ ( 𝑐 Δfunc 𝑑 ) ) ( ( oppCat ‘ 𝑐 ) UP ( oppCat ‘ ( 𝑑 FuncCat 𝑐 ) ) ) 𝑓 ) = ( ( oppFunc ‘ ( 𝐶 Δfunc 𝐷 ) ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝑓 ) )
12 3 11 mpteq12dv ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( 𝑓 ∈ ( 𝑑 Func 𝑐 ) ↦ ( ( oppFunc ‘ ( 𝑐 Δfunc 𝑑 ) ) ( ( oppCat ‘ 𝑐 ) UP ( oppCat ‘ ( 𝑑 FuncCat 𝑐 ) ) ) 𝑓 ) ) = ( 𝑓 ∈ ( 𝐷 Func 𝐶 ) ↦ ( ( oppFunc ‘ ( 𝐶 Δfunc 𝐷 ) ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝑓 ) ) )
13 df-lmd ⊢ Limit = ( 𝑐 ∈ V , 𝑑 ∈ V ↦ ( 𝑓 ∈ ( 𝑑 Func 𝑐 ) ↦ ( ( oppFunc ‘ ( 𝑐 Δfunc 𝑑 ) ) ( ( oppCat ‘ 𝑐 ) UP ( oppCat ‘ ( 𝑑 FuncCat 𝑐 ) ) ) 𝑓 ) ) )
14 ovex ⊢ ( 𝐷 Func 𝐶 ) ∈ V
15 14 mptex ⊢ ( 𝑓 ∈ ( 𝐷 Func 𝐶 ) ↦ ( ( oppFunc ‘ ( 𝐶 Δfunc 𝐷 ) ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝑓 ) ) ∈ V
16 12 13 15 ovmpoa ⊢ ( ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → ( 𝐶 Limit 𝐷 ) = ( 𝑓 ∈ ( 𝐷 Func 𝐶 ) ↦ ( ( oppFunc ‘ ( 𝐶 Δfunc 𝐷 ) ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝑓 ) ) )
17 reldmlmd ⊢ Rel dom Limit
18 17 ovprc ⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → ( 𝐶 Limit 𝐷 ) = ∅ )
19 ancom ⊢ ( ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ↔ ( 𝐷 ∈ V ∧ 𝐶 ∈ V ) )
20 reldmfunc ⊢ Rel dom Func
21 20 ovprc ⊢ ( ¬ ( 𝐷 ∈ V ∧ 𝐶 ∈ V ) → ( 𝐷 Func 𝐶 ) = ∅ )
22 19 21 sylnbi ⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → ( 𝐷 Func 𝐶 ) = ∅ )
23 22 mpteq1d ⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → ( 𝑓 ∈ ( 𝐷 Func 𝐶 ) ↦ ( ( oppFunc ‘ ( 𝐶 Δfunc 𝐷 ) ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝑓 ) ) = ( 𝑓 ∈ ∅ ↦ ( ( oppFunc ‘ ( 𝐶 Δfunc 𝐷 ) ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝑓 ) ) )
24 mpt0 ⊢ ( 𝑓 ∈ ∅ ↦ ( ( oppFunc ‘ ( 𝐶 Δfunc 𝐷 ) ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝑓 ) ) = ∅
25 23 24 eqtrdi ⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → ( 𝑓 ∈ ( 𝐷 Func 𝐶 ) ↦ ( ( oppFunc ‘ ( 𝐶 Δfunc 𝐷 ) ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝑓 ) ) = ∅ )
26 18 25 eqtr4d ⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → ( 𝐶 Limit 𝐷 ) = ( 𝑓 ∈ ( 𝐷 Func 𝐶 ) ↦ ( ( oppFunc ‘ ( 𝐶 Δfunc 𝐷 ) ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝑓 ) ) )
27 16 26 pm2.61i ⊢ ( 𝐶 Limit 𝐷 ) = ( 𝑓 ∈ ( 𝐷 Func 𝐶 ) ↦ ( ( oppFunc ‘ ( 𝐶 Δfunc 𝐷 ) ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝑓 ) )