Theorem cmdfval

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

	Ref	Expression
Assertion	cmdfval	Could not format assertion : No typesetting found for |- ( C Colimit D ) = ( f e. ( D Func C ) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(c=C\wedge d=D\right)\to d=D$$
2		simpl	$$⊢\left(c=C\wedge d=D\right)\to c=C$$
3	1 2	oveq12d	$$⊢\left(c=C\wedge d=D\right)\to d\mathrm{Func}c=D\mathrm{Func}C$$
4	1 2	oveq12d	$$⊢\left(c=C\wedge d=D\right)\to d\mathrm{FuncCat}c=D\mathrm{FuncCat}C$$
5	2 4	oveq12d	Could not format ( ( c = C /\ d = D ) -> ( c UP ( d FuncCat c ) ) = ( C UP ( D FuncCat C ) ) ) : No typesetting found for |- ( ( c = C /\ d = D ) -> ( c UP ( d FuncCat c ) ) = ( C UP ( D FuncCat C ) ) ) with typecode |-
6		oveq12	$$⊢\left(c=C\wedge d=D\right)\to c{\Delta }_{\mathrm{func}}d=C{\Delta }_{\mathrm{func}}D$$
7		eqidd	$$⊢\left(c=C\wedge d=D\right)\to f=f$$
8	5 6 7	oveq123d	Could not format ( ( c = C /\ d = D ) -> ( ( c DiagFunc d ) ( c UP ( d FuncCat c ) ) f ) = ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) ) : No typesetting found for |- ( ( c = C /\ d = D ) -> ( ( c DiagFunc d ) ( c UP ( d FuncCat c ) ) f ) = ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) ) with typecode |-
9	3 8	mpteq12dv	Could not format ( ( c = C /\ d = D ) -> ( f e. ( d Func c ) |-> ( ( c DiagFunc d ) ( c UP ( d FuncCat c ) ) f ) ) = ( f e. ( D Func C ) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) ) ) : No typesetting found for |- ( ( c = C /\ d = D ) -> ( f e. ( d Func c ) |-> ( ( c DiagFunc d ) ( c UP ( d FuncCat c ) ) f ) ) = ( f e. ( D Func C ) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) ) ) with typecode |-
10		df-cmd	Could not format Colimit = ( c e. _V , d e. _V |-> ( f e. ( d Func c ) |-> ( ( c DiagFunc d ) ( c UP ( d FuncCat c ) ) f ) ) ) : No typesetting found for |- Colimit = ( c e. _V , d e. _V |-> ( f e. ( d Func c ) |-> ( ( c DiagFunc d ) ( c UP ( d FuncCat c ) ) f ) ) ) with typecode |-
11		ovex	$$⊢D\mathrm{Func}C\in \mathrm{V}$$
12	11	mptex	Could not format ( f e. ( D Func C ) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) ) e. _V : No typesetting found for |- ( f e. ( D Func C ) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) ) e. _V with typecode |-
13	9 10 12	ovmpoa	Could not format ( ( C e. _V /\ D e. _V ) -> ( C Colimit D ) = ( f e. ( D Func C ) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) ) ) : No typesetting found for |- ( ( C e. _V /\ D e. _V ) -> ( C Colimit D ) = ( f e. ( D Func C ) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) ) ) with typecode |-
14		reldmcmd	Could not format Rel dom Colimit : No typesetting found for |- Rel dom Colimit with typecode |-
15	14	ovprc	Could not format ( -. ( C e. _V /\ D e. _V ) -> ( C Colimit D ) = (/) ) : No typesetting found for |- ( -. ( C e. _V /\ D e. _V ) -> ( C Colimit D ) = (/) ) with typecode |-
16		ancom	$$⊢\left(C\in \mathrm{V}\wedge D\in \mathrm{V}\right)\leftrightarrow \left(D\in \mathrm{V}\wedge C\in \mathrm{V}\right)$$
17		reldmfunc	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{Func}$$
18	17	ovprc	$$⊢\neg \left(D\in \mathrm{V}\wedge C\in \mathrm{V}\right)\to D\mathrm{Func}C=\varnothing$$
19	16 18	sylnbi	$$⊢\neg \left(C\in \mathrm{V}\wedge D\in \mathrm{V}\right)\to D\mathrm{Func}C=\varnothing$$
20	19	mpteq1d	Could not format ( -. ( C e. _V /\ D e. _V ) -> ( f e. ( D Func C ) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) ) = ( f e. (/) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) ) ) : No typesetting found for |- ( -. ( C e. _V /\ D e. _V ) -> ( f e. ( D Func C ) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) ) = ( f e. (/) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) ) ) with typecode |-
21		mpt0	Could not format ( f e. (/) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) ) = (/) : No typesetting found for |- ( f e. (/) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) ) = (/) with typecode |-
22	20 21	eqtrdi	Could not format ( -. ( C e. _V /\ D e. _V ) -> ( f e. ( D Func C ) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) ) = (/) ) : No typesetting found for |- ( -. ( C e. _V /\ D e. _V ) -> ( f e. ( D Func C ) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) ) = (/) ) with typecode |-
23	15 22	eqtr4d	Could not format ( -. ( C e. _V /\ D e. _V ) -> ( C Colimit D ) = ( f e. ( D Func C ) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) ) ) : No typesetting found for |- ( -. ( C e. _V /\ D e. _V ) -> ( C Colimit D ) = ( f e. ( D Func C ) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) ) ) with typecode |-
24	13 23	pm2.61i	Could not format ( C Colimit D ) = ( f e. ( D Func C ) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) ) : No typesetting found for |- ( C Colimit D ) = ( f e. ( D Func C ) |-> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) ) with typecode |-