Metamath Proof Explorer

Theorem issubg

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

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

Proof

Step Hyp Ref Expression
1 issubg.b ⊢ B = Base G
2 df-subg ⊢ SubGrp = w ∈ Grp ⟼ s ∈ 𝒫 Base w | 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 → Base w = Base G
6 5 1 eqtr4di ⊢ w = G → Base w = B
7 6 pweqd ⊢ w = G → 𝒫 Base w = 𝒫 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 ∈ 𝒫 Base w | 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