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	⊢ ( 𝐹 Fn 𝐴 → ( 𝐴 ∖ dom ( 𝐹 ∖ I ) ) = dom ( 𝐹 ∩ I ) )

Proof

Step	Hyp	Ref	Expression
1		eldif	⊢ ( 𝑥 ∈ ( 𝐴 ∖ dom ( 𝐹 ∖ I ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ dom ( 𝐹 ∖ I ) ) )
2		fnelfp	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ dom ( 𝐹 ∩ I ) ↔ ( 𝐹 ‘ 𝑥 ) = 𝑥 ) )
3	2	pm5.32da	⊢ ( 𝐹 Fn 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ dom ( 𝐹 ∩ I ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑥 ) ) )
4		inss1	⊢ ( 𝐹 ∩ I ) ⊆ 𝐹
5		dmss	⊢ ( ( 𝐹 ∩ I ) ⊆ 𝐹 → dom ( 𝐹 ∩ I ) ⊆ dom 𝐹 )
6	4 5	ax-mp	⊢ dom ( 𝐹 ∩ I ) ⊆ dom 𝐹
7		fndm	⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
8	6 7	sseqtrid	⊢ ( 𝐹 Fn 𝐴 → dom ( 𝐹 ∩ I ) ⊆ 𝐴 )
9	8	sseld	⊢ ( 𝐹 Fn 𝐴 → ( 𝑥 ∈ dom ( 𝐹 ∩ I ) → 𝑥 ∈ 𝐴 ) )
10	9	pm4.71rd	⊢ ( 𝐹 Fn 𝐴 → ( 𝑥 ∈ dom ( 𝐹 ∩ I ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ dom ( 𝐹 ∩ I ) ) ) )
11		fnelnfp	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ dom ( 𝐹 ∖ I ) ↔ ( 𝐹 ‘ 𝑥 ) ≠ 𝑥 ) )
12	11	notbid	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ¬ 𝑥 ∈ dom ( 𝐹 ∖ I ) ↔ ¬ ( 𝐹 ‘ 𝑥 ) ≠ 𝑥 ) )
13		nne	⊢ ( ¬ ( 𝐹 ‘ 𝑥 ) ≠ 𝑥 ↔ ( 𝐹 ‘ 𝑥 ) = 𝑥 )
14	12 13	bitrdi	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ¬ 𝑥 ∈ dom ( 𝐹 ∖ I ) ↔ ( 𝐹 ‘ 𝑥 ) = 𝑥 ) )
15	14	pm5.32da	⊢ ( 𝐹 Fn 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ dom ( 𝐹 ∖ I ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑥 ) ) )
16	3 10 15	3bitr4rd	⊢ ( 𝐹 Fn 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ dom ( 𝐹 ∖ I ) ) ↔ 𝑥 ∈ dom ( 𝐹 ∩ I ) ) )
17	1 16	syl5bb	⊢ ( 𝐹 Fn 𝐴 → ( 𝑥 ∈ ( 𝐴 ∖ dom ( 𝐹 ∖ I ) ) ↔ 𝑥 ∈ dom ( 𝐹 ∩ I ) ) )
18	17	eqrdv	⊢ ( 𝐹 Fn 𝐴 → ( 𝐴 ∖ dom ( 𝐹 ∖ I ) ) = dom ( 𝐹 ∩ I ) )