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

Metamath Proof Explorer

Theorem psgndmsubg

Description: The finitary permutations are a subgroup. (Contributed by Stefan O'Rear, 28-Aug-2015)

Ref Expression
Hypotheses psgneldm.g ⊢ G = SymGrp ⁡ D
psgneldm.n ⊢ N = pmSgn ⁡ D
Assertion psgndmsubg ⊢ D ∈ V → dom ⁡ N ∈ SubGrp ⁡ G

Proof

Step Hyp Ref Expression
1 psgneldm.g ⊢ G = SymGrp ⁡ D
2 psgneldm.n ⊢ N = pmSgn ⁡ D
3 eqid ⊢ Base G = Base G
4 eqid ⊢ p ∈ Base G | dom ⁡ p ∖ I ∈ Fin = p ∈ Base G | dom ⁡ p ∖ I ∈ Fin
5 1 3 4 2 psgnfn ⊢ N Fn p ∈ Base G | dom ⁡ p ∖ I ∈ Fin
6 fndm ⊢ N Fn p ∈ Base G | dom ⁡ p ∖ I ∈ Fin → dom ⁡ N = p ∈ Base G | dom ⁡ p ∖ I ∈ Fin
7 5 6 ax-mp ⊢ dom ⁡ N = p ∈ Base G | dom ⁡ p ∖ I ∈ Fin
8 1 3 symgfisg ⊢ D ∈ V → p ∈ Base G | dom ⁡ p ∖ I ∈ Fin ∈ SubGrp ⁡ G
9 7 8 eqeltrid ⊢ D ∈ V → dom ⁡ N ∈ SubGrp ⁡ G