Step | Hyp | Ref
| Expression |
1 | | df-subg 17591 |
. . . 4
⊢ SubGrp =
(𝑤 ∈ Grp ↦
{𝑠 ∈ 𝒫
(Base‘𝑤) ∣
(𝑤 ↾s
𝑠) ∈
Grp}) |
2 | 1 | dmmptss 5631 |
. . 3
⊢ dom
SubGrp ⊆ Grp |
3 | | elfvdm 6220 |
. . 3
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ dom SubGrp) |
4 | 2, 3 | sseldi 3601 |
. 2
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
5 | | simp1 1061 |
. 2
⊢ ((𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp) → 𝐺 ∈ Grp) |
6 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑤 = 𝐺 → (Base‘𝑤) = (Base‘𝐺)) |
7 | | issubg.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝐺) |
8 | 6, 7 | syl6eqr 2674 |
. . . . . . . . 9
⊢ (𝑤 = 𝐺 → (Base‘𝑤) = 𝐵) |
9 | 8 | pweqd 4163 |
. . . . . . . 8
⊢ (𝑤 = 𝐺 → 𝒫 (Base‘𝑤) = 𝒫 𝐵) |
10 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝑤 = 𝐺 → (𝑤 ↾s 𝑠) = (𝐺 ↾s 𝑠)) |
11 | 10 | eleq1d 2686 |
. . . . . . . 8
⊢ (𝑤 = 𝐺 → ((𝑤 ↾s 𝑠) ∈ Grp ↔ (𝐺 ↾s 𝑠) ∈ Grp)) |
12 | 9, 11 | rabeqbidv 3195 |
. . . . . . 7
⊢ (𝑤 = 𝐺 → {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ Grp} = {𝑠 ∈ 𝒫 𝐵 ∣ (𝐺 ↾s 𝑠) ∈ Grp}) |
13 | | fvex 6201 |
. . . . . . . . . 10
⊢
(Base‘𝐺)
∈ V |
14 | 7, 13 | eqeltri 2697 |
. . . . . . . . 9
⊢ 𝐵 ∈ V |
15 | 14 | pwex 4848 |
. . . . . . . 8
⊢ 𝒫
𝐵 ∈ V |
16 | 15 | rabex 4813 |
. . . . . . 7
⊢ {𝑠 ∈ 𝒫 𝐵 ∣ (𝐺 ↾s 𝑠) ∈ Grp} ∈ V |
17 | 12, 1, 16 | fvmpt 6282 |
. . . . . 6
⊢ (𝐺 ∈ Grp →
(SubGrp‘𝐺) = {𝑠 ∈ 𝒫 𝐵 ∣ (𝐺 ↾s 𝑠) ∈ Grp}) |
18 | 17 | eleq2d 2687 |
. . . . 5
⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ 𝑆 ∈ {𝑠 ∈ 𝒫 𝐵 ∣ (𝐺 ↾s 𝑠) ∈ Grp})) |
19 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑠 = 𝑆 → (𝐺 ↾s 𝑠) = (𝐺 ↾s 𝑆)) |
20 | 19 | eleq1d 2686 |
. . . . . . 7
⊢ (𝑠 = 𝑆 → ((𝐺 ↾s 𝑠) ∈ Grp ↔ (𝐺 ↾s 𝑆) ∈ Grp)) |
21 | 20 | elrab 3363 |
. . . . . 6
⊢ (𝑆 ∈ {𝑠 ∈ 𝒫 𝐵 ∣ (𝐺 ↾s 𝑠) ∈ Grp} ↔ (𝑆 ∈ 𝒫 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp)) |
22 | 14 | elpw2 4828 |
. . . . . . 7
⊢ (𝑆 ∈ 𝒫 𝐵 ↔ 𝑆 ⊆ 𝐵) |
23 | 22 | anbi1i 731 |
. . . . . 6
⊢ ((𝑆 ∈ 𝒫 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp) ↔ (𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp)) |
24 | 21, 23 | bitri 264 |
. . . . 5
⊢ (𝑆 ∈ {𝑠 ∈ 𝒫 𝐵 ∣ (𝐺 ↾s 𝑠) ∈ Grp} ↔ (𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp)) |
25 | 18, 24 | syl6bb 276 |
. . . 4
⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp))) |
26 | | ibar 525 |
. . . 4
⊢ (𝐺 ∈ Grp → ((𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp) ↔ (𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp)))) |
27 | 25, 26 | bitrd 268 |
. . 3
⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp)))) |
28 | | 3anass 1042 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp) ↔ (𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp))) |
29 | 27, 28 | syl6bbr 278 |
. 2
⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp))) |
30 | 4, 5, 29 | pm5.21nii 368 |
1
⊢ (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp)) |