Metamath Proof Explorer

Theorem opmpoismgm

Description: A structure with a group addition operation in maps-to notation is a magma if the operation value is contained in the base set. (Contributed by AV, 16-Feb-2020)

Ref Expression
Hypotheses opmpoismgm.b ⊢B=BaseM
opmpoismgm.p ⊢+M=x∈B,y∈B⟼C
opmpoismgm.n ⊢φ→B≠∅
opmpoismgm.c ⊢φ∧x∈B∧y∈B→C∈B
Assertion opmpoismgm ⊢φ→M∈Mgm

Proof

Step Hyp Ref Expression
1 opmpoismgm.b ⊢B=BaseM
2 opmpoismgm.p ⊢+M=x∈B,y∈B⟼C
3 opmpoismgm.n ⊢φ→B≠∅
4 opmpoismgm.c ⊢φ∧x∈B∧y∈B→C∈B
5 4 ralrimivva ⊢φ→∀x∈B∀y∈BC∈B
6 5 adantr ⊢φ∧a∈B∧b∈B→∀x∈B∀y∈BC∈B
7 simprl ⊢φ∧a∈B∧b∈B→a∈B
8 simprr ⊢φ∧a∈B∧b∈B→b∈B
9 eqid ⊢x∈B,y∈B⟼C=x∈B,y∈B⟼C
10 9 ovmpoelrn ⊢∀x∈B∀y∈BC∈B∧a∈B∧b∈B→ax∈B,y∈B⟼Cb∈B
11 6 7 8 10 syl3anc ⊢φ∧a∈B∧b∈B→ax∈B,y∈B⟼Cb∈B
12 11 ralrimivva ⊢φ→∀a∈B∀b∈Bax∈B,y∈B⟼Cb∈B
13 n0 ⊢B≠∅↔∃ee∈B
14 2 eqcomi ⊢x∈B,y∈B⟼C=+M
15 1 14 ismgmn0 ⊢e∈B→M∈Mgm↔∀a∈B∀b∈Bax∈B,y∈B⟼Cb∈B
16 15 exlimiv ⊢∃ee∈B→M∈Mgm↔∀a∈B∀b∈Bax∈B,y∈B⟼Cb∈B
17 13 16 sylbi ⊢B≠∅→M∈Mgm↔∀a∈B∀b∈Bax∈B,y∈B⟼Cb∈B
18 3 17 syl ⊢φ→M∈Mgm↔∀a∈B∀b∈Bax∈B,y∈B⟼Cb∈B
19 12 18 mpbird ⊢φ→M∈Mgm