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	⊢ 𝐵 = ( Base ‘ 𝑀 )
	opmpoismgm.p	⊢ ( +g ‘ 𝑀 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
	opmpoismgm.n	⊢ ( 𝜑 → 𝐵 ≠ ∅ )
	opmpoismgm.c	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐶 ∈ 𝐵 )
Assertion	opmpoismgm	⊢ ( 𝜑 → 𝑀 ∈ Mgm )

Proof

Step	Hyp	Ref	Expression
1		opmpoismgm.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		opmpoismgm.p	⊢ ( +g ‘ 𝑀 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
3		opmpoismgm.n	⊢ ( 𝜑 → 𝐵 ≠ ∅ )
4		opmpoismgm.c	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐶 ∈ 𝐵 )
5	4	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐵 )
6	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐵 )
7		simprl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑎 ∈ 𝐵 )
8		simprr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑏 ∈ 𝐵 )
9		eqid	⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
10	9	ovmpoelrn	⊢ ( ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑏 ) ∈ 𝐵 )
11	6 7 8 10	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑏 ) ∈ 𝐵 )
12	11	ralrimivva	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑏 ) ∈ 𝐵 )
13		n0	⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑒 𝑒 ∈ 𝐵 )
14	2	eqcomi	⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( +g ‘ 𝑀 )
15	1 14	ismgmn0	⊢ ( 𝑒 ∈ 𝐵 → ( 𝑀 ∈ Mgm ↔ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑏 ) ∈ 𝐵 ) )
16	15	exlimiv	⊢ ( ∃ 𝑒 𝑒 ∈ 𝐵 → ( 𝑀 ∈ Mgm ↔ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑏 ) ∈ 𝐵 ) )
17	13 16	sylbi	⊢ ( 𝐵 ≠ ∅ → ( 𝑀 ∈ Mgm ↔ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑏 ) ∈ 𝐵 ) )
18	3 17	syl	⊢ ( 𝜑 → ( 𝑀 ∈ Mgm ↔ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑏 ) ∈ 𝐵 ) )
19	12 18	mpbird	⊢ ( 𝜑 → 𝑀 ∈ Mgm )