dff13

Description: A one-to-one function in terms of function values. Compare Theorem 4.8(iv) of Monk1 p. 43. (Contributed by NM, 29-Oct-1996)

		Ref	Expression
	Assertion	dff13	$⊢ F : A \underset{1-1}{⟶} B \leftrightarrow (F : A ⟶ B \land \forall x \in A \forall y \in A (F (x) = F (y) \to x = y))$

Proof

Step	Hyp	Ref	Expression
1		dff12	$⊢ F : A \underset{1-1}{⟶} B \leftrightarrow (F : A ⟶ B \land \forall z \exists^{*} x x F z)$
2		ffn	$⊢ F : A ⟶ B \to F Fn A$
3		vex	$⊢ x \in V$
4		vex	$⊢ z \in V$
5	3 4	breldm	$⊢ x F z \to x \in dom F$
6		fndm	$⊢ F Fn A \to dom F = A$
7	6	eleq2d	$⊢ F Fn A \to (x \in dom F \leftrightarrow x \in A)$
8	5 7	syl5ib	$⊢ F Fn A \to (x F z \to x \in A)$
9		vex	$⊢ y \in V$
10	9 4	breldm	$⊢ y F z \to y \in dom F$
11	6	eleq2d	$⊢ F Fn A \to (y \in dom F \leftrightarrow y \in A)$
12	10 11	syl5ib	$⊢ F Fn A \to (y F z \to y \in A)$
13	8 12	anim12d	$⊢ F Fn A \to ((x F z \land y F z) \to (x \in A \land y \in A))$
14	13	pm4.71rd	$⊢ F Fn A \to ((x F z \land y F z) \leftrightarrow ((x \in A \land y \in A) \land (x F z \land y F z)))$
15		eqcom	$⊢ z = F (x) \leftrightarrow F (x) = z$
16		fnbrfvb	$⊢ (F Fn A \land x \in A) \to (F (x) = z \leftrightarrow x F z)$
17	15 16	bitrid	$⊢ (F Fn A \land x \in A) \to (z = F (x) \leftrightarrow x F z)$
18		eqcom	$⊢ z = F (y) \leftrightarrow F (y) = z$
19		fnbrfvb	$⊢ (F Fn A \land y \in A) \to (F (y) = z \leftrightarrow y F z)$
20	18 19	bitrid	$⊢ (F Fn A \land y \in A) \to (z = F (y) \leftrightarrow y F z)$
21	17 20	bi2anan9	$⊢ ((F Fn A \land x \in A) \land (F Fn A \land y \in A)) \to ((z = F (x) \land z = F (y)) \leftrightarrow (x F z \land y F z))$
22	21	anandis	$⊢ (F Fn A \land (x \in A \land y \in A)) \to ((z = F (x) \land z = F (y)) \leftrightarrow (x F z \land y F z))$
23	22	pm5.32da	$⊢ F Fn A \to (((x \in A \land y \in A) \land (z = F (x) \land z = F (y))) \leftrightarrow ((x \in A \land y \in A) \land (x F z \land y F z)))$
24	14 23	bitr4d	$⊢ F Fn A \to ((x F z \land y F z) \leftrightarrow ((x \in A \land y \in A) \land (z = F (x) \land z = F (y))))$
25	24	imbi1d	$⊢ F Fn A \to (((x F z \land y F z) \to x = y) \leftrightarrow (((x \in A \land y \in A) \land (z = F (x) \land z = F (y))) \to x = y))$
26		impexp	$⊢ (((x \in A \land y \in A) \land (z = F (x) \land z = F (y))) \to x = y) \leftrightarrow ((x \in A \land y \in A) \to ((z = F (x) \land z = F (y)) \to x = y))$
27	25 26	bitrdi	$⊢ F Fn A \to (((x F z \land y F z) \to x = y) \leftrightarrow ((x \in A \land y \in A) \to ((z = F (x) \land z = F (y)) \to x = y)))$
28	27	albidv	$⊢ F Fn A \to (\forall z ((x F z \land y F z) \to x = y) \leftrightarrow \forall z ((x \in A \land y \in A) \to ((z = F (x) \land z = F (y)) \to x = y)))$
29		19.21v	$⊢ \forall z ((x \in A \land y \in A) \to ((z = F (x) \land z = F (y)) \to x = y)) \leftrightarrow ((x \in A \land y \in A) \to \forall z ((z = F (x) \land z = F (y)) \to x = y))$
30		19.23v	$⊢ \forall z ((z = F (x) \land z = F (y)) \to x = y) \leftrightarrow (\exists z (z = F (x) \land z = F (y)) \to x = y)$
31		fvex	$⊢ F (x) \in V$
32	31	eqvinc	$⊢ F (x) = F (y) \leftrightarrow \exists z (z = F (x) \land z = F (y))$
33	32	imbi1i	$⊢ (F (x) = F (y) \to x = y) \leftrightarrow (\exists z (z = F (x) \land z = F (y)) \to x = y)$
34	30 33	bitr4i	$⊢ \forall z ((z = F (x) \land z = F (y)) \to x = y) \leftrightarrow (F (x) = F (y) \to x = y)$
35	34	imbi2i	$⊢ ((x \in A \land y \in A) \to \forall z ((z = F (x) \land z = F (y)) \to x = y)) \leftrightarrow ((x \in A \land y \in A) \to (F (x) = F (y) \to x = y))$
36	29 35	bitri	$⊢ \forall z ((x \in A \land y \in A) \to ((z = F (x) \land z = F (y)) \to x = y)) \leftrightarrow ((x \in A \land y \in A) \to (F (x) = F (y) \to x = y))$
37	28 36	bitrdi	$⊢ F Fn A \to (\forall z ((x F z \land y F z) \to x = y) \leftrightarrow ((x \in A \land y \in A) \to (F (x) = F (y) \to x = y)))$
38	37	2albidv	$⊢ F Fn A \to (\forall x \forall y \forall z ((x F z \land y F z) \to x = y) \leftrightarrow \forall x \forall y ((x \in A \land y \in A) \to (F (x) = F (y) \to x = y)))$
39		breq1	$⊢ x = y \to (x F z \leftrightarrow y F z)$
40	39	mo4	$⊢ \exists^{*} x x F z \leftrightarrow \forall x \forall y ((x F z \land y F z) \to x = y)$
41	40	albii	$⊢ \forall z \exists^{*} x x F z \leftrightarrow \forall z \forall x \forall y ((x F z \land y F z) \to x = y)$
42		alrot3	$⊢ \forall z \forall x \forall y ((x F z \land y F z) \to x = y) \leftrightarrow \forall x \forall y \forall z ((x F z \land y F z) \to x = y)$
43	41 42	bitri	$⊢ \forall z \exists^{*} x x F z \leftrightarrow \forall x \forall y \forall z ((x F z \land y F z) \to x = y)$
44		r2al	$⊢ \forall x \in A \forall y \in A (F (x) = F (y) \to x = y) \leftrightarrow \forall x \forall y ((x \in A \land y \in A) \to (F (x) = F (y) \to x = y))$
45	38 43 44	3bitr4g	$⊢ F Fn A \to (\forall z \exists^{*} x x F z \leftrightarrow \forall x \in A \forall y \in A (F (x) = F (y) \to x = y))$
46	2 45	syl	$⊢ F : A ⟶ B \to (\forall z \exists^{*} x x F z \leftrightarrow \forall x \in A \forall y \in A (F (x) = F (y) \to x = y))$
47	46	pm5.32i	$⊢ (F : A ⟶ B \land \forall z \exists^{*} x x F z) \leftrightarrow (F : A ⟶ B \land \forall x \in A \forall y \in A (F (x) = F (y) \to x = y))$
48	1 47	bitri	$⊢ F : A \underset{1-1}{⟶} B \leftrightarrow (F : A ⟶ B \land \forall x \in A \forall y \in A (F (x) = F (y) \to x = y))$

Metamath Proof Explorer

Theorem dff13

Proof