Theorem mndtccat

Description: The function value is a category. (Contributed by Zhi Wang, 22-Sep-2024)

	Ref	Expression
Hypotheses	mndtccat.c	$$⊢\phi \to C=\mathrm{MndToCat}\left(M\right)$$
	mndtccat.m	$$⊢\phi \to M\in \mathrm{Mnd}$$
Assertion	mndtccat	$$⊢\phi \to C\in \mathrm{Cat}$$

Proof

Step	Hyp	Ref	Expression
1		mndtccat.c	$$⊢\phi \to C=\mathrm{MndToCat}\left(M\right)$$
2		mndtccat.m	$$⊢\phi \to M\in \mathrm{Mnd}$$
3	1 2	mndtccatid	$$⊢\phi \to \left(C\in \mathrm{Cat}\wedge \mathrm{Id}\left(C\right)=\left(y\in {\mathrm{Base}}_C⟼0_M\right)\right)$$
4	3	simpld	$$⊢\phi \to C\in \mathrm{Cat}$$