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	syl5bb	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑃 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑃 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝑃 ) ∈ Grp ) ) )