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

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 ⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
psgneldm.n ⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
psgneldm.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion psgneldm ( 𝑃 ∈ dom 𝑁 ↔ ( 𝑃 ∈ 𝐵 ∧ dom ( 𝑃 ∖ I ) ∈ Fin ) )

Proof

Step Hyp Ref Expression
1 psgneldm.g ⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
2 psgneldm.n ⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
3 psgneldm.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
4 difeq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 ∖ I ) = ( 𝑃 ∖ I ) )
5 4 dmeqd ⊢ ( 𝑝 = 𝑃 → dom ( 𝑝 ∖ I ) = dom ( 𝑃 ∖ I ) )
6 5 eleq1d ⊢ ( 𝑝 = 𝑃 → ( dom ( 𝑝 ∖ I ) ∈ Fin ↔ dom ( 𝑃 ∖ I ) ∈ Fin ) )
7 eqid ⊢ { 𝑝 ∈ 𝐵 ∣ dom ( 𝑝 ∖ I ) ∈ Fin } = { 𝑝 ∈ 𝐵 ∣ dom ( 𝑝 ∖ I ) ∈ Fin }
8 1 3 7 2 psgnfn ⊢ 𝑁 Fn { 𝑝 ∈ 𝐵 ∣ dom ( 𝑝 ∖ I ) ∈ Fin }
9 8 fndmi ⊢ dom 𝑁 = { 𝑝 ∈ 𝐵 ∣ dom ( 𝑝 ∖ I ) ∈ Fin }
10 6 9 elrab2 ⊢ ( 𝑃 ∈ dom 𝑁 ↔ ( 𝑃 ∈ 𝐵 ∧ dom ( 𝑃 ∖ I ) ∈ Fin ) )