ffvresb

Description: A necessary and sufficient condition for a restricted function. (Contributed by Mario Carneiro, 14-Nov-2013)

		Ref	Expression
	Assertion	ffvresb	$⊢ Fun F \to (({F ↾}_{A}) : A ⟶ B \leftrightarrow \forall x \in A (x \in dom F \land F (x) \in B))$

Proof

Step	Hyp	Ref	Expression
1		fdm	$⊢ ({F ↾}_{A}) : A ⟶ B \to dom ({F ↾}_{A}) = A$
2		dmres	$⊢ dom ({F ↾}_{A}) = A \cap dom F$
3		inss2	$⊢ A \cap dom F \subseteq dom F$
4	2 3	eqsstri	$⊢ dom ({F ↾}_{A}) \subseteq dom F$
5	1 4	eqsstrrdi	$⊢ ({F ↾}_{A}) : A ⟶ B \to A \subseteq dom F$
6	5	sselda	$⊢ (({F ↾}_{A}) : A ⟶ B \land x \in A) \to x \in dom F$
7		fvres	$⊢ x \in A \to ({F ↾}_{A}) (x) = F (x)$
8	7	adantl	$⊢ (({F ↾}_{A}) : A ⟶ B \land x \in A) \to ({F ↾}_{A}) (x) = F (x)$
9		ffvelrn	$⊢ (({F ↾}_{A}) : A ⟶ B \land x \in A) \to ({F ↾}_{A}) (x) \in B$
10	8 9	eqeltrrd	$⊢ (({F ↾}_{A}) : A ⟶ B \land x \in A) \to F (x) \in B$
11	6 10	jca	$⊢ (({F ↾}_{A}) : A ⟶ B \land x \in A) \to (x \in dom F \land F (x) \in B)$
12	11	ralrimiva	$⊢ ({F ↾}_{A}) : A ⟶ B \to \forall x \in A (x \in dom F \land F (x) \in B)$
13		simpl	$⊢ (x \in dom F \land F (x) \in B) \to x \in dom F$
14	13	ralimi	$⊢ \forall x \in A (x \in dom F \land F (x) \in B) \to \forall x \in A x \in dom F$
15		dfss3	$⊢ A \subseteq dom F \leftrightarrow \forall x \in A x \in dom F$
16	14 15	sylibr	$⊢ \forall x \in A (x \in dom F \land F (x) \in B) \to A \subseteq dom F$
17		funfn	$⊢ Fun F \leftrightarrow F Fn dom F$
18		fnssres	$⊢ (F Fn dom F \land A \subseteq dom F) \to ({F ↾}_{A}) Fn A$
19	17 18	sylanb	$⊢ (Fun F \land A \subseteq dom F) \to ({F ↾}_{A}) Fn A$
20	16 19	sylan2	$⊢ (Fun F \land \forall x \in A (x \in dom F \land F (x) \in B)) \to ({F ↾}_{A}) Fn A$
21		simpr	$⊢ (x \in dom F \land F (x) \in B) \to F (x) \in B$
22	7	eleq1d	$⊢ x \in A \to (({F ↾}_{A}) (x) \in B \leftrightarrow F (x) \in B)$
23	21 22	syl5ibr	$⊢ x \in A \to ((x \in dom F \land F (x) \in B) \to ({F ↾}_{A}) (x) \in B)$
24	23	ralimia	$⊢ \forall x \in A (x \in dom F \land F (x) \in B) \to \forall x \in A ({F ↾}_{A}) (x) \in B$
25	24	adantl	$⊢ (Fun F \land \forall x \in A (x \in dom F \land F (x) \in B)) \to \forall x \in A ({F ↾}_{A}) (x) \in B$
26		fnfvrnss	$⊢ (({F ↾}_{A}) Fn A \land \forall x \in A ({F ↾}_{A}) (x) \in B) \to ran ({F ↾}_{A}) \subseteq B$
27	20 25 26	syl2anc	$⊢ (Fun F \land \forall x \in A (x \in dom F \land F (x) \in B)) \to ran ({F ↾}_{A}) \subseteq B$
28		df-f	$⊢ ({F ↾}_{A}) : A ⟶ B \leftrightarrow (({F ↾}_{A}) Fn A \land ran ({F ↾}_{A}) \subseteq B)$
29	20 27 28	sylanbrc	$⊢ (Fun F \land \forall x \in A (x \in dom F \land F (x) \in B)) \to ({F ↾}_{A}) : A ⟶ B$
30	29	ex	$⊢ Fun F \to (\forall x \in A (x \in dom F \land F (x) \in B) \to ({F ↾}_{A}) : A ⟶ B)$
31	12 30	impbid2	$⊢ Fun F \to (({F ↾}_{A}) : A ⟶ B \leftrightarrow \forall x \in A (x \in dom F \land F (x) \in B))$

Metamath Proof Explorer

Theorem ffvresb

Proof