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		inres	$⊢ I \cap ({F ↾}_{A}) = {(I \cap F) ↾}_{A}$
2		incom	$⊢ I \cap F = F \cap I$
3	2	reseq1i	$⊢ {(I \cap F) ↾}_{A} = {(F \cap I) ↾}_{A}$
4	1 3	eqtri	$⊢ I \cap ({F ↾}_{A}) = {(F \cap I) ↾}_{A}$
5		incom	$⊢ ({F ↾}_{A}) \cap I = I \cap ({F ↾}_{A})$
6		inres	$⊢ F \cap ({I ↾}_{A}) = {(F \cap I) ↾}_{A}$
7	4 5 6	3eqtr4i	$⊢ ({F ↾}_{A}) \cap I = F \cap ({I ↾}_{A})$
8		fnresdm	$⊢ F Fn A \to {F ↾}_{A} = F$
9	8	ineq1d	$⊢ F Fn A \to ({F ↾}_{A}) \cap I = F \cap I$
10	7 9	syl5reqr	$⊢ 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