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

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 
|- ( F Fn A -> ( A \ dom ( F \ _I ) ) = dom ( F i^i _I ) )

Proof

Step Hyp Ref Expression
1 eldif 
 |-  ( x e. ( A \ dom ( F \ _I ) ) <-> ( x e. A /\ -. x e. dom ( F \ _I ) ) )
2 fnelfp 
 |-  ( ( F Fn A /\ x e. A ) -> ( x e. dom ( F i^i _I ) <-> ( F ` x ) = x ) )
3 2 pm5.32da 
 |-  ( F Fn A -> ( ( x e. A /\ x e. dom ( F i^i _I ) ) <-> ( x e. A /\ ( F ` x ) = x ) ) )
4 inss1 
 |-  ( F i^i _I ) C_ F
5 dmss 
 |-  ( ( F i^i _I ) C_ F -> dom ( F i^i _I ) C_ dom F )
6 4 5 ax-mp 
 |-  dom ( F i^i _I ) C_ dom F
7 fndm 
 |-  ( F Fn A -> dom F = A )
8 6 7 sseqtrid 
 |-  ( F Fn A -> dom ( F i^i _I ) C_ A )
9 8 sseld 
 |-  ( F Fn A -> ( x e. dom ( F i^i _I ) -> x e. A ) )
10 9 pm4.71rd 
 |-  ( F Fn A -> ( x e. dom ( F i^i _I ) <-> ( x e. A /\ x e. dom ( F i^i _I ) ) ) )
11 fnelnfp 
 |-  ( ( F Fn A /\ x e. A ) -> ( x e. dom ( F \ _I ) <-> ( F ` x ) =/= x ) )
12 11 notbid 
 |-  ( ( F Fn A /\ x e. A ) -> ( -. x e. dom ( F \ _I ) <-> -. ( F ` x ) =/= x ) )
13 nne 
 |-  ( -. ( F ` x ) =/= x <-> ( F ` x ) = x )
14 12 13 bitrdi 
 |-  ( ( F Fn A /\ x e. A ) -> ( -. x e. dom ( F \ _I ) <-> ( F ` x ) = x ) )
15 14 pm5.32da 
 |-  ( F Fn A -> ( ( x e. A /\ -. x e. dom ( F \ _I ) ) <-> ( x e. A /\ ( F ` x ) = x ) ) )
16 3 10 15 3bitr4rd 
 |-  ( F Fn A -> ( ( x e. A /\ -. x e. dom ( F \ _I ) ) <-> x e. dom ( F i^i _I ) ) )
17 1 16 bitrid 
 |-  ( F Fn A -> ( x e. ( A \ dom ( F \ _I ) ) <-> x e. dom ( F i^i _I ) ) )
18 17 eqrdv 
 |-  ( F Fn A -> ( A \ dom ( F \ _I ) ) = dom ( F i^i _I ) )