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

Metamath Proof Explorer

Theorem sygbasnfpfi

Description: The class of non-fixed points of a permutation of a finite set is finite. (Contributed by AV, 13-Jan-2019)

Ref Expression
Hypotheses psgnfvalfi.g ⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
psgnfvalfi.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion sygbasnfpfi ( ( 𝐷 ∈ Fin ∧ 𝑃 ∈ 𝐵 ) → dom ( 𝑃 ∖ I ) ∈ Fin )

Proof

Step Hyp Ref Expression
1 psgnfvalfi.g ⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
2 psgnfvalfi.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
3 1 2 symgbasf ⊢ ( 𝑃 ∈ 𝐵 → 𝑃 : 𝐷 ⟶ 𝐷 )
4 3 ffnd ⊢ ( 𝑃 ∈ 𝐵 → 𝑃 Fn 𝐷 )
5 4 adantl ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑃 ∈ 𝐵 ) → 𝑃 Fn 𝐷 )
6 fndifnfp ⊢ ( 𝑃 Fn 𝐷 → dom ( 𝑃 ∖ I ) = { 𝑥 ∈ 𝐷 ∣ ( 𝑃 ‘ 𝑥 ) ≠ 𝑥 } )
7 5 6 syl ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑃 ∈ 𝐵 ) → dom ( 𝑃 ∖ I ) = { 𝑥 ∈ 𝐷 ∣ ( 𝑃 ‘ 𝑥 ) ≠ 𝑥 } )
8 rabfi ⊢ ( 𝐷 ∈ Fin → { 𝑥 ∈ 𝐷 ∣ ( 𝑃 ‘ 𝑥 ) ≠ 𝑥 } ∈ Fin )
9 8 adantr ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑃 ∈ 𝐵 ) → { 𝑥 ∈ 𝐷 ∣ ( 𝑃 ‘ 𝑥 ) ≠ 𝑥 } ∈ Fin )
10 7 9 eqeltrd ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑃 ∈ 𝐵 ) → dom ( 𝑃 ∖ I ) ∈ Fin )