Theorem submgmacs

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

	Ref	Expression
Hypothesis	submgmacs.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion	submgmacs	⊢ ( 𝐺 ∈ Mgm → ( SubMgm ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		submgmacs.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
3	1 2	issubmgm	⊢ ( 𝐺 ∈ Mgm → ( 𝑠 ∈ ( SubMgm ‘ 𝐺 ) ↔ ( 𝑠 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑠 ) ) )
4		velpw	⊢ ( 𝑠 ∈ 𝒫 𝐵 ↔ 𝑠 ⊆ 𝐵 )
5	4	anbi1i	⊢ ( ( 𝑠 ∈ 𝒫 𝐵 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑠 ) ↔ ( 𝑠 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑠 ) )
6	3 5	bitr4di	⊢ ( 𝐺 ∈ Mgm → ( 𝑠 ∈ ( SubMgm ‘ 𝐺 ) ↔ ( 𝑠 ∈ 𝒫 𝐵 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑠 ) ) )
7	6	eqabdv	⊢ ( 𝐺 ∈ Mgm → ( SubMgm ‘ 𝐺 ) = { 𝑠 ∣ ( 𝑠 ∈ 𝒫 𝐵 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑠 ) } )
8		df-rab	⊢ { 𝑠 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑠 } = { 𝑠 ∣ ( 𝑠 ∈ 𝒫 𝐵 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑠 ) }
9	7 8	eqtr4di	⊢ ( 𝐺 ∈ Mgm → ( SubMgm ‘ 𝐺 ) = { 𝑠 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑠 } )
10	1	fvexi	⊢ 𝐵 ∈ V
11	1 2	mgmcl	⊢ ( ( 𝐺 ∈ Mgm ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐵 )
12	11	3expb	⊢ ( ( 𝐺 ∈ Mgm ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐵 )
13	12	ralrimivva	⊢ ( 𝐺 ∈ Mgm → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐵 )
14		acsfn2	⊢ ( ( 𝐵 ∈ V ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐵 ) → { 𝑠 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑠 } ∈ ( ACS ‘ 𝐵 ) )
15	10 13 14	sylancr	⊢ ( 𝐺 ∈ Mgm → { 𝑠 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑠 } ∈ ( ACS ‘ 𝐵 ) )
16	9 15	eqeltrd	⊢ ( 𝐺 ∈ Mgm → ( SubMgm ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) )