hashfun

Description: A finite set is a function iff it is equinumerous to its domain. (Contributed by Mario Carneiro, 26-Sep-2013) (Revised by Mario Carneiro, 12-Mar-2015)

		Ref	Expression
	Assertion	hashfun	$⊢ F \in Fin \to (Fun F \leftrightarrow \|F\| = \|dom F\|)$

Proof

Step	Hyp	Ref	Expression
1		funfn	$⊢ Fun F \leftrightarrow F Fn dom F$
2		hashfn	$⊢ F Fn dom F \to \|F\| = \|dom F\|$
3	1 2	sylbi	$⊢ Fun F \to \|F\| = \|dom F\|$
4		dmfi	$⊢ F \in Fin \to dom F \in Fin$
5		hashcl	$⊢ dom F \in Fin \to \|dom F\| \in ℕ_{0}$
6	4 5	syl	$⊢ F \in Fin \to \|dom F\| \in ℕ_{0}$
7	6	nn0red	$⊢ F \in Fin \to \|dom F\| \in ℝ$
8	7	adantr	$⊢ (F \in Fin \land \neg Rel F) \to \|dom F\| \in ℝ$
9		df-rel	$⊢ Rel F \leftrightarrow F \subseteq V \times V$
10		dfss3	$⊢ F \subseteq V \times V \leftrightarrow \forall x \in F x \in (V \times V)$
11	9 10	bitri	$⊢ Rel F \leftrightarrow \forall x \in F x \in (V \times V)$
12	11	notbii	$⊢ \neg Rel F \leftrightarrow \neg \forall x \in F x \in (V \times V)$
13		rexnal	$⊢ \exists x \in F \neg x \in (V \times V) \leftrightarrow \neg \forall x \in F x \in (V \times V)$
14	12 13	bitr4i	$⊢ \neg Rel F \leftrightarrow \exists x \in F \neg x \in (V \times V)$
15		dmun	$⊢ dom ((F ∖ \{x\}) \cup \{x\}) = dom (F ∖ \{x\}) \cup dom \{x\}$
16	15	fveq2i	$⊢ \|dom ((F ∖ \{x\}) \cup \{x\})\| = \|dom (F ∖ \{x\}) \cup dom \{x\}\|$
17		dmsnn0	$⊢ x \in (V \times V) \leftrightarrow dom \{x\} \neq \emptyset$
18	17	biimpri	$⊢ dom \{x\} \neq \emptyset \to x \in (V \times V)$
19	18	necon1bi	$⊢ \neg x \in (V \times V) \to dom \{x\} = \emptyset$
20	19	3ad2ant3	$⊢ (F \in Fin \land x \in F \land \neg x \in (V \times V)) \to dom \{x\} = \emptyset$
21	20	uneq2d	$⊢ (F \in Fin \land x \in F \land \neg x \in (V \times V)) \to dom (F ∖ \{x\}) \cup dom \{x\} = dom (F ∖ \{x\}) \cup \emptyset$
22		un0	$⊢ dom (F ∖ \{x\}) \cup \emptyset = dom (F ∖ \{x\})$
23	21 22	syl6eq	$⊢ (F \in Fin \land x \in F \land \neg x \in (V \times V)) \to dom (F ∖ \{x\}) \cup dom \{x\} = dom (F ∖ \{x\})$
24	23	fveq2d	$⊢ (F \in Fin \land x \in F \land \neg x \in (V \times V)) \to \|dom (F ∖ \{x\}) \cup dom \{x\}\| = \|dom (F ∖ \{x\})\|$
25	16 24	syl5eq	$⊢ (F \in Fin \land x \in F \land \neg x \in (V \times V)) \to \|dom ((F ∖ \{x\}) \cup \{x\})\| = \|dom (F ∖ \{x\})\|$
26		diffi	$⊢ F \in Fin \to F ∖ \{x\} \in Fin$
27		dmfi	$⊢ F ∖ \{x\} \in Fin \to dom (F ∖ \{x\}) \in Fin$
28	26 27	syl	$⊢ F \in Fin \to dom (F ∖ \{x\}) \in Fin$
29		hashcl	$⊢ dom (F ∖ \{x\}) \in Fin \to \|dom (F ∖ \{x\})\| \in ℕ_{0}$
30	28 29	syl	$⊢ F \in Fin \to \|dom (F ∖ \{x\})\| \in ℕ_{0}$
31	30	nn0red	$⊢ F \in Fin \to \|dom (F ∖ \{x\})\| \in ℝ$
32		hashcl	$⊢ F ∖ \{x\} \in Fin \to \|F ∖ \{x\}\| \in ℕ_{0}$
33	26 32	syl	$⊢ F \in Fin \to \|F ∖ \{x\}\| \in ℕ_{0}$
34	33	nn0red	$⊢ F \in Fin \to \|F ∖ \{x\}\| \in ℝ$
35		peano2re	$⊢ \|F ∖ \{x\}\| \in ℝ \to \|F ∖ \{x\}\| + 1 \in ℝ$
36	34 35	syl	$⊢ F \in Fin \to \|F ∖ \{x\}\| + 1 \in ℝ$
37		fidomdm	$⊢ F ∖ \{x\} \in Fin \to dom (F ∖ \{x\}) ≼ (F ∖ \{x\})$
38	26 37	syl	$⊢ F \in Fin \to dom (F ∖ \{x\}) ≼ (F ∖ \{x\})$
39		hashdom	$⊢ (dom (F ∖ \{x\}) \in Fin \land F ∖ \{x\} \in Fin) \to (\|dom (F ∖ \{x\})\| \leq \|F ∖ \{x\}\| \leftrightarrow dom (F ∖ \{x\}) ≼ (F ∖ \{x\}))$
40	28 26 39	syl2anc	$⊢ F \in Fin \to (\|dom (F ∖ \{x\})\| \leq \|F ∖ \{x\}\| \leftrightarrow dom (F ∖ \{x\}) ≼ (F ∖ \{x\}))$
41	38 40	mpbird	$⊢ F \in Fin \to \|dom (F ∖ \{x\})\| \leq \|F ∖ \{x\}\|$
42	34	ltp1d	$⊢ F \in Fin \to \|F ∖ \{x\}\| < \|F ∖ \{x\}\| + 1$
43	31 34 36 41 42	lelttrd	$⊢ F \in Fin \to \|dom (F ∖ \{x\})\| < \|F ∖ \{x\}\| + 1$
44	43	3ad2ant1	$⊢ (F \in Fin \land x \in F \land \neg x \in (V \times V)) \to \|dom (F ∖ \{x\})\| < \|F ∖ \{x\}\| + 1$
45	25 44	eqbrtrd	$⊢ (F \in Fin \land x \in F \land \neg x \in (V \times V)) \to \|dom ((F ∖ \{x\}) \cup \{x\})\| < \|F ∖ \{x\}\| + 1$
46		snfi	$⊢ \{x\} \in Fin$
47		incom	$⊢ (F ∖ \{x\}) \cap \{x\} = \{x\} \cap (F ∖ \{x\})$
48		disjdif	$⊢ \{x\} \cap (F ∖ \{x\}) = \emptyset$
49	47 48	eqtri	$⊢ (F ∖ \{x\}) \cap \{x\} = \emptyset$
50		hashun	$⊢ (F ∖ \{x\} \in Fin \land \{x\} \in Fin \land (F ∖ \{x\}) \cap \{x\} = \emptyset) \to \|(F ∖ \{x\}) \cup \{x\}\| = \|F ∖ \{x\}\| + \|\{x\}\|$
51	46 49 50	mp3an23	$⊢ F ∖ \{x\} \in Fin \to \|(F ∖ \{x\}) \cup \{x\}\| = \|F ∖ \{x\}\| + \|\{x\}\|$
52	26 51	syl	$⊢ F \in Fin \to \|(F ∖ \{x\}) \cup \{x\}\| = \|F ∖ \{x\}\| + \|\{x\}\|$
53		hashsng	$⊢ x \in V \to \|\{x\}\| = 1$
54	53	elv	$⊢ \|\{x\}\| = 1$
55	54	oveq2i	$⊢ \|F ∖ \{x\}\| + \|\{x\}\| = \|F ∖ \{x\}\| + 1$
56	52 55	syl6req	$⊢ F \in Fin \to \|F ∖ \{x\}\| + 1 = \|(F ∖ \{x\}) \cup \{x\}\|$
57	56	3ad2ant1	$⊢ (F \in Fin \land x \in F \land \neg x \in (V \times V)) \to \|F ∖ \{x\}\| + 1 = \|(F ∖ \{x\}) \cup \{x\}\|$
58	45 57	breqtrd	$⊢ (F \in Fin \land x \in F \land \neg x \in (V \times V)) \to \|dom ((F ∖ \{x\}) \cup \{x\})\| < \|(F ∖ \{x\}) \cup \{x\}\|$
59		difsnid	$⊢ x \in F \to (F ∖ \{x\}) \cup \{x\} = F$
60	59	dmeqd	$⊢ x \in F \to dom ((F ∖ \{x\}) \cup \{x\}) = dom F$
61	60	fveq2d	$⊢ x \in F \to \|dom ((F ∖ \{x\}) \cup \{x\})\| = \|dom F\|$
62	61	3ad2ant2	$⊢ (F \in Fin \land x \in F \land \neg x \in (V \times V)) \to \|dom ((F ∖ \{x\}) \cup \{x\})\| = \|dom F\|$
63	59	fveq2d	$⊢ x \in F \to \|(F ∖ \{x\}) \cup \{x\}\| = \|F\|$
64	63	3ad2ant2	$⊢ (F \in Fin \land x \in F \land \neg x \in (V \times V)) \to \|(F ∖ \{x\}) \cup \{x\}\| = \|F\|$
65	58 62 64	3brtr3d	$⊢ (F \in Fin \land x \in F \land \neg x \in (V \times V)) \to \|dom F\| < \|F\|$
66	65	rexlimdv3a	$⊢ F \in Fin \to (\exists x \in F \neg x \in (V \times V) \to \|dom F\| < \|F\|)$
67	14 66	syl5bi	$⊢ F \in Fin \to (\neg Rel F \to \|dom F\| < \|F\|)$
68	67	imp	$⊢ (F \in Fin \land \neg Rel F) \to \|dom F\| < \|F\|$
69	8 68	gtned	$⊢ (F \in Fin \land \neg Rel F) \to \|F\| \neq \|dom F\|$
70	69	ex	$⊢ F \in Fin \to (\neg Rel F \to \|F\| \neq \|dom F\|)$
71	70	necon4bd	$⊢ F \in Fin \to (\|F\| = \|dom F\| \to Rel F)$
72	71	imp	$⊢ (F \in Fin \land \|F\| = \|dom F\|) \to Rel F$
73		2nalexn	$⊢ \neg \forall x \forall y \forall z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z) \leftrightarrow \exists x \exists y \neg \forall z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z)$
74		df-ne	$⊢ y \neq z \leftrightarrow \neg y = z$
75	74	anbi2i	$⊢ ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z) \leftrightarrow ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land \neg y = z)$
76		annim	$⊢ ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land \neg y = z) \leftrightarrow \neg ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z)$
77	75 76	bitri	$⊢ ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z) \leftrightarrow \neg ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z)$
78	77	exbii	$⊢ \exists z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z) \leftrightarrow \exists z \neg ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z)$
79		exnal	$⊢ \exists z \neg ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z) \leftrightarrow \neg \forall z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z)$
80	78 79	bitr2i	$⊢ \neg \forall z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z) \leftrightarrow \exists z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z)$
81	80	2exbii	$⊢ \exists x \exists y \neg \forall z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z) \leftrightarrow \exists x \exists y \exists z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z)$
82	73 81	bitri	$⊢ \neg \forall x \forall y \forall z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z) \leftrightarrow \exists x \exists y \exists z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z)$
83	7	adantr	$⊢ (F \in Fin \land ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z)) \to \|dom F\| \in ℝ$
84		2re	$⊢ 2 \in ℝ$
85		diffi	$⊢ F \in Fin \to F ∖ \{⟨x, y⟩, ⟨x, z⟩\} \in Fin$
86		dmfi	$⊢ F ∖ \{⟨x, y⟩, ⟨x, z⟩\} \in Fin \to dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\}) \in Fin$
87	85 86	syl	$⊢ F \in Fin \to dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\}) \in Fin$
88		hashcl	$⊢ dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\}) \in Fin \to \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \in ℕ_{0}$
89	87 88	syl	$⊢ F \in Fin \to \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \in ℕ_{0}$
90	89	nn0red	$⊢ F \in Fin \to \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \in ℝ$
91	90	adantr	$⊢ (F \in Fin \land ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z)) \to \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \in ℝ$
92		readdcl	$⊢ (2 \in ℝ \land \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \in ℝ) \to 2 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \in ℝ$
93	84 91 92	sylancr	$⊢ (F \in Fin \land ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z)) \to 2 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \in ℝ$
94		hashcl	$⊢ F \in Fin \to \|F\| \in ℕ_{0}$
95	94	nn0red	$⊢ F \in Fin \to \|F\| \in ℝ$
96	95	adantr	$⊢ (F \in Fin \land ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z)) \to \|F\| \in ℝ$
97		1re	$⊢ 1 \in ℝ$
98		readdcl	$⊢ (1 \in ℝ \land \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \in ℝ) \to 1 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \in ℝ$
99	97 90 98	sylancr	$⊢ F \in Fin \to 1 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \in ℝ$
100	99	adantr	$⊢ (F \in Fin \land ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z)) \to 1 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \in ℝ$
101	84 90 92	sylancr	$⊢ F \in Fin \to 2 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \in ℝ$
102	101	adantr	$⊢ (F \in Fin \land ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z)) \to 2 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \in ℝ$
103		dmun	$⊢ dom (\{⟨x, y⟩, ⟨x, z⟩\} \cup (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})) = dom \{⟨x, y⟩, ⟨x, z⟩\} \cup dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})$
104		opex	$⊢ ⟨x, y⟩ \in V$
105		opex	$⊢ ⟨x, z⟩ \in V$
106	104 105	prss	$⊢ (⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \leftrightarrow \{⟨x, y⟩, ⟨x, z⟩\} \subseteq F$
107		undif	$⊢ \{⟨x, y⟩, ⟨x, z⟩\} \subseteq F \leftrightarrow \{⟨x, y⟩, ⟨x, z⟩\} \cup (F ∖ \{⟨x, y⟩, ⟨x, z⟩\}) = F$
108	106 107	sylbb	$⊢ (⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to \{⟨x, y⟩, ⟨x, z⟩\} \cup (F ∖ \{⟨x, y⟩, ⟨x, z⟩\}) = F$
109	108	dmeqd	$⊢ (⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to dom (\{⟨x, y⟩, ⟨x, z⟩\} \cup (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})) = dom F$
110	103 109	syl5reqr	$⊢ (⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to dom F = dom \{⟨x, y⟩, ⟨x, z⟩\} \cup dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})$
111		vex	$⊢ y \in V$
112		vex	$⊢ z \in V$
113	111 112	dmprop	$⊢ dom \{⟨x, y⟩, ⟨x, z⟩\} = \{x, x\}$
114		dfsn2	$⊢ \{x\} = \{x, x\}$
115	113 114	eqtr4i	$⊢ dom \{⟨x, y⟩, ⟨x, z⟩\} = \{x\}$
116	115	uneq1i	$⊢ dom \{⟨x, y⟩, ⟨x, z⟩\} \cup dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\}) = \{x\} \cup dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})$
117	110 116	syl6eq	$⊢ (⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to dom F = \{x\} \cup dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})$
118	117	fveq2d	$⊢ (⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to \|dom F\| = \|\{x\} \cup dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\|$
119	118	ad2antrl	$⊢ (F \in Fin \land ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z)) \to \|dom F\| = \|\{x\} \cup dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\|$
120		hashun2	$⊢ (\{x\} \in Fin \land dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\}) \in Fin) \to \|\{x\} \cup dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \leq \|\{x\}\| + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\|$
121	46 87 120	sylancr	$⊢ F \in Fin \to \|\{x\} \cup dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \leq \|\{x\}\| + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\|$
122	54	oveq1i	$⊢ \|\{x\}\| + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| = 1 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\|$
123	121 122	breqtrdi	$⊢ F \in Fin \to \|\{x\} \cup dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \leq 1 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\|$
124	123	adantr	$⊢ (F \in Fin \land ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z)) \to \|\{x\} \cup dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \leq 1 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\|$
125	119 124	eqbrtrd	$⊢ (F \in Fin \land ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z)) \to \|dom F\| \leq 1 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\|$
126		1lt2	$⊢ 1 < 2$
127		ltadd1	$⊢ (1 \in ℝ \land 2 \in ℝ \land \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \in ℝ) \to (1 < 2 \leftrightarrow 1 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| < 2 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\|)$
128	97 84 90 127	mp3an12i	$⊢ F \in Fin \to (1 < 2 \leftrightarrow 1 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| < 2 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\|)$
129	126 128	mpbii	$⊢ F \in Fin \to 1 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| < 2 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\|$
130	129	adantr	$⊢ (F \in Fin \land ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z)) \to 1 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| < 2 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\|$
131	83 100 102 125 130	lelttrd	$⊢ (F \in Fin \land ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z)) \to \|dom F\| < 2 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\|$
132		fidomdm	$⊢ F ∖ \{⟨x, y⟩, ⟨x, z⟩\} \in Fin \to dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\}) ≼ (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})$
133	85 132	syl	$⊢ F \in Fin \to dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\}) ≼ (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})$
134		hashdom	$⊢ (dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\}) \in Fin \land F ∖ \{⟨x, y⟩, ⟨x, z⟩\} \in Fin) \to (\|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \leq \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\| \leftrightarrow dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\}) ≼ (F ∖ \{⟨x, y⟩, ⟨x, z⟩\}))$
135	87 85 134	syl2anc	$⊢ F \in Fin \to (\|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \leq \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\| \leftrightarrow dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\}) ≼ (F ∖ \{⟨x, y⟩, ⟨x, z⟩\}))$
136	133 135	mpbird	$⊢ F \in Fin \to \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \leq \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\|$
137		hashcl	$⊢ F ∖ \{⟨x, y⟩, ⟨x, z⟩\} \in Fin \to \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\| \in ℕ_{0}$
138	85 137	syl	$⊢ F \in Fin \to \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\| \in ℕ_{0}$
139	138	nn0red	$⊢ F \in Fin \to \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\| \in ℝ$
140		leadd2	$⊢ (\|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \in ℝ \land \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\| \in ℝ \land 2 \in ℝ) \to (\|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \leq \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\| \leftrightarrow 2 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \leq 2 + \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\|)$
141	84 140	mp3an3	$⊢ (\|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \in ℝ \land \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\| \in ℝ) \to (\|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \leq \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\| \leftrightarrow 2 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \leq 2 + \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\|)$
142	90 139 141	syl2anc	$⊢ F \in Fin \to (\|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \leq \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\| \leftrightarrow 2 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \leq 2 + \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\|)$
143	136 142	mpbid	$⊢ F \in Fin \to 2 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \leq 2 + \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\|$
144	143	adantr	$⊢ (F \in Fin \land ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z)) \to 2 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \leq 2 + \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\|$
145		prfi	$⊢ \{⟨x, y⟩, ⟨x, z⟩\} \in Fin$
146		disjdif	$⊢ \{⟨x, y⟩, ⟨x, z⟩\} \cap (F ∖ \{⟨x, y⟩, ⟨x, z⟩\}) = \emptyset$
147		hashun	$⊢ (\{⟨x, y⟩, ⟨x, z⟩\} \in Fin \land F ∖ \{⟨x, y⟩, ⟨x, z⟩\} \in Fin \land \{⟨x, y⟩, ⟨x, z⟩\} \cap (F ∖ \{⟨x, y⟩, ⟨x, z⟩\}) = \emptyset) \to \|\{⟨x, y⟩, ⟨x, z⟩\} \cup (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| = \|\{⟨x, y⟩, ⟨x, z⟩\}\| + \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\|$
148	145 146 147	mp3an13	$⊢ F ∖ \{⟨x, y⟩, ⟨x, z⟩\} \in Fin \to \|\{⟨x, y⟩, ⟨x, z⟩\} \cup (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| = \|\{⟨x, y⟩, ⟨x, z⟩\}\| + \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\|$
149	85 148	syl	$⊢ F \in Fin \to \|\{⟨x, y⟩, ⟨x, z⟩\} \cup (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| = \|\{⟨x, y⟩, ⟨x, z⟩\}\| + \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\|$
150	149	adantr	$⊢ (F \in Fin \land ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z)) \to \|\{⟨x, y⟩, ⟨x, z⟩\} \cup (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| = \|\{⟨x, y⟩, ⟨x, z⟩\}\| + \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\|$
151	108	fveq2d	$⊢ (⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to \|\{⟨x, y⟩, ⟨x, z⟩\} \cup (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| = \|F\|$
152	151	ad2antrl	$⊢ (F \in Fin \land ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z)) \to \|\{⟨x, y⟩, ⟨x, z⟩\} \cup (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| = \|F\|$
153		vex	$⊢ x \in V$
154	153 111	opth	$⊢ ⟨x, y⟩ = ⟨x, z⟩ \leftrightarrow (x = x \land y = z)$
155	154	simprbi	$⊢ ⟨x, y⟩ = ⟨x, z⟩ \to y = z$
156	155	necon3i	$⊢ y \neq z \to ⟨x, y⟩ \neq ⟨x, z⟩$
157		hashprg	$⊢ (⟨x, y⟩ \in V \land ⟨x, z⟩ \in V) \to (⟨x, y⟩ \neq ⟨x, z⟩ \leftrightarrow \|\{⟨x, y⟩, ⟨x, z⟩\}\| = 2)$
158	104 105 157	mp2an	$⊢ ⟨x, y⟩ \neq ⟨x, z⟩ \leftrightarrow \|\{⟨x, y⟩, ⟨x, z⟩\}\| = 2$
159	156 158	sylib	$⊢ y \neq z \to \|\{⟨x, y⟩, ⟨x, z⟩\}\| = 2$
160	159	oveq1d	$⊢ y \neq z \to \|\{⟨x, y⟩, ⟨x, z⟩\}\| + \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\| = 2 + \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\|$
161	160	ad2antll	$⊢ (F \in Fin \land ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z)) \to \|\{⟨x, y⟩, ⟨x, z⟩\}\| + \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\| = 2 + \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\|$
162	150 152 161	3eqtr3rd	$⊢ (F \in Fin \land ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z)) \to 2 + \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\| = \|F\|$
163	144 162	breqtrd	$⊢ (F \in Fin \land ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z)) \to 2 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \leq \|F\|$
164	83 93 96 131 163	ltletrd	$⊢ (F \in Fin \land ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z)) \to \|dom F\| < \|F\|$
165	83 164	gtned	$⊢ (F \in Fin \land ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z)) \to \|F\| \neq \|dom F\|$
166	165	ex	$⊢ F \in Fin \to (((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z) \to \|F\| \neq \|dom F\|)$
167	166	exlimdv	$⊢ F \in Fin \to (\exists z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z) \to \|F\| \neq \|dom F\|)$
168	167	exlimdvv	$⊢ F \in Fin \to (\exists x \exists y \exists z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z) \to \|F\| \neq \|dom F\|)$
169	82 168	syl5bi	$⊢ F \in Fin \to (\neg \forall x \forall y \forall z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z) \to \|F\| \neq \|dom F\|)$
170	169	necon4bd	$⊢ F \in Fin \to (\|F\| = \|dom F\| \to \forall x \forall y \forall z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z))$
171	170	imp	$⊢ (F \in Fin \land \|F\| = \|dom F\|) \to \forall x \forall y \forall z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z)$
172		dffun4	$⊢ Fun F \leftrightarrow (Rel F \land \forall x \forall y \forall z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z))$
173	72 171 172	sylanbrc	$⊢ (F \in Fin \land \|F\| = \|dom F\|) \to Fun F$
174	173	ex	$⊢ F \in Fin \to (\|F\| = \|dom F\| \to Fun F)$
175	3 174	impbid2	$⊢ F \in Fin \to (Fun F \leftrightarrow \|F\| = \|dom F\|)$

Metamath Proof Explorer

Theorem hashfun

Proof