Metamath Proof Explorer

Theorem issubg

Description: The subgroup predicate. (Contributed by Mario Carneiro, 2-Dec-2014)

Ref Expression
Hypothesis issubg.b ⊢B=BaseG
Assertion issubg ⊢S∈SubGrp⁡G↔G∈Grp∧S⊆B∧G↾𝑠S∈Grp

Proof

Step Hyp Ref Expression
1 issubg.b ⊢B=BaseG
2 df-subg ⊢SubGrp=w∈Grp⟼s∈𝒫Basew|w↾𝑠s∈Grp
3 2 mptrcl ⊢S∈SubGrp⁡G→G∈Grp
4 simp1 ⊢G∈Grp∧S⊆B∧G↾𝑠S∈Grp→G∈Grp
5 fveq2 ⊢w=G→Basew=BaseG
6 5 1 eqtr4di ⊢w=G→Basew=B
7 6 pweqd ⊢w=G→𝒫Basew=𝒫B
8 oveq1 ⊢w=G→w↾𝑠s=G↾𝑠s
9 8 eleq1d ⊢w=G→w↾𝑠s∈Grp↔G↾𝑠s∈Grp
10 7 9 rabeqbidv ⊢w=G→s∈𝒫Basew|w↾𝑠s∈Grp=s∈𝒫B|G↾𝑠s∈Grp
11 1 fvexi ⊢B∈V
12 11 pwex ⊢𝒫B∈V
13 12 rabex ⊢s∈𝒫B|G↾𝑠s∈Grp∈V
14 10 2 13 fvmpt ⊢G∈Grp→SubGrp⁡G=s∈𝒫B|G↾𝑠s∈Grp
15 14 eleq2d ⊢G∈Grp→S∈SubGrp⁡G↔S∈s∈𝒫B|G↾𝑠s∈Grp
16 oveq2 ⊢s=S→G↾𝑠s=G↾𝑠S
17 16 eleq1d ⊢s=S→G↾𝑠s∈Grp↔G↾𝑠S∈Grp
18 17 elrab ⊢S∈s∈𝒫B|G↾𝑠s∈Grp↔S∈𝒫B∧G↾𝑠S∈Grp
19 11 elpw2 ⊢S∈𝒫B↔S⊆B
20 19 anbi1i ⊢S∈𝒫B∧G↾𝑠S∈Grp↔S⊆B∧G↾𝑠S∈Grp
21 18 20 bitri ⊢S∈s∈𝒫B|G↾𝑠s∈Grp↔S⊆B∧G↾𝑠S∈Grp
22 15 21 bitrdi ⊢G∈Grp→S∈SubGrp⁡G↔S⊆B∧G↾𝑠S∈Grp
23 ibar ⊢G∈Grp→S⊆B∧G↾𝑠S∈Grp↔G∈Grp∧S⊆B∧G↾𝑠S∈Grp
24 22 23 bitrd ⊢G∈Grp→S∈SubGrp⁡G↔G∈Grp∧S⊆B∧G↾𝑠S∈Grp
25 3anass ⊢G∈Grp∧S⊆B∧G↾𝑠S∈Grp↔G∈Grp∧S⊆B∧G↾𝑠S∈Grp
26 24 25 bitr4di ⊢G∈Grp→S∈SubGrp⁡G↔G∈Grp∧S⊆B∧G↾𝑠S∈Grp
27 3 4 26 pm5.21nii ⊢S∈SubGrp⁡G↔G∈Grp∧S⊆B∧G↾𝑠S∈Grp