Metamath Proof Explorer

Theorem submgmacs

Description: Submagmas are an algebraic closure system. (Contributed by AV, 27-Feb-2020)

		Ref	Expression
	Hypothesis	submgmacs.b	$⊢ B = {Base}_{G}$
	Assertion	submgmacs	$⊢ G \in Mgm \to SubMgm (G) \in ACS (B)$

Proof

Step	Hyp	Ref	Expression
1		submgmacs.b	$⊢ B = {Base}_{G}$
2		eqid	$⊢ +_{G} = +_{G}$
3	1 2	issubmgm	$⊢ G \in Mgm \to (s \in SubMgm (G) \leftrightarrow (s \subseteq B \land \forall x \in s \forall y \in s x +_{G} y \in s))$
4		velpw	$⊢ s \in 𝒫 B \leftrightarrow s \subseteq B$
5	4	anbi1i	$⊢ (s \in 𝒫 B \land \forall x \in s \forall y \in s x +_{G} y \in s) \leftrightarrow (s \subseteq B \land \forall x \in s \forall y \in s x +_{G} y \in s)$
6	3 5	bitr4di	$⊢ G \in Mgm \to (s \in SubMgm (G) \leftrightarrow (s \in 𝒫 B \land \forall x \in s \forall y \in s x +_{G} y \in s))$
7	6	abbi2dv	$⊢ G \in Mgm \to SubMgm (G) = \{s \| (s \in 𝒫 B \land \forall x \in s \forall y \in s x +_{G} y \in s)\}$
8		df-rab	$⊢ \{s \in 𝒫 B \| \forall x \in s \forall y \in s x +_{G} y \in s\} = \{s \| (s \in 𝒫 B \land \forall x \in s \forall y \in s x +_{G} y \in s)\}$
9	7 8	eqtr4di	$⊢ G \in Mgm \to SubMgm (G) = \{s \in 𝒫 B \| \forall x \in s \forall y \in s x +_{G} y \in s\}$
10	1	fvexi	$⊢ B \in V$
11	1 2	mgmcl	$⊢ (G \in Mgm \land x \in B \land y \in B) \to x +_{G} y \in B$
12	11	3expb	$⊢ (G \in Mgm \land (x \in B \land y \in B)) \to x +_{G} y \in B$
13	12	ralrimivva	$⊢ G \in Mgm \to \forall x \in B \forall y \in B x +_{G} y \in B$
14		acsfn2	$⊢ (B \in V \land \forall x \in B \forall y \in B x +_{G} y \in B) \to \{s \in 𝒫 B \| \forall x \in s \forall y \in s x +_{G} y \in s\} \in ACS (B)$
15	10 13 14	sylancr	$⊢ G \in Mgm \to \{s \in 𝒫 B \| \forall x \in s \forall y \in s x +_{G} y \in s\} \in ACS (B)$
16	9 15	eqeltrd	$⊢ G \in Mgm \to SubMgm (G) \in ACS (B)$