Theorem reldmlmd2

Description: The domain of ( C Limit D ) is a relation. (Contributed by Zhi Wang, 14-Nov-2025)

	Ref	Expression
Assertion	reldmlmd2	Could not format assertion : No typesetting found for |- Rel dom ( C Limit D ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		relfunc	$$⊢\mathrm{Rel}\left(D\mathrm{Func}C\right)$$
2		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 |-
3		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 |-
4	2 3	dmmpti	Could not format dom ( C Limit D ) = ( D Func C ) : No typesetting found for |- dom ( C Limit D ) = ( D Func C ) with typecode |-
5	4	releqi	Could not format ( Rel dom ( C Limit D ) <-> Rel ( D Func C ) ) : No typesetting found for |- ( Rel dom ( C Limit D ) <-> Rel ( D Func C ) ) with typecode |-
6	1 5	mpbir	Could not format Rel dom ( C Limit D ) : No typesetting found for |- Rel dom ( C Limit D ) with typecode |-