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	$$⊢\phi \to C=\mathrm{MndToCat}\left(M\right)$$
	mndtcbaseu.m	$$⊢\phi \to M\in \mathrm{Mnd}$$
	mndtcbaseu.b	$$⊢\phi \to B={\mathrm{Base}}_C$$
Assertion	mndtcbasval	$$⊢\phi \to B=\left\{M\right\}$$

Proof

Step	Hyp	Ref	Expression
1		mndtcbaseu.c	$$⊢\phi \to C=\mathrm{MndToCat}\left(M\right)$$
2		mndtcbaseu.m	$$⊢\phi \to M\in \mathrm{Mnd}$$
3		mndtcbaseu.b	$$⊢\phi \to B={\mathrm{Base}}_C$$
4	1 2	mndtcval	$$⊢\phi \to C=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{M\right\}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left\{⟨M,M,{\mathrm{Base}}_M⟩\right\}⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left\{⟨⟨M,M,M⟩,{+}_M⟩\right\}⟩\right\}$$
5	4	fveq2d	$$⊢\phi \to {\mathrm{Base}}_C={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{M\right\}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left\{⟨M,M,{\mathrm{Base}}_M⟩\right\}⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left\{⟨⟨M,M,M⟩,{+}_M⟩\right\}⟩\right\}}$$
6		snex	$$⊢\left\{M\right\}\in \mathrm{V}$$
7		catstr	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{M\right\}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left\{⟨M,M,{\mathrm{Base}}_M⟩\right\}⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left\{⟨⟨M,M,M⟩,{+}_M⟩\right\}⟩\right\}\mathrm{Struct}⟨1,15⟩$$
8		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
9		snsstp1	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{M\right\}⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{M\right\}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left\{⟨M,M,{\mathrm{Base}}_M⟩\right\}⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left\{⟨⟨M,M,M⟩,{+}_M⟩\right\}⟩\right\}$$
10	7 8 9	strfv	$$⊢\left\{M\right\}\in \mathrm{V}\to \left\{M\right\}={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{M\right\}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left\{⟨M,M,{\mathrm{Base}}_M⟩\right\}⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left\{⟨⟨M,M,M⟩,{+}_M⟩\right\}⟩\right\}}$$
11	6 10	mp1i	$$⊢\phi \to \left\{M\right\}={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{M\right\}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left\{⟨M,M,{\mathrm{Base}}_M⟩\right\}⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left\{⟨⟨M,M,M⟩,{+}_M⟩\right\}⟩\right\}}$$
12	5 3 11	3eqtr4d	$$⊢\phi \to B=\left\{M\right\}$$