Theorem lmdfval2

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

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

Proof

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