Theorem mndtccat

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

	Ref	Expression
Hypotheses	mndtccat.c	⊢ ( 𝜑 → 𝐶 = ( MndToCat ‘ 𝑀 ) )
	mndtccat.m	⊢ ( 𝜑 → 𝑀 ∈ Mnd )
Assertion	mndtccat	⊢ ( 𝜑 → 𝐶 ∈ Cat )

Proof

Step	Hyp	Ref	Expression
1		mndtccat.c	⊢ ( 𝜑 → 𝐶 = ( MndToCat ‘ 𝑀 ) )
2		mndtccat.m	⊢ ( 𝜑 → 𝑀 ∈ Mnd )
3	1 2	mndtccatid	⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 0g ‘ 𝑀 ) ) ) )
4	3	simpld	⊢ ( 𝜑 → 𝐶 ∈ Cat )