# Metamath Proof Explorer

## Theorem mndvass

Description: Tuple-wise associativity in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Hypotheses mndvcl.b ${⊢}{B}={\mathrm{Base}}_{{M}}$
mndvcl.p
Assertion mndvass

### Proof

Step Hyp Ref Expression
1 mndvcl.b ${⊢}{B}={\mathrm{Base}}_{{M}}$
2 mndvcl.p
3 elmapex ${⊢}{X}\in \left({{B}}^{{I}}\right)\to \left({B}\in \mathrm{V}\wedge {I}\in \mathrm{V}\right)$
4 3 simprd ${⊢}{X}\in \left({{B}}^{{I}}\right)\to {I}\in \mathrm{V}$
5 4 3ad2ant1 ${⊢}\left({X}\in \left({{B}}^{{I}}\right)\wedge {Y}\in \left({{B}}^{{I}}\right)\wedge {Z}\in \left({{B}}^{{I}}\right)\right)\to {I}\in \mathrm{V}$
6 5 adantl ${⊢}\left({M}\in \mathrm{Mnd}\wedge \left({X}\in \left({{B}}^{{I}}\right)\wedge {Y}\in \left({{B}}^{{I}}\right)\wedge {Z}\in \left({{B}}^{{I}}\right)\right)\right)\to {I}\in \mathrm{V}$
7 elmapi ${⊢}{X}\in \left({{B}}^{{I}}\right)\to {X}:{I}⟶{B}$
8 7 3ad2ant1 ${⊢}\left({X}\in \left({{B}}^{{I}}\right)\wedge {Y}\in \left({{B}}^{{I}}\right)\wedge {Z}\in \left({{B}}^{{I}}\right)\right)\to {X}:{I}⟶{B}$
9 8 adantl ${⊢}\left({M}\in \mathrm{Mnd}\wedge \left({X}\in \left({{B}}^{{I}}\right)\wedge {Y}\in \left({{B}}^{{I}}\right)\wedge {Z}\in \left({{B}}^{{I}}\right)\right)\right)\to {X}:{I}⟶{B}$
10 elmapi ${⊢}{Y}\in \left({{B}}^{{I}}\right)\to {Y}:{I}⟶{B}$
11 10 3ad2ant2 ${⊢}\left({X}\in \left({{B}}^{{I}}\right)\wedge {Y}\in \left({{B}}^{{I}}\right)\wedge {Z}\in \left({{B}}^{{I}}\right)\right)\to {Y}:{I}⟶{B}$
12 11 adantl ${⊢}\left({M}\in \mathrm{Mnd}\wedge \left({X}\in \left({{B}}^{{I}}\right)\wedge {Y}\in \left({{B}}^{{I}}\right)\wedge {Z}\in \left({{B}}^{{I}}\right)\right)\right)\to {Y}:{I}⟶{B}$
13 elmapi ${⊢}{Z}\in \left({{B}}^{{I}}\right)\to {Z}:{I}⟶{B}$
14 13 3ad2ant3 ${⊢}\left({X}\in \left({{B}}^{{I}}\right)\wedge {Y}\in \left({{B}}^{{I}}\right)\wedge {Z}\in \left({{B}}^{{I}}\right)\right)\to {Z}:{I}⟶{B}$
15 14 adantl ${⊢}\left({M}\in \mathrm{Mnd}\wedge \left({X}\in \left({{B}}^{{I}}\right)\wedge {Y}\in \left({{B}}^{{I}}\right)\wedge {Z}\in \left({{B}}^{{I}}\right)\right)\right)\to {Z}:{I}⟶{B}$
16 1 2 mndass