dff3

Description: Alternate definition of a mapping. (Contributed by NM, 20-Mar-2007)

		Ref	Expression
	Assertion	dff3	$⊢ F : A ⟶ B \leftrightarrow (F \subseteq A \times B \land \forall x \in A \exists! y x F y)$

Proof

Step	Hyp	Ref	Expression
1		fssxp	$⊢ F : A ⟶ B \to F \subseteq A \times B$
2		ffun	$⊢ F : A ⟶ B \to Fun F$
3		fdm	$⊢ F : A ⟶ B \to dom F = A$
4	3	eleq2d	$⊢ F : A ⟶ B \to (x \in dom F \leftrightarrow x \in A)$
5	4	biimpar	$⊢ (F : A ⟶ B \land x \in A) \to x \in dom F$
6		funfvop	$⊢ (Fun F \land x \in dom F) \to ⟨x, F (x)⟩ \in F$
7	2 5 6	syl2an2r	$⊢ (F : A ⟶ B \land x \in A) \to ⟨x, F (x)⟩ \in F$
8		df-br	$⊢ x F F (x) \leftrightarrow ⟨x, F (x)⟩ \in F$
9	7 8	sylibr	$⊢ (F : A ⟶ B \land x \in A) \to x F F (x)$
10		fvex	$⊢ F (x) \in V$
11		breq2	$⊢ y = F (x) \to (x F y \leftrightarrow x F F (x))$
12	10 11	spcev	$⊢ x F F (x) \to \exists y x F y$
13	9 12	syl	$⊢ (F : A ⟶ B \land x \in A) \to \exists y x F y$
14		funmo	$⊢ Fun F \to \exists^{*} y x F y$
15	2 14	syl	$⊢ F : A ⟶ B \to \exists^{*} y x F y$
16	15	adantr	$⊢ (F : A ⟶ B \land x \in A) \to \exists^{*} y x F y$
17		df-eu	$⊢ \exists! y x F y \leftrightarrow (\exists y x F y \land \exists^{*} y x F y)$
18	13 16 17	sylanbrc	$⊢ (F : A ⟶ B \land x \in A) \to \exists! y x F y$
19	18	ralrimiva	$⊢ F : A ⟶ B \to \forall x \in A \exists! y x F y$
20	1 19	jca	$⊢ F : A ⟶ B \to (F \subseteq A \times B \land \forall x \in A \exists! y x F y)$
21		xpss	$⊢ A \times B \subseteq V \times V$
22		sstr	$⊢ (F \subseteq A \times B \land A \times B \subseteq V \times V) \to F \subseteq V \times V$
23	21 22	mpan2	$⊢ F \subseteq A \times B \to F \subseteq V \times V$
24		df-rel	$⊢ Rel F \leftrightarrow F \subseteq V \times V$
25	23 24	sylibr	$⊢ F \subseteq A \times B \to Rel F$
26	25	adantr	$⊢ (F \subseteq A \times B \land \forall x \in A \exists! y x F y) \to Rel F$
27		df-ral	$⊢ \forall x \in A \exists! y x F y \leftrightarrow \forall x (x \in A \to \exists! y x F y)$
28		eumo	$⊢ \exists! y x F y \to \exists^{*} y x F y$
29	28	imim2i	$⊢ (x \in A \to \exists! y x F y) \to (x \in A \to \exists^{*} y x F y)$
30	29	adantl	$⊢ (F \subseteq A \times B \land (x \in A \to \exists! y x F y)) \to (x \in A \to \exists^{*} y x F y)$
31		df-br	$⊢ x F y \leftrightarrow ⟨x, y⟩ \in F$
32		ssel	$⊢ F \subseteq A \times B \to (⟨x, y⟩ \in F \to ⟨x, y⟩ \in (A \times B))$
33	31 32	biimtrid	$⊢ F \subseteq A \times B \to (x F y \to ⟨x, y⟩ \in (A \times B))$
34		opelxp1	$⊢ ⟨x, y⟩ \in (A \times B) \to x \in A$
35	33 34	syl6	$⊢ F \subseteq A \times B \to (x F y \to x \in A)$
36	35	exlimdv	$⊢ F \subseteq A \times B \to (\exists y x F y \to x \in A)$
37	36	con3d	$⊢ F \subseteq A \times B \to (\neg x \in A \to \neg \exists y x F y)$
38		nexmo	$⊢ \neg \exists y x F y \to \exists^{*} y x F y$
39	37 38	syl6	$⊢ F \subseteq A \times B \to (\neg x \in A \to \exists^{*} y x F y)$
40	39	adantr	$⊢ (F \subseteq A \times B \land (x \in A \to \exists! y x F y)) \to (\neg x \in A \to \exists^{*} y x F y)$
41	30 40	pm2.61d	$⊢ (F \subseteq A \times B \land (x \in A \to \exists! y x F y)) \to \exists^{*} y x F y$
42	41	ex	$⊢ F \subseteq A \times B \to ((x \in A \to \exists! y x F y) \to \exists^{*} y x F y)$
43	42	alimdv	$⊢ F \subseteq A \times B \to (\forall x (x \in A \to \exists! y x F y) \to \forall x \exists^{*} y x F y)$
44	27 43	biimtrid	$⊢ F \subseteq A \times B \to (\forall x \in A \exists! y x F y \to \forall x \exists^{*} y x F y)$
45	44	imp	$⊢ (F \subseteq A \times B \land \forall x \in A \exists! y x F y) \to \forall x \exists^{*} y x F y$
46		dffun6	$⊢ Fun F \leftrightarrow (Rel F \land \forall x \exists^{*} y x F y)$
47	26 45 46	sylanbrc	$⊢ (F \subseteq A \times B \land \forall x \in A \exists! y x F y) \to Fun F$
48		dmss	$⊢ F \subseteq A \times B \to dom F \subseteq dom (A \times B)$
49		dmxpss	$⊢ dom (A \times B) \subseteq A$
50	48 49	sstrdi	$⊢ F \subseteq A \times B \to dom F \subseteq A$
51		breq1	$⊢ x = z \to (x F y \leftrightarrow z F y)$
52	51	eubidv	$⊢ x = z \to (\exists! y x F y \leftrightarrow \exists! y z F y)$
53	52	rspccv	$⊢ \forall x \in A \exists! y x F y \to (z \in A \to \exists! y z F y)$
54		euex	$⊢ \exists! y z F y \to \exists y z F y$
55		vex	$⊢ z \in V$
56	55	eldm	$⊢ z \in dom F \leftrightarrow \exists y z F y$
57	54 56	sylibr	$⊢ \exists! y z F y \to z \in dom F$
58	53 57	syl6	$⊢ \forall x \in A \exists! y x F y \to (z \in A \to z \in dom F)$
59	58	ssrdv	$⊢ \forall x \in A \exists! y x F y \to A \subseteq dom F$
60	50 59	anim12i	$⊢ (F \subseteq A \times B \land \forall x \in A \exists! y x F y) \to (dom F \subseteq A \land A \subseteq dom F)$
61		eqss	$⊢ dom F = A \leftrightarrow (dom F \subseteq A \land A \subseteq dom F)$
62	60 61	sylibr	$⊢ (F \subseteq A \times B \land \forall x \in A \exists! y x F y) \to dom F = A$
63		df-fn	$⊢ F Fn A \leftrightarrow (Fun F \land dom F = A)$
64	47 62 63	sylanbrc	$⊢ (F \subseteq A \times B \land \forall x \in A \exists! y x F y) \to F Fn A$
65		rnss	$⊢ F \subseteq A \times B \to ran F \subseteq ran (A \times B)$
66		rnxpss	$⊢ ran (A \times B) \subseteq B$
67	65 66	sstrdi	$⊢ F \subseteq A \times B \to ran F \subseteq B$
68	67	adantr	$⊢ (F \subseteq A \times B \land \forall x \in A \exists! y x F y) \to ran F \subseteq B$
69		df-f	$⊢ F : A ⟶ B \leftrightarrow (F Fn A \land ran F \subseteq B)$
70	64 68 69	sylanbrc	$⊢ (F \subseteq A \times B \land \forall x \in A \exists! y x F y) \to F : A ⟶ B$
71	20 70	impbii	$⊢ F : A ⟶ B \leftrightarrow (F \subseteq A \times B \land \forall x \in A \exists! y x F y)$

Metamath Proof Explorer

Theorem dff3

Proof