Theorem cmdfval2

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

	Ref	Expression
Assertion	cmdfval2	Could not format assertion : No typesetting found for |- ( ( C Colimit D ) ` F ) = ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		cmdfval	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 |-
2	1	mptrcl	Could not format ( f e. ( ( C Colimit D ) ` F ) -> F e. ( D Func C ) ) : No typesetting found for |- ( f e. ( ( C Colimit D ) ` F ) -> F e. ( D Func C ) ) with typecode |-
3		eqid	$$⊢D\mathrm{FuncCat}C=D\mathrm{FuncCat}C$$
4	3	fucbas	$$⊢D\mathrm{Func}C={\mathrm{Base}}_{\left(D\mathrm{FuncCat}C\right)}$$
5	4	uprcl	Could not format ( f e. ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) -> ( ( C DiagFunc D ) e. ( C Func ( D FuncCat C ) ) /\ F e. ( D Func C ) ) ) : No typesetting found for |- ( f e. ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) -> ( ( C DiagFunc D ) e. ( C Func ( D FuncCat C ) ) /\ F e. ( D Func C ) ) ) with typecode |-
6	5	simprd	Could not format ( f e. ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) -> F e. ( D Func C ) ) : No typesetting found for |- ( f e. ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) -> F e. ( D Func C ) ) with typecode |-
7		oveq2	Could not format ( f = F -> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) = ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) ) : No typesetting found for |- ( f = F -> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) f ) = ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) ) with typecode |-
8		ovex	Could not format ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) e. _V : No typesetting found for |- ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) e. _V with typecode |-
9	7 1 8	fvmpt	Could not format ( F e. ( D Func C ) -> ( ( C Colimit D ) ` F ) = ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) ) : No typesetting found for |- ( F e. ( D Func C ) -> ( ( C Colimit D ) ` F ) = ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) ) with typecode |-
10	9	eleq2d	Could not format ( F e. ( D Func C ) -> ( f e. ( ( C Colimit D ) ` F ) <-> f e. ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) ) ) : No typesetting found for |- ( F e. ( D Func C ) -> ( f e. ( ( C Colimit D ) ` F ) <-> f e. ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) ) ) with typecode |-
11	2 6 10	pm5.21nii	Could not format ( f e. ( ( C Colimit D ) ` F ) <-> f e. ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) ) : No typesetting found for |- ( f e. ( ( C Colimit D ) ` F ) <-> f e. ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) ) with typecode |-
12	11	eqriv	Could not format ( ( C Colimit D ) ` F ) = ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) : No typesetting found for |- ( ( C Colimit D ) ` F ) = ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) with typecode |-