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

Metamath Proof Explorer

Theorem mndtcbasval

Description: The base set of the category built from a monoid. (Contributed by Zhi Wang, 22-Sep-2024) (New usage is discouraged.)

Ref Expression
Hypotheses mndtcbas.c ⊢ ( 𝜑 → 𝐶 = ( MndToCat ‘ 𝑀 ) )
mndtcbas.m ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
mndtcbas.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
Assertion mndtcbasval ( 𝜑 → 𝐵 = { 𝑀 } )

Proof

Step Hyp Ref Expression
1 mndtcbas.c ⊢ ( 𝜑 → 𝐶 = ( MndToCat ‘ 𝑀 ) )
2 mndtcbas.m ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
3 mndtcbas.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
4 1 2 mndtcval ⊢ ( 𝜑 → 𝐶 = { ⟨ ( Base ‘ ndx ) , { 𝑀 } ⟩ , ⟨ ( Hom ‘ ndx ) , { ⟨ 𝑀 , 𝑀 , ( Base ‘ 𝑀 ) ⟩ } ⟩ , ⟨ ( comp ‘ ndx ) , { ⟨ ⟨ 𝑀 , 𝑀 , 𝑀 ⟩ , ( +g ‘ 𝑀 ) ⟩ } ⟩ } )
5 4 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( Base ‘ { ⟨ ( Base ‘ ndx ) , { 𝑀 } ⟩ , ⟨ ( Hom ‘ ndx ) , { ⟨ 𝑀 , 𝑀 , ( Base ‘ 𝑀 ) ⟩ } ⟩ , ⟨ ( comp ‘ ndx ) , { ⟨ ⟨ 𝑀 , 𝑀 , 𝑀 ⟩ , ( +g ‘ 𝑀 ) ⟩ } ⟩ } ) )
6 snex ⊢ { 𝑀 } ∈ V
7 catstr ⊢ { ⟨ ( Base ‘ ndx ) , { 𝑀 } ⟩ , ⟨ ( Hom ‘ ndx ) , { ⟨ 𝑀 , 𝑀 , ( Base ‘ 𝑀 ) ⟩ } ⟩ , ⟨ ( comp ‘ ndx ) , { ⟨ ⟨ 𝑀 , 𝑀 , 𝑀 ⟩ , ( +g ‘ 𝑀 ) ⟩ } ⟩ } Struct ⟨ 1 , 1 5 ⟩
8 baseid ⊢ Base = Slot ( Base ‘ ndx )
9 snsstp1 ⊢ { ⟨ ( Base ‘ ndx ) , { 𝑀 } ⟩ } ⊆ { ⟨ ( Base ‘ ndx ) , { 𝑀 } ⟩ , ⟨ ( Hom ‘ ndx ) , { ⟨ 𝑀 , 𝑀 , ( Base ‘ 𝑀 ) ⟩ } ⟩ , ⟨ ( comp ‘ ndx ) , { ⟨ ⟨ 𝑀 , 𝑀 , 𝑀 ⟩ , ( +g ‘ 𝑀 ) ⟩ } ⟩ }
10 7 8 9 strfv ⊢ ( { 𝑀 } ∈ V → { 𝑀 } = ( Base ‘ { ⟨ ( Base ‘ ndx ) , { 𝑀 } ⟩ , ⟨ ( Hom ‘ ndx ) , { ⟨ 𝑀 , 𝑀 , ( Base ‘ 𝑀 ) ⟩ } ⟩ , ⟨ ( comp ‘ ndx ) , { ⟨ ⟨ 𝑀 , 𝑀 , 𝑀 ⟩ , ( +g ‘ 𝑀 ) ⟩ } ⟩ } ) )
11 6 10 mp1i ⊢ ( 𝜑 → { 𝑀 } = ( Base ‘ { ⟨ ( Base ‘ ndx ) , { 𝑀 } ⟩ , ⟨ ( Hom ‘ ndx ) , { ⟨ 𝑀 , 𝑀 , ( Base ‘ 𝑀 ) ⟩ } ⟩ , ⟨ ( comp ‘ ndx ) , { ⟨ ⟨ 𝑀 , 𝑀 , 𝑀 ⟩ , ( +g ‘ 𝑀 ) ⟩ } ⟩ } ) )
12 5 3 11 3eqtr4d ⊢ ( 𝜑 → 𝐵 = { 𝑀 } )