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 \to A ∖ dom (F ∖ I) = dom (F \cap I)$

Step	Hyp	Ref	Expression
1		eldif	$⊢ x \in (A ∖ dom (F ∖ I)) \leftrightarrow (x \in A \land \neg x \in dom (F ∖ I))$
2		fnelfp	$⊢ (F Fn A \land x \in A) \to (x \in dom (F \cap I) \leftrightarrow F (x) = x)$
3	2	pm5.32da	$⊢ F Fn A \to ((x \in A \land x \in dom (F \cap I)) \leftrightarrow (x \in A \land F (x) = x))$
4		inss1	$⊢ F \cap I \subseteq F$
5		dmss	$⊢ F \cap I \subseteq F \to dom (F \cap I) \subseteq dom F$
6	4 5	ax-mp	$⊢ dom (F \cap I) \subseteq dom F$
7		fndm	$⊢ F Fn A \to dom F = A$
8	6 7	sseqtrid	$⊢ F Fn A \to dom (F \cap I) \subseteq A$
9	8	sseld	$⊢ F Fn A \to (x \in dom (F \cap I) \to x \in A)$
10	9	pm4.71rd	$⊢ F Fn A \to (x \in dom (F \cap I) \leftrightarrow (x \in A \land x \in dom (F \cap I)))$
11		fnelnfp	$⊢ (F Fn A \land x \in A) \to (x \in dom (F ∖ I) \leftrightarrow F (x) \neq x)$
12	11	notbid	$⊢ (F Fn A \land x \in A) \to (\neg x \in dom (F ∖ I) \leftrightarrow \neg F (x) \neq x)$
13		nne	$⊢ \neg F (x) \neq x \leftrightarrow F (x) = x$
14	12 13	bitrdi	$⊢ (F Fn A \land x \in A) \to (\neg x \in dom (F ∖ I) \leftrightarrow F (x) = x)$
15	14	pm5.32da	$⊢ F Fn A \to ((x \in A \land \neg x \in dom (F ∖ I)) \leftrightarrow (x \in A \land F (x) = x))$
16	3 10 15	3bitr4rd	$⊢ F Fn A \to ((x \in A \land \neg x \in dom (F ∖ I)) \leftrightarrow x \in dom (F \cap I))$
17	1 16	syl5bb	$⊢ F Fn A \to (x \in (A ∖ dom (F ∖ I)) \leftrightarrow x \in dom (F \cap I))$
18	17	eqrdv	$⊢ F Fn A \to A ∖ dom (F ∖ I) = dom (F \cap I)$

Metamath Proof Explorer