Metamath Proof Explorer

Theorem idrespermg

Description: The structure with the singleton containing only the identity function restricted to a set as base set and the function composition as group operation (constructed by (structure) restricting the symmetric group to that singleton) is a permutation group (group consisting of permutations). (Contributed by AV, 17-Mar-2019)

Ref Expression
Hypotheses idressubgsymg.g ⊢ G = SymGrp ⁡ A
idrespermg.e ⊢ E = G ↾ 𝑠 I ↾ A
Assertion idrespermg ⊢ A ∈ V → E ∈ Grp ∧ Base E ⊆ Base G

Proof

Step Hyp Ref Expression
1 idressubgsymg.g ⊢ G = SymGrp ⁡ A
2 idrespermg.e ⊢ E = G ↾ 𝑠 I ↾ A
3 1 idressubgsymg ⊢ A ∈ V → I ↾ A ∈ SubGrp ⁡ G
4 eqid ⊢ Base G = Base G
5 1 4 pgrpsubgsymgbi ⊢ A ∈ V → I ↾ A ∈ SubGrp ⁡ G ↔ I ↾ A ⊆ Base G ∧ G ↾ 𝑠 I ↾ A ∈ Grp
6 snex ⊢ I ↾ A ∈ V
7 2 4 ressbas ⊢ I ↾ A ∈ V → I ↾ A ∩ Base G = Base E
8 6 7 mp1i ⊢ A ∈ V → I ↾ A ∩ Base G = Base E
9 inss2 ⊢ I ↾ A ∩ Base G ⊆ Base G
10 8 9 eqsstrrdi ⊢ A ∈ V → Base E ⊆ Base G
11 2 eqcomi ⊢ G ↾ 𝑠 I ↾ A = E
12 11 eleq1i ⊢ G ↾ 𝑠 I ↾ A ∈ Grp ↔ E ∈ Grp
13 12 bilani ⊢ I ↾ A ⊆ Base G ∧ G ↾ 𝑠 I ↾ A ∈ Grp → E ∈ Grp
14 10 13 anim12ci ⊢ A ∈ V ∧ I ↾ A ⊆ Base G ∧ G ↾ 𝑠 I ↾ A ∈ Grp → E ∈ Grp ∧ Base E ⊆ Base G
15 14 ex ⊢ A ∈ V → I ↾ A ⊆ Base G ∧ G ↾ 𝑠 I ↾ A ∈ Grp → E ∈ Grp ∧ Base E ⊆ Base G
16 5 15 sylbid ⊢ A ∈ V → I ↾ A ∈ SubGrp ⁡ G → E ∈ Grp ∧ Base E ⊆ Base G
17 3 16 mpd ⊢ A ∈ V → E ∈ Grp ∧ Base E ⊆ Base G