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 ⊢ φ → C = MndToCat ⁡ M
mndtcbas.m ⊢ φ → M ∈ Mnd
mndtcbas.b ⊢ φ → B = Base C
Assertion mndtcbasval ⊢ φ → B = M

Proof

Step Hyp Ref Expression
1 mndtcbas.c ⊢ φ → C = MndToCat ⁡ M
2 mndtcbas.m ⊢ φ → M ∈ Mnd
3 mndtcbas.b ⊢ φ → B = Base C
4 1 2 mndtcval ⊢ φ → C = Base ndx M Hom ⁡ ndx M M Base M comp ⁡ ndx M M M + M
5 4 fveq2d ⊢ φ → Base C = Base Base ndx M Hom ⁡ ndx M M Base M comp ⁡ ndx M M M + M
6 snex ⊢ M ∈ V
7 catstr ⊢ Base ndx M Hom ⁡ ndx M M Base M comp ⁡ ndx M M M + M Struct 1 15
8 baseid ⊢ Base = Slot Base ndx
9 snsstp1 ⊢ Base ndx M ⊆ Base ndx M Hom ⁡ ndx M M Base M comp ⁡ ndx M M M + M
10 7 8 9 strfv ⊢ M ∈ V → M = Base Base ndx M Hom ⁡ ndx M M Base M comp ⁡ ndx M M M + M
11 6 10 mp1i ⊢ φ → M = Base Base ndx M Hom ⁡ ndx M M Base M comp ⁡ ndx M M M + M
12 5 3 11 3eqtr4d ⊢ φ → B = M