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 
|- G = ( SymGrp ` D )
psgnfvalfi.b 
|- B = ( Base ` G )
Assertion sygbasnfpfi 
|- ( ( D e. Fin /\ P e. B ) -> dom ( P \ _I ) e. Fin )

Proof

Step Hyp Ref Expression
1 psgnfvalfi.g 
 |-  G = ( SymGrp ` D )
2 psgnfvalfi.b 
 |-  B = ( Base ` G )
3 1 2 symgbasf 
 |-  ( P e. B -> P : D --> D )
4 3 ffnd 
 |-  ( P e. B -> P Fn D )
5 4 adantl 
 |-  ( ( D e. Fin /\ P e. B ) -> P Fn D )
6 fndifnfp 
 |-  ( P Fn D -> dom ( P \ _I ) = { x e. D | ( P ` x ) =/= x } )
7 5 6 syl 
 |-  ( ( D e. Fin /\ P e. B ) -> dom ( P \ _I ) = { x e. D | ( P ` x ) =/= x } )
8 rabfi 
 |-  ( D e. Fin -> { x e. D | ( P ` x ) =/= x } e. Fin )
9 8 adantr 
 |-  ( ( D e. Fin /\ P e. B ) -> { x e. D | ( P ` x ) =/= x } e. Fin )
10 7 9 eqeltrd 
 |-  ( ( D e. Fin /\ P e. B ) -> dom ( P \ _I ) e. Fin )