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 = Base M
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 = Base M
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 ∈ B C ∈ B
6 5 adantr ⊢ φ ∧ a ∈ B ∧ b ∈ B → ∀ x ∈ B ∀ y ∈ B C ∈ 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 ∈ B C ∈ B ∧ a ∈ B ∧ b ∈ B → a x ∈ B , y ∈ B ⟼ C b ∈ B
11 6 7 8 10 syl3anc ⊢ φ ∧ a ∈ B ∧ b ∈ B → a x ∈ B , y ∈ B ⟼ C b ∈ B
12 11 ralrimivva ⊢ φ → ∀ a ∈ B ∀ b ∈ B a x ∈ B , y ∈ B ⟼ C b ∈ B
13 n0 ⊢ B ≠ ∅ ↔ ∃ e e ∈ B
14 2 eqcomi ⊢ x ∈ B , y ∈ B ⟼ C = + M
15 1 14 ismgmn0 ⊢ e ∈ B → M ∈ Mgm ↔ ∀ a ∈ B ∀ b ∈ B a x ∈ B , y ∈ B ⟼ C b ∈ B
16 15 exlimiv ⊢ ∃ e e ∈ B → M ∈ Mgm ↔ ∀ a ∈ B ∀ b ∈ B a x ∈ B , y ∈ B ⟼ C b ∈ B
17 13 16 sylbi ⊢ B ≠ ∅ → M ∈ Mgm ↔ ∀ a ∈ B ∀ b ∈ B a x ∈ B , y ∈ B ⟼ C b ∈ B
18 3 17 syl ⊢ φ → M ∈ Mgm ↔ ∀ a ∈ B ∀ b ∈ B a x ∈ B , y ∈ B ⟼ C b ∈ B
19 12 18 mpbird ⊢ φ → M ∈ Mgm