Metamath Proof Explorer


Theorem nfpconfp

Description: The set of fixed points of F is the complement of the set of points moved by F . (Contributed by Thierry Arnoux, 17-Nov-2023)

Ref Expression
Assertion nfpconfp FFnAAdomFI=domFI

Proof

Step Hyp Ref Expression
1 eldif xAdomFIxA¬xdomFI
2 fnelfp FFnAxAxdomFIFx=x
3 2 pm5.32da FFnAxAxdomFIxAFx=x
4 inss1 FIF
5 dmss FIFdomFIdomF
6 4 5 ax-mp domFIdomF
7 fndm FFnAdomF=A
8 6 7 sseqtrid FFnAdomFIA
9 8 sseld FFnAxdomFIxA
10 9 pm4.71rd FFnAxdomFIxAxdomFI
11 fnelnfp FFnAxAxdomFIFxx
12 11 notbid FFnAxA¬xdomFI¬Fxx
13 nne ¬FxxFx=x
14 12 13 bitrdi FFnAxA¬xdomFIFx=x
15 14 pm5.32da FFnAxA¬xdomFIxAFx=x
16 3 10 15 3bitr4rd FFnAxA¬xdomFIxdomFI
17 1 16 syl5bb FFnAxAdomFIxdomFI
18 17 eqrdv FFnAAdomFI=domFI