| Step | Hyp | Ref
| Expression |
| 1 | | df-subg 19141 |
. . 3
⊢ SubGrp =
(𝑤 ∈ Grp ↦
{𝑠 ∈ 𝒫
(Base‘𝑤) ∣
(𝑤 ↾s
𝑠) ∈
Grp}) |
| 2 | 1 | mptrcl 7025 |
. 2
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
| 3 | | simp1 1137 |
. 2
⊢ ((𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp) → 𝐺 ∈ Grp) |
| 4 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑤 = 𝐺 → (Base‘𝑤) = (Base‘𝐺)) |
| 5 | | issubg.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝐺) |
| 6 | 4, 5 | eqtr4di 2795 |
. . . . . . . . 9
⊢ (𝑤 = 𝐺 → (Base‘𝑤) = 𝐵) |
| 7 | 6 | pweqd 4617 |
. . . . . . . 8
⊢ (𝑤 = 𝐺 → 𝒫 (Base‘𝑤) = 𝒫 𝐵) |
| 8 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑤 = 𝐺 → (𝑤 ↾s 𝑠) = (𝐺 ↾s 𝑠)) |
| 9 | 8 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝑤 = 𝐺 → ((𝑤 ↾s 𝑠) ∈ Grp ↔ (𝐺 ↾s 𝑠) ∈ Grp)) |
| 10 | 7, 9 | rabeqbidv 3455 |
. . . . . . 7
⊢ (𝑤 = 𝐺 → {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ Grp} = {𝑠 ∈ 𝒫 𝐵 ∣ (𝐺 ↾s 𝑠) ∈ Grp}) |
| 11 | 5 | fvexi 6920 |
. . . . . . . . 9
⊢ 𝐵 ∈ V |
| 12 | 11 | pwex 5380 |
. . . . . . . 8
⊢ 𝒫
𝐵 ∈ V |
| 13 | 12 | rabex 5339 |
. . . . . . 7
⊢ {𝑠 ∈ 𝒫 𝐵 ∣ (𝐺 ↾s 𝑠) ∈ Grp} ∈ V |
| 14 | 10, 1, 13 | fvmpt 7016 |
. . . . . 6
⊢ (𝐺 ∈ Grp →
(SubGrp‘𝐺) = {𝑠 ∈ 𝒫 𝐵 ∣ (𝐺 ↾s 𝑠) ∈ Grp}) |
| 15 | 14 | eleq2d 2827 |
. . . . 5
⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ 𝑆 ∈ {𝑠 ∈ 𝒫 𝐵 ∣ (𝐺 ↾s 𝑠) ∈ Grp})) |
| 16 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑠 = 𝑆 → (𝐺 ↾s 𝑠) = (𝐺 ↾s 𝑆)) |
| 17 | 16 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑠 = 𝑆 → ((𝐺 ↾s 𝑠) ∈ Grp ↔ (𝐺 ↾s 𝑆) ∈ Grp)) |
| 18 | 17 | elrab 3692 |
. . . . . 6
⊢ (𝑆 ∈ {𝑠 ∈ 𝒫 𝐵 ∣ (𝐺 ↾s 𝑠) ∈ Grp} ↔ (𝑆 ∈ 𝒫 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp)) |
| 19 | 11 | elpw2 5334 |
. . . . . . 7
⊢ (𝑆 ∈ 𝒫 𝐵 ↔ 𝑆 ⊆ 𝐵) |
| 20 | 19 | anbi1i 624 |
. . . . . 6
⊢ ((𝑆 ∈ 𝒫 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp) ↔ (𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp)) |
| 21 | 18, 20 | bitri 275 |
. . . . 5
⊢ (𝑆 ∈ {𝑠 ∈ 𝒫 𝐵 ∣ (𝐺 ↾s 𝑠) ∈ Grp} ↔ (𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp)) |
| 22 | 15, 21 | bitrdi 287 |
. . . 4
⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp))) |
| 23 | | ibar 528 |
. . . 4
⊢ (𝐺 ∈ Grp → ((𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp) ↔ (𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp)))) |
| 24 | 22, 23 | bitrd 279 |
. . 3
⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp)))) |
| 25 | | 3anass 1095 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp) ↔ (𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp))) |
| 26 | 24, 25 | bitr4di 289 |
. 2
⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp))) |
| 27 | 2, 3, 26 | pm5.21nii 378 |
1
⊢ (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp)) |