Theorem submgmid

Description: Every magma is trivially a submagma of itself. (Contributed by AV, 26-Feb-2020)

	Ref	Expression
Hypothesis	submgmss.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
Assertion	submgmid	⊢ ( 𝑀 ∈ Mgm → 𝐵 ∈ ( SubMgm ‘ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		submgmss.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		ssidd	⊢ ( 𝑀 ∈ Mgm → 𝐵 ⊆ 𝐵 )
3	1	ressid	⊢ ( 𝑀 ∈ Mgm → ( 𝑀 ↾s 𝐵 ) = 𝑀 )
4		id	⊢ ( 𝑀 ∈ Mgm → 𝑀 ∈ Mgm )
5	3 4	eqeltrd	⊢ ( 𝑀 ∈ Mgm → ( 𝑀 ↾s 𝐵 ) ∈ Mgm )
6		eqid	⊢ ( 𝑀 ↾s 𝐵 ) = ( 𝑀 ↾s 𝐵 )
7	1 6	issubmgm2	⊢ ( 𝑀 ∈ Mgm → ( 𝐵 ∈ ( SubMgm ‘ 𝑀 ) ↔ ( 𝐵 ⊆ 𝐵 ∧ ( 𝑀 ↾s 𝐵 ) ∈ Mgm ) ) )
8	2 5 7	mpbir2and	⊢ ( 𝑀 ∈ Mgm → 𝐵 ∈ ( SubMgm ‘ 𝑀 ) )