Metamath Proof Explorer

Theorem psgneldm

Description: Property of being a finitary permutation. (Contributed by Stefan O'Rear, 28-Aug-2015)

Ref Expression
Hypotheses psgneldm.g ⊢ G = SymGrp ⁡ D
psgneldm.n ⊢ N = pmSgn ⁡ D
psgneldm.b ⊢ B = Base G
Assertion psgneldm ⊢ P ∈ dom ⁡ N ↔ P ∈ B ∧ dom ⁡ P ∖ I ∈ Fin

Proof

Step Hyp Ref Expression
1 psgneldm.g ⊢ G = SymGrp ⁡ D
2 psgneldm.n ⊢ N = pmSgn ⁡ D
3 psgneldm.b ⊢ B = Base G
4 difeq1 ⊢ p = P → p ∖ I = P ∖ I
5 4 dmeqd ⊢ p = P → dom ⁡ p ∖ I = dom ⁡ P ∖ I
6 5 eleq1d ⊢ p = P → dom ⁡ p ∖ I ∈ Fin ↔ dom ⁡ P ∖ I ∈ Fin
7 eqid ⊢ p ∈ B | dom ⁡ p ∖ I ∈ Fin = p ∈ B | dom ⁡ p ∖ I ∈ Fin
8 1 3 7 2 psgnfn ⊢ N Fn p ∈ B | dom ⁡ p ∖ I ∈ Fin
9 8 fndmi ⊢ dom ⁡ N = p ∈ B | dom ⁡ p ∖ I ∈ Fin
10 6 9 elrab2 ⊢ P ∈ dom ⁡ N ↔ P ∈ B ∧ dom ⁡ P ∖ I ∈ Fin