funcnvmpt

Description: Condition for a function in maps-to notation to be single-rooted. (Contributed by Thierry Arnoux, 28-Feb-2017) (Proof shortened by Peter Mazsa, 24-Feb-2026)

	Ref	Expression
Hypotheses	funcnvmpt.0	$⊢ Ⅎ x φ$
	funcnvmpt.1	$⊢ \underline{Ⅎ} x A$
	funcnvmpt.2	$⊢ \underline{Ⅎ} x F$
	funcnvmpt.3	$⊢ F = (x \in A ⟼ B)$
	funcnvmpt.4	$⊢ (φ \land x \in A) \to B \in V$
Assertion	funcnvmpt	$⊢ φ \to (Fun F^{-1} \leftrightarrow \forall y \exists^{*} x \in A y = B)$

Proof

Step	Hyp	Ref	Expression
1		funcnvmpt.0	$⊢ Ⅎ x φ$
2		funcnvmpt.1	$⊢ \underline{Ⅎ} x A$
3		funcnvmpt.2	$⊢ \underline{Ⅎ} x F$
4		funcnvmpt.3	$⊢ F = (x \in A ⟼ B)$
5		funcnvmpt.4	$⊢ (φ \land x \in A) \to B \in V$
6		relcnv	$⊢ Rel F^{-1}$
7		nfcv	$⊢ \underline{Ⅎ} y F^{-1}$
8	3	nfcnv	$⊢ \underline{Ⅎ} x F^{-1}$
9	7 8	dffun6f	$⊢ Fun F^{-1} \leftrightarrow (Rel F^{-1} \land \forall y \exists^{*} x y F^{-1} x)$
10	6 9	mpbiran	$⊢ Fun F^{-1} \leftrightarrow \forall y \exists^{*} x y F^{-1} x$
11		vex	$⊢ y \in V$
12		vex	$⊢ x \in V$
13	11 12	brcnv	$⊢ y F^{-1} x \leftrightarrow x F y$
14	13	mobii	$⊢ \exists^{} x y F^{-1} x \leftrightarrow \exists^{} x x F y$
15	14	albii	$⊢ \forall y \exists^{} x y F^{-1} x \leftrightarrow \forall y \exists^{} x x F y$
16	10 15	bitri	$⊢ Fun F^{-1} \leftrightarrow \forall y \exists^{*} x x F y$
17	4	funmpt2	$⊢ Fun F$
18		funbrfv2b	$⊢ Fun F \to (x F y \leftrightarrow (x \in dom F \land F (x) = y))$
19	17 18	ax-mp	$⊢ x F y \leftrightarrow (x \in dom F \land F (x) = y)$
20	4	dmmpt	$⊢ dom F = \{x \in A \| B \in V\}$
21	5	elexd	$⊢ (φ \land x \in A) \to B \in V$
22	1 21	ralrimia	$⊢ φ \to \forall x \in A B \in V$
23	2	rabid2f	$⊢ A = \{x \in A \| B \in V\} \leftrightarrow \forall x \in A B \in V$
24	22 23	sylibr	$⊢ φ \to A = \{x \in A \| B \in V\}$
25	20 24	eqtr4id	$⊢ φ \to dom F = A$
26	25	eleq2d	$⊢ φ \to (x \in dom F \leftrightarrow x \in A)$
27	26	anbi1d	$⊢ φ \to ((x \in dom F \land F (x) = y) \leftrightarrow (x \in A \land F (x) = y))$
28	19 27	bitrid	$⊢ φ \to (x F y \leftrightarrow (x \in A \land F (x) = y))$
29	28	bian1d	$⊢ φ \to ((x \in A \land x F y) \leftrightarrow (x \in A \land F (x) = y))$
30		simpr	$⊢ (φ \land x \in A) \to x \in A$
31	4	fveq1i	$⊢ F (x) = (x \in A ⟼ B) (x)$
32	2	fvmpt2f	$⊢ (x \in A \land B \in V) \to (x \in A ⟼ B) (x) = B$
33	31 32	eqtrid	$⊢ (x \in A \land B \in V) \to F (x) = B$
34	30 5 33	syl2anc	$⊢ (φ \land x \in A) \to F (x) = B$
35	34	eqeq2d	$⊢ (φ \land x \in A) \to (y = F (x) \leftrightarrow y = B)$
36		eqcom	$⊢ F (x) = y \leftrightarrow y = F (x)$
37	26	biimpar	$⊢ (φ \land x \in A) \to x \in dom F$
38		funbrfvb	$⊢ (Fun F \land x \in dom F) \to (F (x) = y \leftrightarrow x F y)$
39	17 37 38	sylancr	$⊢ (φ \land x \in A) \to (F (x) = y \leftrightarrow x F y)$
40	36 39	bitr3id	$⊢ (φ \land x \in A) \to (y = F (x) \leftrightarrow x F y)$
41	35 40	bitr3d	$⊢ (φ \land x \in A) \to (y = B \leftrightarrow x F y)$
42	41	pm5.32da	$⊢ φ \to ((x \in A \land y = B) \leftrightarrow (x \in A \land x F y))$
43	29 42 28	3bitr4rd	$⊢ φ \to (x F y \leftrightarrow (x \in A \land y = B))$
44	1 43	mobid	$⊢ φ \to (\exists^{} x x F y \leftrightarrow \exists^{} x (x \in A \land y = B))$
45		df-rmo	$⊢ \exists^{} x \in A y = B \leftrightarrow \exists^{} x (x \in A \land y = B)$
46	44 45	bitr4di	$⊢ φ \to (\exists^{} x x F y \leftrightarrow \exists^{} x \in A y = B)$
47	46	albidv	$⊢ φ \to (\forall y \exists^{} x x F y \leftrightarrow \forall y \exists^{} x \in A y = B)$
48	16 47	bitrid	$⊢ φ \to (Fun F^{-1} \leftrightarrow \forall y \exists^{*} x \in A y = B)$

Metamath Proof Explorer

Theorem funcnvmpt

Proof