fninfp

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

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

Step	Hyp	Ref	Expression
1		fnresdm	$⊢ F Fn A \to {F ↾}_{A} = F$
2	1	ineq1d	$⊢ F Fn A \to ({F ↾}_{A}) \cap I = F \cap I$
3		inres	$⊢ I \cap ({F ↾}_{A}) = {(I \cap F) ↾}_{A}$
4		incom	$⊢ I \cap F = F \cap I$
5	4	reseq1i	$⊢ {(I \cap F) ↾}_{A} = {(F \cap I) ↾}_{A}$
6	3 5	eqtri	$⊢ I \cap ({F ↾}_{A}) = {(F \cap I) ↾}_{A}$
7		incom	$⊢ ({F ↾}_{A}) \cap I = I \cap ({F ↾}_{A})$
8		inres	$⊢ F \cap ({I ↾}_{A}) = {(F \cap I) ↾}_{A}$
9	6 7 8	3eqtr4i	$⊢ ({F ↾}_{A}) \cap I = F \cap ({I ↾}_{A})$
10	2 9	eqtr3di	$⊢ F Fn A \to F \cap I = F \cap ({I ↾}_{A})$
11	10	dmeqd	$⊢ F Fn A \to dom (F \cap I) = dom (F \cap ({I ↾}_{A}))$
12		fnresi	$⊢ ({I ↾}_{A}) Fn A$
13		fndmin	$⊢ (F Fn A \land ({I ↾}_{A}) Fn A) \to dom (F \cap ({I ↾}_{A})) = \{x \in A \| F (x) = ({I ↾}_{A}) (x)\}$
14	12 13	mpan2	$⊢ F Fn A \to dom (F \cap ({I ↾}_{A})) = \{x \in A \| F (x) = ({I ↾}_{A}) (x)\}$
15		fvresi	$⊢ x \in A \to ({I ↾}_{A}) (x) = x$
16	15	eqeq2d	$⊢ x \in A \to (F (x) = ({I ↾}_{A}) (x) \leftrightarrow F (x) = x)$
17	16	rabbiia	$⊢ \{x \in A \| F (x) = ({I ↾}_{A}) (x)\} = \{x \in A \| F (x) = x\}$
18	17	a1i	$⊢ F Fn A \to \{x \in A \| F (x) = ({I ↾}_{A}) (x)\} = \{x \in A \| F (x) = x\}$
19	11 14 18	3eqtrd	$⊢ F Fn A \to dom (F \cap I) = \{x \in A \| F (x) = x\}$

Metamath Proof Explorer