Metamath Proof Explorer

Theorem pgrpsubgsymgbi

Description: Every permutation group is a subgroup of the corresponding symmetric group. (Contributed by AV, 14-Mar-2019)

Ref Expression
Hypotheses pgrpsubgsymgbi.g ⊢ G = SymGrp ⁡ A
pgrpsubgsymgbi.b ⊢ B = Base G
Assertion pgrpsubgsymgbi ⊢ A ∈ V → P ∈ SubGrp ⁡ G ↔ P ⊆ B ∧ G ↾ 𝑠 P ∈ Grp

Proof

Step Hyp Ref Expression
1 pgrpsubgsymgbi.g ⊢ G = SymGrp ⁡ A
2 pgrpsubgsymgbi.b ⊢ B = Base G
3 2 issubg ⊢ P ∈ SubGrp ⁡ G ↔ G ∈ Grp ∧ P ⊆ B ∧ G ↾ 𝑠 P ∈ Grp
4 3anass ⊢ G ∈ Grp ∧ P ⊆ B ∧ G ↾ 𝑠 P ∈ Grp ↔ G ∈ Grp ∧ P ⊆ B ∧ G ↾ 𝑠 P ∈ Grp
5 3 4 bitri ⊢ P ∈ SubGrp ⁡ G ↔ G ∈ Grp ∧ P ⊆ B ∧ G ↾ 𝑠 P ∈ Grp
6 1 symggrp ⊢ A ∈ V → G ∈ Grp
7 ibar ⊢ G ∈ Grp → P ⊆ B ∧ G ↾ 𝑠 P ∈ Grp ↔ G ∈ Grp ∧ P ⊆ B ∧ G ↾ 𝑠 P ∈ Grp
8 7 bicomd ⊢ G ∈ Grp → G ∈ Grp ∧ P ⊆ B ∧ G ↾ 𝑠 P ∈ Grp ↔ P ⊆ B ∧ G ↾ 𝑠 P ∈ Grp
9 6 8 syl ⊢ A ∈ V → G ∈ Grp ∧ P ⊆ B ∧ G ↾ 𝑠 P ∈ Grp ↔ P ⊆ B ∧ G ↾ 𝑠 P ∈ Grp
10 5 9 bitrid ⊢ A ∈ V → P ∈ SubGrp ⁡ G ↔ P ⊆ B ∧ G ↾ 𝑠 P ∈ Grp