mptfnf

Description: The maps-to notation defines a function with domain. (Contributed by Scott Fenton, 21-Mar-2011) (Revised by Thierry Arnoux, 10-May-2017)

		Ref	Expression
	Hypothesis	mptfnf.0	$⊢ \underline{Ⅎ} x A$
	Assertion	mptfnf	$⊢ \forall x \in A B \in V \leftrightarrow (x \in A ⟼ B) Fn A$

Proof

Step	Hyp	Ref	Expression
1		mptfnf.0	$⊢ \underline{Ⅎ} x A$
2		eueq	$⊢ B \in V \leftrightarrow \exists! y y = B$
3	2	ralbii	$⊢ \forall x \in A B \in V \leftrightarrow \forall x \in A \exists! y y = B$
4		r19.26	$⊢ \forall x \in A (\exists y y = B \land \exists^{} y y = B) \leftrightarrow (\forall x \in A \exists y y = B \land \forall x \in A \exists^{} y y = B)$
5		df-eu	$⊢ \exists! y y = B \leftrightarrow (\exists y y = B \land \exists^{*} y y = B)$
6	5	ralbii	$⊢ \forall x \in A \exists! y y = B \leftrightarrow \forall x \in A (\exists y y = B \land \exists^{*} y y = B)$
7		df-mpt	$⊢ (x \in A ⟼ B) = \{⟨x, y⟩ \| (x \in A \land y = B)\}$
8	7	fneq1i	$⊢ (x \in A ⟼ B) Fn A \leftrightarrow \{⟨x, y⟩ \| (x \in A \land y = B)\} Fn A$
9		df-fn	$⊢ \{⟨x, y⟩ \| (x \in A \land y = B)\} Fn A \leftrightarrow (Fun \{⟨x, y⟩ \| (x \in A \land y = B)\} \land dom \{⟨x, y⟩ \| (x \in A \land y = B)\} = A)$
10	8 9	bitri	$⊢ (x \in A ⟼ B) Fn A \leftrightarrow (Fun \{⟨x, y⟩ \| (x \in A \land y = B)\} \land dom \{⟨x, y⟩ \| (x \in A \land y = B)\} = A)$
11		moanimv	$⊢ \exists^{} y (x \in A \land y = B) \leftrightarrow (x \in A \to \exists^{} y y = B)$
12	11	albii	$⊢ \forall x \exists^{} y (x \in A \land y = B) \leftrightarrow \forall x (x \in A \to \exists^{} y y = B)$
13		funopab	$⊢ Fun \{⟨x, y⟩ \| (x \in A \land y = B)\} \leftrightarrow \forall x \exists^{*} y (x \in A \land y = B)$
14		df-ral	$⊢ \forall x \in A \exists^{} y y = B \leftrightarrow \forall x (x \in A \to \exists^{} y y = B)$
15	12 13 14	3bitr4ri	$⊢ \forall x \in A \exists^{*} y y = B \leftrightarrow Fun \{⟨x, y⟩ \| (x \in A \land y = B)\}$
16		eqcom	$⊢ \{x \| (x \in A \land \exists y y = B)\} = A \leftrightarrow A = \{x \| (x \in A \land \exists y y = B)\}$
17		dmopab	$⊢ dom \{⟨x, y⟩ \| (x \in A \land y = B)\} = \{x \| \exists y (x \in A \land y = B)\}$
18		19.42v	$⊢ \exists y (x \in A \land y = B) \leftrightarrow (x \in A \land \exists y y = B)$
19	18	abbii	$⊢ \{x \| \exists y (x \in A \land y = B)\} = \{x \| (x \in A \land \exists y y = B)\}$
20	17 19	eqtri	$⊢ dom \{⟨x, y⟩ \| (x \in A \land y = B)\} = \{x \| (x \in A \land \exists y y = B)\}$
21	20	eqeq1i	$⊢ dom \{⟨x, y⟩ \| (x \in A \land y = B)\} = A \leftrightarrow \{x \| (x \in A \land \exists y y = B)\} = A$
22		pm4.71	$⊢ (x \in A \to \exists y y = B) \leftrightarrow (x \in A \leftrightarrow (x \in A \land \exists y y = B))$
23	22	albii	$⊢ \forall x (x \in A \to \exists y y = B) \leftrightarrow \forall x (x \in A \leftrightarrow (x \in A \land \exists y y = B))$
24		df-ral	$⊢ \forall x \in A \exists y y = B \leftrightarrow \forall x (x \in A \to \exists y y = B)$
25	1	eqabf	$⊢ A = \{x \| (x \in A \land \exists y y = B)\} \leftrightarrow \forall x (x \in A \leftrightarrow (x \in A \land \exists y y = B))$
26	23 24 25	3bitr4i	$⊢ \forall x \in A \exists y y = B \leftrightarrow A = \{x \| (x \in A \land \exists y y = B)\}$
27	16 21 26	3bitr4ri	$⊢ \forall x \in A \exists y y = B \leftrightarrow dom \{⟨x, y⟩ \| (x \in A \land y = B)\} = A$
28	15 27	anbi12i	$⊢ (\forall x \in A \exists^{*} y y = B \land \forall x \in A \exists y y = B) \leftrightarrow (Fun \{⟨x, y⟩ \| (x \in A \land y = B)\} \land dom \{⟨x, y⟩ \| (x \in A \land y = B)\} = A)$
29		ancom	$⊢ (\forall x \in A \exists^{} y y = B \land \forall x \in A \exists y y = B) \leftrightarrow (\forall x \in A \exists y y = B \land \forall x \in A \exists^{} y y = B)$
30	10 28 29	3bitr2i	$⊢ (x \in A ⟼ B) Fn A \leftrightarrow (\forall x \in A \exists y y = B \land \forall x \in A \exists^{*} y y = B)$
31	4 6 30	3bitr4ri	$⊢ (x \in A ⟼ B) Fn A \leftrightarrow \forall x \in A \exists! y y = B$
32	3 31	bitr4i	$⊢ \forall x \in A B \in V \leftrightarrow (x \in A ⟼ B) Fn A$

Metamath Proof Explorer

Theorem mptfnf

Proof