Metamath Proof Explorer

Theorem psgndmfi

Description: For a finite base set, the permutation sign is defined for all permutations. (Contributed by Thierry Arnoux, 22-Aug-2020)

Ref Expression
Hypotheses psgndmfi.s ⊢ S = pmSgn ⁡ D
psgndmfi.g ⊢ G = Base SymGrp ⁡ D
Assertion psgndmfi ⊢ D ∈ Fin → S Fn G

Proof

Step Hyp Ref Expression
1 psgndmfi.s ⊢ S = pmSgn ⁡ D
2 psgndmfi.g ⊢ G = Base SymGrp ⁡ D
3 eqid ⊢ SymGrp ⁡ D = SymGrp ⁡ D
4 eqid ⊢ p ∈ G | dom ⁡ p ∖ I ∈ Fin = p ∈ G | dom ⁡ p ∖ I ∈ Fin
5 3 2 4 1 psgnfn ⊢ S Fn p ∈ G | dom ⁡ p ∖ I ∈ Fin
6 3 2 sygbasnfpfi ⊢ D ∈ Fin ∧ p ∈ G → dom ⁡ p ∖ I ∈ Fin
7 6 ralrimiva ⊢ D ∈ Fin → ∀ p ∈ G dom ⁡ p ∖ I ∈ Fin
8 rabid2 ⊢ G = p ∈ G | dom ⁡ p ∖ I ∈ Fin ↔ ∀ p ∈ G dom ⁡ p ∖ I ∈ Fin
9 7 8 sylibr ⊢ D ∈ Fin → G = p ∈ G | dom ⁡ p ∖ I ∈ Fin
10 9 eqcomd ⊢ D ∈ Fin → p ∈ G | dom ⁡ p ∖ I ∈ Fin = G
11 10 fneq2d ⊢ D ∈ Fin → S Fn p ∈ G | dom ⁡ p ∖ I ∈ Fin ↔ S Fn G
12 5 11 mpbii ⊢ D ∈ Fin → S Fn G