This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
pgrpsubgsymgbi.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion pgrpsubgsymgbi ( 𝐴 ∈ 𝑉 → ( 𝑃 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑃 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝑃 ) ∈ Grp ) ) )

Proof

Step Hyp Ref Expression
1 pgrpsubgsymgbi.g ⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
2 pgrpsubgsymgbi.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
3 2 issubg ⊢ ( 𝑃 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝐺 ∈ Grp ∧ 𝑃 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝑃 ) ∈ Grp ) )
4 3anass ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑃 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝑃 ) ∈ Grp ) ↔ ( 𝐺 ∈ Grp ∧ ( 𝑃 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝑃 ) ∈ Grp ) ) )
5 3 4 bitri ⊢ ( 𝑃 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝐺 ∈ Grp ∧ ( 𝑃 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝑃 ) ∈ Grp ) ) )
6 1 symggrp ⊢ ( 𝐴 ∈ 𝑉 → 𝐺 ∈ Grp )
7 ibar ⊢ ( 𝐺 ∈ Grp → ( ( 𝑃 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝑃 ) ∈ Grp ) ↔ ( 𝐺 ∈ Grp ∧ ( 𝑃 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝑃 ) ∈ Grp ) ) ) )
8 7 bicomd ⊢ ( 𝐺 ∈ Grp → ( ( 𝐺 ∈ Grp ∧ ( 𝑃 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝑃 ) ∈ Grp ) ) ↔ ( 𝑃 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝑃 ) ∈ Grp ) ) )
9 6 8 syl ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐺 ∈ Grp ∧ ( 𝑃 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝑃 ) ∈ Grp ) ) ↔ ( 𝑃 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝑃 ) ∈ Grp ) ) )
10 5 9 bitrid ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑃 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑃 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝑃 ) ∈ Grp ) ) )