Metamath Proof Explorer

Theorem cmdfval

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

Ref Expression
Assertion cmdfval ( 𝐶 Colimit 𝐷 ) = ( 𝑓 ∈ ( 𝐷 Func 𝐶 ) ↦ ( ( 𝐶 Δfunc 𝐷 ) ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝑓 ) )

Proof

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