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 ( 𝐹 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 bitrid ⊢ ( 𝐹 Fn 𝐴 → ( 𝑥 ∈ ( 𝐴 ∖ dom ( 𝐹 ∖ I ) ) ↔ 𝑥 ∈ dom ( 𝐹 ∩ I ) ) )
18 17 eqrdv ⊢ ( 𝐹 Fn 𝐴 → ( 𝐴 ∖ dom ( 𝐹 ∖ I ) ) = dom ( 𝐹 ∩ I ) )