fndifnfp

Description: Express the class of non-fixed points of a function. (Contributed by Stefan O'Rear, 14-Aug-2015)

		Ref	Expression
	Assertion	fndifnfp	$⊢ F Fn A \to dom (F ∖ I) = \{x \in A \| F (x) \neq x\}$

Proof

Step	Hyp	Ref	Expression
1		dffn2	$⊢ F Fn A \leftrightarrow F : A ⟶ V$
2		fssxp	$⊢ F : A ⟶ V \to F \subseteq A \times V$
3	1 2	sylbi	$⊢ F Fn A \to F \subseteq A \times V$
4		ssdif0	$⊢ F \subseteq A \times V \leftrightarrow F ∖ (A \times V) = \emptyset$
5	3 4	sylib	$⊢ F Fn A \to F ∖ (A \times V) = \emptyset$
6	5	uneq2d	$⊢ F Fn A \to (F ∖ I) \cup (F ∖ (A \times V)) = (F ∖ I) \cup \emptyset$
7		un0	$⊢ (F ∖ I) \cup \emptyset = F ∖ I$
8	6 7	syl6req	$⊢ F Fn A \to F ∖ I = (F ∖ I) \cup (F ∖ (A \times V))$
9		df-res	$⊢ {I ↾}_{A} = I \cap (A \times V)$
10	9	difeq2i	$⊢ F ∖ ({I ↾}_{A}) = F ∖ (I \cap (A \times V))$
11		difindi	$⊢ F ∖ (I \cap (A \times V)) = (F ∖ I) \cup (F ∖ (A \times V))$
12	10 11	eqtri	$⊢ F ∖ ({I ↾}_{A}) = (F ∖ I) \cup (F ∖ (A \times V))$
13	8 12	syl6eqr	$⊢ F Fn A \to F ∖ I = F ∖ ({I ↾}_{A})$
14	13	dmeqd	$⊢ F Fn A \to dom (F ∖ I) = dom (F ∖ ({I ↾}_{A}))$
15		fnresi	$⊢ ({I ↾}_{A}) Fn A$
16		fndmdif	$⊢ (F Fn A \land ({I ↾}_{A}) Fn A) \to dom (F ∖ ({I ↾}_{A})) = \{x \in A \| F (x) \neq ({I ↾}_{A}) (x)\}$
17	15 16	mpan2	$⊢ F Fn A \to dom (F ∖ ({I ↾}_{A})) = \{x \in A \| F (x) \neq ({I ↾}_{A}) (x)\}$
18		fvresi	$⊢ x \in A \to ({I ↾}_{A}) (x) = x$
19	18	neeq2d	$⊢ x \in A \to (F (x) \neq ({I ↾}_{A}) (x) \leftrightarrow F (x) \neq x)$
20	19	rabbiia	$⊢ \{x \in A \| F (x) \neq ({I ↾}_{A}) (x)\} = \{x \in A \| F (x) \neq x\}$
21	20	a1i	$⊢ F Fn A \to \{x \in A \| F (x) \neq ({I ↾}_{A}) (x)\} = \{x \in A \| F (x) \neq x\}$
22	14 17 21	3eqtrd	$⊢ F Fn A \to dom (F ∖ I) = \{x \in A \| F (x) \neq x\}$

Metamath Proof Explorer

Theorem fndifnfp

Proof