Theorem subgacs

Description: Subgroups are an algebraic closure system. (Contributed by Stefan O'Rear, 4-Apr-2015) (Revised by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Hypothesis	subgacs.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion	subgacs	⊢ ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		subgacs.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		eqid	⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
3	2	issubg3	⊢ ( 𝐺 ∈ Grp → ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑠 ∈ ( SubMnd ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑠 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑠 ) ) )
4	1	submss	⊢ ( 𝑠 ∈ ( SubMnd ‘ 𝐺 ) → 𝑠 ⊆ 𝐵 )
5	4	adantl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑠 ∈ ( SubMnd ‘ 𝐺 ) ) → 𝑠 ⊆ 𝐵 )
6		velpw	⊢ ( 𝑠 ∈ 𝒫 𝐵 ↔ 𝑠 ⊆ 𝐵 )
7	5 6	sylibr	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑠 ∈ ( SubMnd ‘ 𝐺 ) ) → 𝑠 ∈ 𝒫 𝐵 )
8		eleq2w	⊢ ( 𝑦 = 𝑠 → ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑦 ↔ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑠 ) )
9	8	raleqbi1dv	⊢ ( 𝑦 = 𝑠 → ( ∀ 𝑥 ∈ 𝑦 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑦 ↔ ∀ 𝑥 ∈ 𝑠 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑠 ) )
10	9	elrab3	⊢ ( 𝑠 ∈ 𝒫 𝐵 → ( 𝑠 ∈ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑦 } ↔ ∀ 𝑥 ∈ 𝑠 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑠 ) )
11	7 10	syl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑠 ∈ ( SubMnd ‘ 𝐺 ) ) → ( 𝑠 ∈ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑦 } ↔ ∀ 𝑥 ∈ 𝑠 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑠 ) )
12	11	pm5.32da	⊢ ( 𝐺 ∈ Grp → ( ( 𝑠 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑠 ∈ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑦 } ) ↔ ( 𝑠 ∈ ( SubMnd ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑠 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑠 ) ) )
13	3 12	bitr4d	⊢ ( 𝐺 ∈ Grp → ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑠 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑠 ∈ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑦 } ) ) )
14		elin	⊢ ( 𝑠 ∈ ( ( SubMnd ‘ 𝐺 ) ∩ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑦 } ) ↔ ( 𝑠 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑠 ∈ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑦 } ) )
15	13 14	bitr4di	⊢ ( 𝐺 ∈ Grp → ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ↔ 𝑠 ∈ ( ( SubMnd ‘ 𝐺 ) ∩ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑦 } ) ) )
16	15	eqrdv	⊢ ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) = ( ( SubMnd ‘ 𝐺 ) ∩ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑦 } ) )
17	1	fvexi	⊢ 𝐵 ∈ V
18		mreacs	⊢ ( 𝐵 ∈ V → ( ACS ‘ 𝐵 ) ∈ ( Moore ‘ 𝒫 𝐵 ) )
19	17 18	mp1i	⊢ ( 𝐺 ∈ Grp → ( ACS ‘ 𝐵 ) ∈ ( Moore ‘ 𝒫 𝐵 ) )
20		grpmnd	⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
21	1	submacs	⊢ ( 𝐺 ∈ Mnd → ( SubMnd ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) )
22	20 21	syl	⊢ ( 𝐺 ∈ Grp → ( SubMnd ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) )
23	1 2	grpinvcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐵 )
24	23	ralrimiva	⊢ ( 𝐺 ∈ Grp → ∀ 𝑥 ∈ 𝐵 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐵 )
25		acsfn1	⊢ ( ( 𝐵 ∈ V ∧ ∀ 𝑥 ∈ 𝐵 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐵 ) → { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑦 } ∈ ( ACS ‘ 𝐵 ) )
26	17 24 25	sylancr	⊢ ( 𝐺 ∈ Grp → { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑦 } ∈ ( ACS ‘ 𝐵 ) )
27		mreincl	⊢ ( ( ( ACS ‘ 𝐵 ) ∈ ( Moore ‘ 𝒫 𝐵 ) ∧ ( SubMnd ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) ∧ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑦 } ∈ ( ACS ‘ 𝐵 ) ) → ( ( SubMnd ‘ 𝐺 ) ∩ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑦 } ) ∈ ( ACS ‘ 𝐵 ) )
28	19 22 26 27	syl3anc	⊢ ( 𝐺 ∈ Grp → ( ( SubMnd ‘ 𝐺 ) ∩ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑦 } ) ∈ ( ACS ‘ 𝐵 ) )
29	16 28	eqeltrd	⊢ ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) )