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

Metamath Proof Explorer

Theorem mgmcl

Description: Closure of the operation of a magma. (Contributed by FL, 14-Sep-2010) (Revised by AV, 13-Jan-2020)

Ref Expression
Hypotheses mgmcl.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
mgmcl.o ⊢ ⚬ = ( +g ‘ 𝑀 )
Assertion mgmcl ( ( 𝑀 ∈ Mgm ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ⚬ 𝑌 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 mgmcl.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 mgmcl.o ⊢ ⚬ = ( +g ‘ 𝑀 )
3 1 2 ismgm ⊢ ( 𝑀 ∈ Mgm → ( 𝑀 ∈ Mgm ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ⚬ 𝑦 ) ∈ 𝐵 ) )
4 3 ibi ⊢ ( 𝑀 ∈ Mgm → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ⚬ 𝑦 ) ∈ 𝐵 )
5 ovrspc2v ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ⚬ 𝑦 ) ∈ 𝐵 ) → ( 𝑋 ⚬ 𝑌 ) ∈ 𝐵 )
6 5 expcom ⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ⚬ 𝑦 ) ∈ 𝐵 → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ⚬ 𝑌 ) ∈ 𝐵 ) )
7 4 6 syl ⊢ ( 𝑀 ∈ Mgm → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ⚬ 𝑌 ) ∈ 𝐵 ) )
8 7 3impib ⊢ ( ( 𝑀 ∈ Mgm ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ⚬ 𝑌 ) ∈ 𝐵 )