fnnfpeq0

Description: A function is the identity iff it moves no points. (Contributed by Stefan O'Rear, 25-Aug-2015)

		Ref	Expression
	Assertion	fnnfpeq0	$⊢ F Fn A \to (dom (F ∖ I) = \emptyset \leftrightarrow F = {I ↾}_{A})$

Step	Hyp	Ref	Expression
1		rabeq0	$⊢ \{x \in A \| F (x) \neq x\} = \emptyset \leftrightarrow \forall x \in A \neg F (x) \neq x$
2		nne	$⊢ \neg F (x) \neq x \leftrightarrow F (x) = x$
3		fvresi	$⊢ x \in A \to ({I ↾}_{A}) (x) = x$
4	3	eqeq2d	$⊢ x \in A \to (F (x) = ({I ↾}_{A}) (x) \leftrightarrow F (x) = x)$
5	4	adantl	$⊢ (F Fn A \land x \in A) \to (F (x) = ({I ↾}_{A}) (x) \leftrightarrow F (x) = x)$
6	2 5	bitr4id	$⊢ (F Fn A \land x \in A) \to (\neg F (x) \neq x \leftrightarrow F (x) = ({I ↾}_{A}) (x))$
7	6	ralbidva	$⊢ F Fn A \to (\forall x \in A \neg F (x) \neq x \leftrightarrow \forall x \in A F (x) = ({I ↾}_{A}) (x))$
8	1 7	bitrid	$⊢ F Fn A \to (\{x \in A \| F (x) \neq x\} = \emptyset \leftrightarrow \forall x \in A F (x) = ({I ↾}_{A}) (x))$
9		fndifnfp	$⊢ F Fn A \to dom (F ∖ I) = \{x \in A \| F (x) \neq x\}$
10	9	eqeq1d	$⊢ F Fn A \to (dom (F ∖ I) = \emptyset \leftrightarrow \{x \in A \| F (x) \neq x\} = \emptyset)$
11		fnresi	$⊢ ({I ↾}_{A}) Fn A$
12		eqfnfv	$⊢ (F Fn A \land ({I ↾}_{A}) Fn A) \to (F = {I ↾}_{A} \leftrightarrow \forall x \in A F (x) = ({I ↾}_{A}) (x))$
13	11 12	mpan2	$⊢ F Fn A \to (F = {I ↾}_{A} \leftrightarrow \forall x \in A F (x) = ({I ↾}_{A}) (x))$
14	8 10 13	3bitr4d	$⊢ F Fn A \to (dom (F ∖ I) = \emptyset \leftrightarrow F = {I ↾}_{A})$

Metamath Proof Explorer