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=SymGrpD
psgneldm.n N=pmSgnD
Assertion psgndmsubg DVdomNSubGrpG

Proof

Step Hyp Ref Expression
1 psgneldm.g G=SymGrpD
2 psgneldm.n N=pmSgnD
3 eqid BaseG=BaseG
4 eqid pBaseG|dompIFin=pBaseG|dompIFin
5 1 3 4 2 psgnfn NFnpBaseG|dompIFin
6 fndm NFnpBaseG|dompIFindomN=pBaseG|dompIFin
7 5 6 ax-mp domN=pBaseG|dompIFin
8 1 3 symgfisg DVpBaseG|dompIFinSubGrpG
9 7 8 eqeltrid DVdomNSubGrpG