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	eqtrdi	$⊢ (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	eqtrid	$⊢ (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		disjdifr	$⊢ (F ∖ \{x\}) \cap \{x\} = \emptyset$
48		hashun	$⊢ (F ∖ \{x\} \in Fin \land \{x\} \in Fin \land (F ∖ \{x\}) \cap \{x\} = \emptyset) \to \|(F ∖ \{x\}) \cup \{x\}\| = \|F ∖ \{x\}\| + \|\{x\}\|$
49	46 47 48	mp3an23	$⊢ F ∖ \{x\} \in Fin \to \|(F ∖ \{x\}) \cup \{x\}\| = \|F ∖ \{x\}\| + \|\{x\}\|$
50	26 49	syl	$⊢ F \in Fin \to \|(F ∖ \{x\}) \cup \{x\}\| = \|F ∖ \{x\}\| + \|\{x\}\|$
51		hashsng	$⊢ x \in V \to \|\{x\}\| = 1$
52	51	elv	$⊢ \|\{x\}\| = 1$
53	52	oveq2i	$⊢ \|F ∖ \{x\}\| + \|\{x\}\| = \|F ∖ \{x\}\| + 1$
54	50 53	eqtr2di	$⊢ F \in Fin \to \|F ∖ \{x\}\| + 1 = \|(F ∖ \{x\}) \cup \{x\}\|$
55	54	3ad2ant1	$⊢ (F \in Fin \land x \in F \land \neg x \in (V \times V)) \to \|F ∖ \{x\}\| + 1 = \|(F ∖ \{x\}) \cup \{x\}\|$
56	45 55	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\}\|$
57		difsnid	$⊢ x \in F \to (F ∖ \{x\}) \cup \{x\} = F$
58	57	dmeqd	$⊢ x \in F \to dom ((F ∖ \{x\}) \cup \{x\}) = dom F$
59	58	fveq2d	$⊢ x \in F \to \|dom ((F ∖ \{x\}) \cup \{x\})\| = \|dom F\|$
60	59	3ad2ant2	$⊢ (F \in Fin \land x \in F \land \neg x \in (V \times V)) \to \|dom ((F ∖ \{x\}) \cup \{x\})\| = \|dom F\|$
61	57	fveq2d	$⊢ x \in F \to \|(F ∖ \{x\}) \cup \{x\}\| = \|F\|$
62	61	3ad2ant2	$⊢ (F \in Fin \land x \in F \land \neg x \in (V \times V)) \to \|(F ∖ \{x\}) \cup \{x\}\| = \|F\|$
63	56 60 62	3brtr3d	$⊢ (F \in Fin \land x \in F \land \neg x \in (V \times V)) \to \|dom F\| < \|F\|$
64	63	rexlimdv3a	$⊢ F \in Fin \to (\exists x \in F \neg x \in (V \times V) \to \|dom F\| < \|F\|)$
65	14 64	syl5bi	$⊢ F \in Fin \to (\neg Rel F \to \|dom F\| < \|F\|)$
66	65	imp	$⊢ (F \in Fin \land \neg Rel F) \to \|dom F\| < \|F\|$
67	8 66	gtned	$⊢ (F \in Fin \land \neg Rel F) \to \|F\| \neq \|dom F\|$
68	67	ex	$⊢ F \in Fin \to (\neg Rel F \to \|F\| \neq \|dom F\|)$
69	68	necon4bd	$⊢ F \in Fin \to (\|F\| = \|dom F\| \to Rel F)$
70	69	imp	$⊢ (F \in Fin \land \|F\| = \|dom F\|) \to Rel F$
71		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)$
72		df-ne	$⊢ y \neq z \leftrightarrow \neg y = z$
73	72	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)$
74		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)$
75	73 74	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)$
76	75	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)$
77		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)$
78	76 77	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)$
79	78	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)$
80	71 79	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)$
81	7	adantr	$⊢ (F \in Fin \land ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z)) \to \|dom F\| \in ℝ$
82		2re	$⊢ 2 \in ℝ$
83		diffi	$⊢ F \in Fin \to F ∖ \{⟨x, y⟩, ⟨x, z⟩\} \in Fin$
84		dmfi	$⊢ F ∖ \{⟨x, y⟩, ⟨x, z⟩\} \in Fin \to dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\}) \in Fin$
85	83 84	syl	$⊢ F \in Fin \to dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\}) \in Fin$
86		hashcl	$⊢ dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\}) \in Fin \to \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \in ℕ_{0}$
87	85 86	syl	$⊢ F \in Fin \to \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \in ℕ_{0}$
88	87	nn0red	$⊢ F \in Fin \to \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \in ℝ$
89	88	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 ℝ$
90		readdcl	$⊢ (2 \in ℝ \land \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \in ℝ) \to 2 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \in ℝ$
91	82 89 90	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 ℝ$
92		hashcl	$⊢ F \in Fin \to \|F\| \in ℕ_{0}$
93	92	nn0red	$⊢ F \in Fin \to \|F\| \in ℝ$
94	93	adantr	$⊢ (F \in Fin \land ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z)) \to \|F\| \in ℝ$
95		1re	$⊢ 1 \in ℝ$
96		readdcl	$⊢ (1 \in ℝ \land \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \in ℝ) \to 1 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \in ℝ$
97	95 88 96	sylancr	$⊢ F \in Fin \to 1 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \in ℝ$
98	97	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 ℝ$
99	82 88 90	sylancr	$⊢ F \in Fin \to 2 + \|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 2 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \in ℝ$
101		opex	$⊢ ⟨x, y⟩ \in V$
102		opex	$⊢ ⟨x, z⟩ \in V$
103	101 102	prss	$⊢ (⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \leftrightarrow \{⟨x, y⟩, ⟨x, z⟩\} \subseteq F$
104		undif	$⊢ \{⟨x, y⟩, ⟨x, z⟩\} \subseteq F \leftrightarrow \{⟨x, y⟩, ⟨x, z⟩\} \cup (F ∖ \{⟨x, y⟩, ⟨x, z⟩\}) = F$
105	103 104	sylbb	$⊢ (⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to \{⟨x, y⟩, ⟨x, z⟩\} \cup (F ∖ \{⟨x, y⟩, ⟨x, z⟩\}) = F$
106	105	dmeqd	$⊢ (⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to dom (\{⟨x, y⟩, ⟨x, z⟩\} \cup (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})) = dom F$
107		dmun	$⊢ dom (\{⟨x, y⟩, ⟨x, z⟩\} \cup (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})) = dom \{⟨x, y⟩, ⟨x, z⟩\} \cup dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})$
108	106 107	eqtr3di	$⊢ (⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to dom F = dom \{⟨x, y⟩, ⟨x, z⟩\} \cup dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})$
109		vex	$⊢ y \in V$
110		vex	$⊢ z \in V$
111	109 110	dmprop	$⊢ dom \{⟨x, y⟩, ⟨x, z⟩\} = \{x, x\}$
112		dfsn2	$⊢ \{x\} = \{x, x\}$
113	111 112	eqtr4i	$⊢ dom \{⟨x, y⟩, ⟨x, z⟩\} = \{x\}$
114	113	uneq1i	$⊢ dom \{⟨x, y⟩, ⟨x, z⟩\} \cup dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\}) = \{x\} \cup dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})$
115	108 114	eqtrdi	$⊢ (⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to dom F = \{x\} \cup dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})$
116	115	fveq2d	$⊢ (⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to \|dom F\| = \|\{x\} \cup dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\|$
117	116	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⟩\})\|$
118		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⟩\})\|$
119	46 85 118	sylancr	$⊢ F \in Fin \to \|\{x\} \cup dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \leq \|\{x\}\| + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\|$
120	52	oveq1i	$⊢ \|\{x\}\| + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| = 1 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\|$
121	119 120	breqtrdi	$⊢ F \in Fin \to \|\{x\} \cup dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \leq 1 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\|$
122	121	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⟩\})\|$
123	117 122	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⟩\})\|$
124		1lt2	$⊢ 1 < 2$
125		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⟩\})\|)$
126	95 82 88 125	mp3an12i	$⊢ F \in Fin \to (1 < 2 \leftrightarrow 1 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| < 2 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\|)$
127	124 126	mpbii	$⊢ F \in Fin \to 1 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| < 2 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\|$
128	127	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⟩\})\|$
129	81 98 100 123 128	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⟩\})\|$
130		fidomdm	$⊢ F ∖ \{⟨x, y⟩, ⟨x, z⟩\} \in Fin \to dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\}) ≼ (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})$
131	83 130	syl	$⊢ F \in Fin \to dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\}) ≼ (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})$
132		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⟩\}))$
133	85 83 132	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⟩\}))$
134	131 133	mpbird	$⊢ F \in Fin \to \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \leq \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\|$
135		hashcl	$⊢ F ∖ \{⟨x, y⟩, ⟨x, z⟩\} \in Fin \to \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\| \in ℕ_{0}$
136	83 135	syl	$⊢ F \in Fin \to \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\| \in ℕ_{0}$
137	136	nn0red	$⊢ F \in Fin \to \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\| \in ℝ$
138		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⟩\}\|)$
139	82 138	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⟩\}\|)$
140	88 137 139	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⟩\}\|)$
141	134 140	mpbid	$⊢ F \in Fin \to 2 + \|dom (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| \leq 2 + \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\|$
142	141	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⟩\}\|$
143		prfi	$⊢ \{⟨x, y⟩, ⟨x, z⟩\} \in Fin$
144		disjdif	$⊢ \{⟨x, y⟩, ⟨x, z⟩\} \cap (F ∖ \{⟨x, y⟩, ⟨x, z⟩\}) = \emptyset$
145		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⟩\}\|$
146	143 144 145	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⟩\}\|$
147	83 146	syl	$⊢ F \in Fin \to \|\{⟨x, y⟩, ⟨x, z⟩\} \cup (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| = \|\{⟨x, y⟩, ⟨x, z⟩\}\| + \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\|$
148	147	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⟩\}\|$
149	105	fveq2d	$⊢ (⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to \|\{⟨x, y⟩, ⟨x, z⟩\} \cup (F ∖ \{⟨x, y⟩, ⟨x, z⟩\})\| = \|F\|$
150	149	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\|$
151		vex	$⊢ x \in V$
152	151 109	opth	$⊢ ⟨x, y⟩ = ⟨x, z⟩ \leftrightarrow (x = x \land y = z)$
153	152	simprbi	$⊢ ⟨x, y⟩ = ⟨x, z⟩ \to y = z$
154	153	necon3i	$⊢ y \neq z \to ⟨x, y⟩ \neq ⟨x, z⟩$
155		hashprg	$⊢ (⟨x, y⟩ \in V \land ⟨x, z⟩ \in V) \to (⟨x, y⟩ \neq ⟨x, z⟩ \leftrightarrow \|\{⟨x, y⟩, ⟨x, z⟩\}\| = 2)$
156	101 102 155	mp2an	$⊢ ⟨x, y⟩ \neq ⟨x, z⟩ \leftrightarrow \|\{⟨x, y⟩, ⟨x, z⟩\}\| = 2$
157	154 156	sylib	$⊢ y \neq z \to \|\{⟨x, y⟩, ⟨x, z⟩\}\| = 2$
158	157	oveq1d	$⊢ y \neq z \to \|\{⟨x, y⟩, ⟨x, z⟩\}\| + \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\| = 2 + \|F ∖ \{⟨x, y⟩, ⟨x, z⟩\}\|$
159	158	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⟩\}\|$
160	148 150 159	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\|$
161	142 160	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\|$
162	81 91 94 129 161	ltletrd	$⊢ (F \in Fin \land ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z)) \to \|dom F\| < \|F\|$
163	81 162	gtned	$⊢ (F \in Fin \land ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z)) \to \|F\| \neq \|dom F\|$
164	163	ex	$⊢ F \in Fin \to (((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \land y \neq z) \to \|F\| \neq \|dom F\|)$
165	164	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\|)$
166	165	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\|)$
167	80 166	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\|)$
168	167	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))$
169	168	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)$
170		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))$
171	70 169 170	sylanbrc	$⊢ (F \in Fin \land \|F\| = \|dom F\|) \to Fun F$
172	171	ex	$⊢ F \in Fin \to (\|F\| = \|dom F\| \to Fun F)$
173	3 172	impbid2	$⊢ F \in Fin \to (Fun F \leftrightarrow \|F\| = \|dom F\|)$

Metamath Proof Explorer

Theorem hashfun

Proof