funcnvmpt

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

	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	21	ex	$⊢ φ \to (x \in A \to B \in V)$
23	1 22	ralrimi	$⊢ φ \to \forall x \in A B \in V$
24	2	rabid2f	$⊢ A = \{x \in A \| B \in V\} \leftrightarrow \forall x \in A B \in V$
25	23 24	sylibr	$⊢ φ \to A = \{x \in A \| B \in V\}$
26	20 25	eqtr4id	$⊢ φ \to dom F = A$
27	26	eleq2d	$⊢ φ \to (x \in dom F \leftrightarrow x \in A)$
28	27	anbi1d	$⊢ φ \to ((x \in dom F \land F (x) = y) \leftrightarrow (x \in A \land F (x) = y))$
29	19 28	bitrid	$⊢ φ \to (x F y \leftrightarrow (x \in A \land F (x) = y))$
30	29	bian1d	$⊢ φ \to ((x \in A \land x F y) \leftrightarrow (x \in A \land F (x) = y))$
31		simpr	$⊢ (φ \land x \in A) \to x \in A$
32	4	fveq1i	$⊢ F (x) = (x \in A ⟼ B) (x)$
33	2	fvmpt2f	$⊢ (x \in A \land B \in V) \to (x \in A ⟼ B) (x) = B$
34	32 33	eqtrid	$⊢ (x \in A \land B \in V) \to F (x) = B$
35	31 5 34	syl2anc	$⊢ (φ \land x \in A) \to F (x) = B$
36	35	eqeq2d	$⊢ (φ \land x \in A) \to (y = F (x) \leftrightarrow y = B)$
37		eqcom	$⊢ F (x) = y \leftrightarrow y = F (x)$
38	27	biimpar	$⊢ (φ \land x \in A) \to x \in dom F$
39		funbrfvb	$⊢ (Fun F \land x \in dom F) \to (F (x) = y \leftrightarrow x F y)$
40	17 38 39	sylancr	$⊢ (φ \land x \in A) \to (F (x) = y \leftrightarrow x F y)$
41	37 40	bitr3id	$⊢ (φ \land x \in A) \to (y = F (x) \leftrightarrow x F y)$
42	36 41	bitr3d	$⊢ (φ \land x \in A) \to (y = B \leftrightarrow x F y)$
43	42	pm5.32da	$⊢ φ \to ((x \in A \land y = B) \leftrightarrow (x \in A \land x F y))$
44	30 43 29	3bitr4rd	$⊢ φ \to (x F y \leftrightarrow (x \in A \land y = B))$
45	1 44	mobid	$⊢ φ \to (\exists^{} x x F y \leftrightarrow \exists^{} x (x \in A \land y = B))$
46		df-rmo	$⊢ \exists^{} x \in A y = B \leftrightarrow \exists^{} x (x \in A \land y = B)$
47	45 46	bitr4di	$⊢ φ \to (\exists^{} x x F y \leftrightarrow \exists^{} x \in A y = B)$
48	47	albidv	$⊢ φ \to (\forall y \exists^{} x x F y \leftrightarrow \forall y \exists^{} x \in A y = B)$
49	16 48	bitrid	$⊢ φ \to (Fun F^{-1} \leftrightarrow \forall y \exists^{*} x \in A y = B)$

Metamath Proof Explorer

Theorem funcnvmpt

Proof