submgmid

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

		Ref	Expression
	Hypothesis	submgmss.b	$⊢ B = {Base}_{M}$
	Assertion	submgmid	$⊢ M \in Mgm \to B \in SubMgm (M)$

Step	Hyp	Ref	Expression
1		submgmss.b	$⊢ B = {Base}_{M}$
2		ssidd	$⊢ M \in Mgm \to B \subseteq B$
3	1	ressid	$⊢ M \in Mgm \to M ↾_{𝑠} B = M$
4		id	$⊢ M \in Mgm \to M \in Mgm$
5	3 4	eqeltrd	$⊢ M \in Mgm \to M ↾_{𝑠} B \in Mgm$
6		eqid	$⊢ M ↾_{𝑠} B = M ↾_{𝑠} B$
7	1 6	issubmgm2	$⊢ M \in Mgm \to (B \in SubMgm (M) \leftrightarrow (B \subseteq B \land M ↾_{𝑠} B \in Mgm))$
8	2 5 7	mpbir2and	$⊢ M \in Mgm \to B \in SubMgm (M)$

Metamath Proof Explorer