Metamath Proof Explorer

Theorem symgga

Description: The symmetric group induces a group action on its base set. (Contributed by Mario Carneiro, 24-Jan-2015)

Ref Expression
Hypotheses symgga.g ⊢ G = SymGrp ⁡ X
symgga.b ⊢ B = Base G
symgga.f ⊢ F = f ∈ B , x ∈ X ⟼ f ⁡ x
Assertion symgga ⊢ X ∈ V → F ∈ G GrpAct X

Proof

Step Hyp Ref Expression
1 symgga.g ⊢ G = SymGrp ⁡ X
2 symgga.b ⊢ B = Base G
3 symgga.f ⊢ F = f ∈ B , x ∈ X ⟼ f ⁡ x
4 1 symggrp ⊢ X ∈ V → G ∈ Grp
5 2 idghm ⊢ G ∈ Grp → I ↾ B ∈ G GrpHom G
6 fvresi ⊢ f ∈ B → I ↾ B ⁡ f = f
7 6 adantr ⊢ f ∈ B ∧ x ∈ X → I ↾ B ⁡ f = f
8 7 fveq1d ⊢ f ∈ B ∧ x ∈ X → I ↾ B ⁡ f ⁡ x = f ⁡ x
9 8 mpoeq3ia ⊢ f ∈ B , x ∈ X ⟼ I ↾ B ⁡ f ⁡ x = f ∈ B , x ∈ X ⟼ f ⁡ x
10 3 9 eqtr4i ⊢ F = f ∈ B , x ∈ X ⟼ I ↾ B ⁡ f ⁡ x
11 2 1 10 lactghmga ⊢ I ↾ B ∈ G GrpHom G → F ∈ G GrpAct X
12 4 5 11 3syl ⊢ X ∈ V → F ∈ G GrpAct X