# Metamath Proof Explorer

## Theorem mndvcl

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

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

### Proof

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