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 ) )