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 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ⚬ 𝑌 ) ∈ 𝐵 )