This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )