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	mndtcbaseu.c	⊢ ( 𝜑 → 𝐶 = ( MndToCat ‘ 𝑀 ) )
	mndtcbaseu.m	⊢ ( 𝜑 → 𝑀 ∈ Mnd )
	mndtcbaseu.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
Assertion	mndtcbasval	⊢ ( 𝜑 → 𝐵 = { 𝑀 } )

Proof

Step	Hyp	Ref	Expression
1		mndtcbaseu.c	⊢ ( 𝜑 → 𝐶 = ( MndToCat ‘ 𝑀 ) )
2		mndtcbaseu.m	⊢ ( 𝜑 → 𝑀 ∈ Mnd )
3		mndtcbaseu.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	⊢ ( 𝜑 → 𝐵 = { 𝑀 } )