This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mgm0

Description: Any set with an empty base set and any group operation is a magma. (Contributed by AV, 28-Aug-2021)

Ref Expression
Assertion mgm0 ⊢ M ∈ V ∧ Base M = ∅ → M ∈ Mgm

Proof

Step Hyp Ref Expression
1 rzal ⊢ Base M = ∅ → ∀ x ∈ Base M ∀ y ∈ Base M x + M y ∈ Base M
2 1 adantl ⊢ M ∈ V ∧ Base M = ∅ → ∀ x ∈ Base M ∀ y ∈ Base M x + M y ∈ Base M
3 eqid ⊢ Base M = Base M
4 eqid ⊢ + M = + M
5 3 4 ismgm ⊢ M ∈ V → M ∈ Mgm ↔ ∀ x ∈ Base M ∀ y ∈ Base M x + M y ∈ Base M
6 5 adantr ⊢ M ∈ V ∧ Base M = ∅ → M ∈ Mgm ↔ ∀ x ∈ Base M ∀ y ∈ Base M x + M y ∈ Base M
7 2 6 mpbird ⊢ M ∈ V ∧ Base M = ∅ → M ∈ Mgm