fnres

Description: An equivalence for functionality of a restriction. Compare dffun8 . (Contributed by Mario Carneiro, 20-May-2015) (Proof shortened by Peter Mazsa, 2-Oct-2022)

		Ref	Expression
	Assertion	fnres	$⊢ ({F ↾}_{A}) Fn A \leftrightarrow \forall x \in A \exists! y x F y$

Proof

Step	Hyp	Ref	Expression
1		ancom	$⊢ (\forall x \in A \exists^{} y x F y \land \forall x \in A \exists y x F y) \leftrightarrow (\forall x \in A \exists y x F y \land \forall x \in A \exists^{} y x F y)$
2		vex	$⊢ y \in V$
3	2	brresi	$⊢ x ({F ↾}_{A}) y \leftrightarrow (x \in A \land x F y)$
4	3	mobii	$⊢ \exists^{} y x ({F ↾}_{A}) y \leftrightarrow \exists^{} y (x \in A \land x F y)$
5		moanimv	$⊢ \exists^{} y (x \in A \land x F y) \leftrightarrow (x \in A \to \exists^{} y x F y)$
6	4 5	bitri	$⊢ \exists^{} y x ({F ↾}_{A}) y \leftrightarrow (x \in A \to \exists^{} y x F y)$
7	6	albii	$⊢ \forall x \exists^{} y x ({F ↾}_{A}) y \leftrightarrow \forall x (x \in A \to \exists^{} y x F y)$
8		relres	$⊢ Rel ({F ↾}_{A})$
9		dffun6	$⊢ Fun ({F ↾}_{A}) \leftrightarrow (Rel ({F ↾}_{A}) \land \forall x \exists^{*} y x ({F ↾}_{A}) y)$
10	8 9	mpbiran	$⊢ Fun ({F ↾}_{A}) \leftrightarrow \forall x \exists^{*} y x ({F ↾}_{A}) y$
11		df-ral	$⊢ \forall x \in A \exists^{} y x F y \leftrightarrow \forall x (x \in A \to \exists^{} y x F y)$
12	7 10 11	3bitr4i	$⊢ Fun ({F ↾}_{A}) \leftrightarrow \forall x \in A \exists^{*} y x F y$
13		dmres	$⊢ dom ({F ↾}_{A}) = A \cap dom F$
14		inss1	$⊢ A \cap dom F \subseteq A$
15	13 14	eqsstri	$⊢ dom ({F ↾}_{A}) \subseteq A$
16		eqss	$⊢ dom ({F ↾}_{A}) = A \leftrightarrow (dom ({F ↾}_{A}) \subseteq A \land A \subseteq dom ({F ↾}_{A}))$
17	15 16	mpbiran	$⊢ dom ({F ↾}_{A}) = A \leftrightarrow A \subseteq dom ({F ↾}_{A})$
18		dfss3	$⊢ A \subseteq dom ({F ↾}_{A}) \leftrightarrow \forall x \in A x \in dom ({F ↾}_{A})$
19	13	elin2	$⊢ x \in dom ({F ↾}_{A}) \leftrightarrow (x \in A \land x \in dom F)$
20	19	baib	$⊢ x \in A \to (x \in dom ({F ↾}_{A}) \leftrightarrow x \in dom F)$
21		vex	$⊢ x \in V$
22	21	eldm	$⊢ x \in dom F \leftrightarrow \exists y x F y$
23	20 22	bitrdi	$⊢ x \in A \to (x \in dom ({F ↾}_{A}) \leftrightarrow \exists y x F y)$
24	23	ralbiia	$⊢ \forall x \in A x \in dom ({F ↾}_{A}) \leftrightarrow \forall x \in A \exists y x F y$
25	18 24	bitri	$⊢ A \subseteq dom ({F ↾}_{A}) \leftrightarrow \forall x \in A \exists y x F y$
26	17 25	bitri	$⊢ dom ({F ↾}_{A}) = A \leftrightarrow \forall x \in A \exists y x F y$
27	12 26	anbi12i	$⊢ (Fun ({F ↾}_{A}) \land dom ({F ↾}_{A}) = A) \leftrightarrow (\forall x \in A \exists^{*} y x F y \land \forall x \in A \exists y x F y)$
28		r19.26	$⊢ \forall x \in A (\exists y x F y \land \exists^{} y x F y) \leftrightarrow (\forall x \in A \exists y x F y \land \forall x \in A \exists^{} y x F y)$
29	1 27 28	3bitr4i	$⊢ (Fun ({F ↾}_{A}) \land dom ({F ↾}_{A}) = A) \leftrightarrow \forall x \in A (\exists y x F y \land \exists^{*} y x F y)$
30		df-fn	$⊢ ({F ↾}_{A}) Fn A \leftrightarrow (Fun ({F ↾}_{A}) \land dom ({F ↾}_{A}) = A)$
31		df-eu	$⊢ \exists! y x F y \leftrightarrow (\exists y x F y \land \exists^{*} y x F y)$
32	31	ralbii	$⊢ \forall x \in A \exists! y x F y \leftrightarrow \forall x \in A (\exists y x F y \land \exists^{*} y x F y)$
33	29 30 32	3bitr4i	$⊢ ({F ↾}_{A}) Fn A \leftrightarrow \forall x \in A \exists! y x F y$

Metamath Proof Explorer

Theorem fnres

Proof