Theorem lmdfval

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

	Ref	Expression
Assertion	lmdfval	Could not format assertion : 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 |-

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