This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fresin

Description: An identity for the mapping relationship under restriction. (Contributed by Scott Fenton, 4-Sep-2011) (Proof shortened by Mario Carneiro, 26-May-2016)

		Ref	Expression
	Assertion	fresin	$⊢ F : A ⟶ B \to ({F ↾}_{X}) : A \cap X ⟶ B$

Proof

Step	Hyp	Ref	Expression
1		inss1	$⊢ A \cap X \subseteq A$
2		fssres	$⊢ (F : A ⟶ B \land A \cap X \subseteq A) \to ({F ↾}_{(A \cap X)}) : A \cap X ⟶ B$
3	1 2	mpan2	$⊢ F : A ⟶ B \to ({F ↾}_{(A \cap X)}) : A \cap X ⟶ B$
4		resres	$⊢ {({F ↾}_{A}) ↾}_{X} = {F ↾}_{(A \cap X)}$
5		ffn	$⊢ F : A ⟶ B \to F Fn A$
6		fnresdm	$⊢ F Fn A \to {F ↾}_{A} = F$
7	5 6	syl	$⊢ F : A ⟶ B \to {F ↾}_{A} = F$
8	7	reseq1d	$⊢ F : A ⟶ B \to {({F ↾}_{A}) ↾}_{X} = {F ↾}_{X}$
9	4 8	eqtr3id	$⊢ F : A ⟶ B \to {F ↾}_{(A \cap X)} = {F ↾}_{X}$
10	9	feq1d	$⊢ F : A ⟶ B \to (({F ↾}_{(A \cap X)}) : A \cap X ⟶ B \leftrightarrow ({F ↾}_{X}) : A \cap X ⟶ B)$
11	3 10	mpbid	$⊢ F : A ⟶ B \to ({F ↾}_{X}) : A \cap X ⟶ B$