Theorem hashfun 14401

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.)

Assertion

Ref	Expression
hashfun	⊢ (𝐹 ∈ Fin → (Fun 𝐹 ↔ (♯‘𝐹) = (♯‘dom 𝐹)))

Proof of Theorem hashfun

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		funfn 6577	. . 3 ⊢ (Fun 𝐹 ↔ 𝐹 Fn dom 𝐹)
2		hashfn 14339	. . 3 ⊢ (𝐹 Fn dom 𝐹 → (♯‘𝐹) = (♯‘dom 𝐹))
3	1, 2	sylbi 216	. 2 ⊢ (Fun 𝐹 → (♯‘𝐹) = (♯‘dom 𝐹))
4		dmfi 9332	. . . . . . . . . . 11 ⊢ (𝐹 ∈ Fin → dom 𝐹 ∈ Fin)
5		hashcl 14320	. . . . . . . . . . 11 ⊢ (dom 𝐹 ∈ Fin → (♯‘dom 𝐹) ∈ ℕ0)
6	4, 5	syl 17	. . . . . . . . . 10 ⊢ (𝐹 ∈ Fin → (♯‘dom 𝐹) ∈ ℕ0)
7	6	nn0red 12537	. . . . . . . . 9 ⊢ (𝐹 ∈ Fin → (♯‘dom 𝐹) ∈ ℝ)
8	7	adantr 479	. . . . . . . 8 ⊢ ((𝐹 ∈ Fin ∧ ¬ Rel 𝐹) → (♯‘dom 𝐹) ∈ ℝ)
9		df-rel 5682	. . . . . . . . . . . . 13 ⊢ (Rel 𝐹 ↔ 𝐹 ⊆ (V × V))
10		dfss3 3969	. . . . . . . . . . . . 13 ⊢ (𝐹 ⊆ (V × V) ↔ ∀𝑥 ∈ 𝐹 𝑥 ∈ (V × V))
11	9, 10	bitri 274	. . . . . . . . . . . 12 ⊢ (Rel 𝐹 ↔ ∀𝑥 ∈ 𝐹 𝑥 ∈ (V × V))
12	11	notbii 319	. . . . . . . . . . 11 ⊢ (¬ Rel 𝐹 ↔ ¬ ∀𝑥 ∈ 𝐹 𝑥 ∈ (V × V))
13		rexnal 3098	. . . . . . . . . . 11 ⊢ (∃𝑥 ∈ 𝐹 ¬ 𝑥 ∈ (V × V) ↔ ¬ ∀𝑥 ∈ 𝐹 𝑥 ∈ (V × V))
14	12, 13	bitr4i 277	. . . . . . . . . 10 ⊢ (¬ Rel 𝐹 ↔ ∃𝑥 ∈ 𝐹 ¬ 𝑥 ∈ (V × V))
15		dmun 5909	. . . . . . . . . . . . . . . 16 ⊢ dom ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥})
16	15	fveq2i 6893	. . . . . . . . . . . . . . 15 ⊢ (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘(dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}))
17		dmsnn0 6205	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (V × V) ↔ dom {𝑥} ≠ ∅)
18	17	biimpri 227	. . . . . . . . . . . . . . . . . . . 20 ⊢ (dom {𝑥} ≠ ∅ → 𝑥 ∈ (V × V))
19	18	necon1bi 2967	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑥 ∈ (V × V) → dom {𝑥} = ∅)
20	19	3ad2ant3 1133	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → dom {𝑥} = ∅)
21	20	uneq2d 4162	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}) = (dom (𝐹 ∖ {𝑥}) ∪ ∅))
22		un0 4389	. . . . . . . . . . . . . . . . 17 ⊢ (dom (𝐹 ∖ {𝑥}) ∪ ∅) = dom (𝐹 ∖ {𝑥})
23	21, 22	eqtrdi 2786	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}) = dom (𝐹 ∖ {𝑥}))
24	23	fveq2d 6894	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘(dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥})) = (♯‘dom (𝐹 ∖ {𝑥})))
25	16, 24	eqtrid 2782	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘dom (𝐹 ∖ {𝑥})))
26		diffi 9181	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ Fin → (𝐹 ∖ {𝑥}) ∈ Fin)
27		dmfi 9332	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹 ∖ {𝑥}) ∈ Fin → dom (𝐹 ∖ {𝑥}) ∈ Fin)
28	26, 27	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 ∈ Fin → dom (𝐹 ∖ {𝑥}) ∈ Fin)
29		hashcl 14320	. . . . . . . . . . . . . . . . . 18 ⊢ (dom (𝐹 ∖ {𝑥}) ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) ∈ ℕ0)
30	28, 29	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) ∈ ℕ0)
31	30	nn0red 12537	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) ∈ ℝ)
32		hashcl 14320	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∖ {𝑥}) ∈ Fin → (♯‘(𝐹 ∖ {𝑥})) ∈ ℕ0)
33	26, 32	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {𝑥})) ∈ ℕ0)
34	33	nn0red 12537	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {𝑥})) ∈ ℝ)
35		peano2re 11391	. . . . . . . . . . . . . . . . 17 ⊢ ((♯‘(𝐹 ∖ {𝑥})) ∈ ℝ → ((♯‘(𝐹 ∖ {𝑥})) + 1) ∈ ℝ)
36	34, 35	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ Fin → ((♯‘(𝐹 ∖ {𝑥})) + 1) ∈ ℝ)
37		fidomdm 9331	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∖ {𝑥}) ∈ Fin → dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥}))
38	26, 37	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ Fin → dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥}))
39		hashdom 14343	. . . . . . . . . . . . . . . . . 18 ⊢ ((dom (𝐹 ∖ {𝑥}) ∈ Fin ∧ (𝐹 ∖ {𝑥}) ∈ Fin) → ((♯‘dom (𝐹 ∖ {𝑥})) ≤ (♯‘(𝐹 ∖ {𝑥})) ↔ dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥})))
40	28, 26, 39	syl2anc 582	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ Fin → ((♯‘dom (𝐹 ∖ {𝑥})) ≤ (♯‘(𝐹 ∖ {𝑥})) ↔ dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥})))
41	38, 40	mpbird 256	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) ≤ (♯‘(𝐹 ∖ {𝑥})))
42	34	ltp1d 12148	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {𝑥})) < ((♯‘(𝐹 ∖ {𝑥})) + 1))
43	31, 34, 36, 41, 42	lelttrd 11376	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) < ((♯‘(𝐹 ∖ {𝑥})) + 1))
44	43	3ad2ant1 1131	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom (𝐹 ∖ {𝑥})) < ((♯‘(𝐹 ∖ {𝑥})) + 1))
45	25, 44	eqbrtrd 5169	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) < ((♯‘(𝐹 ∖ {𝑥})) + 1))
46		snfi 9046	. . . . . . . . . . . . . . . . 17 ⊢ {𝑥} ∈ Fin
47		disjdifr 4471	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ∖ {𝑥}) ∩ {𝑥}) = ∅
48		hashun 14346	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∖ {𝑥}) ∈ Fin ∧ {𝑥} ∈ Fin ∧ ((𝐹 ∖ {𝑥}) ∩ {𝑥}) = ∅) → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥})))
49	46, 47, 48	mp3an23 1451	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∖ {𝑥}) ∈ Fin → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥})))
50	26, 49	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ Fin → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥})))
51		hashsng 14333	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ V → (♯‘{𝑥}) = 1)
52	51	elv 3478	. . . . . . . . . . . . . . . 16 ⊢ (♯‘{𝑥}) = 1
53	52	oveq2i 7422	. . . . . . . . . . . . . . 15 ⊢ ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + 1)
54	50, 53	eqtr2di 2787	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ Fin → ((♯‘(𝐹 ∖ {𝑥})) + 1) = (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})))
55	54	3ad2ant1 1131	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → ((♯‘(𝐹 ∖ {𝑥})) + 1) = (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})))
56	45, 55	breqtrd 5173	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) < (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})))
57		difsnid 4812	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝐹 → ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = 𝐹)
58	57	dmeqd 5904	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐹 → dom ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = dom 𝐹)
59	58	fveq2d 6894	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐹 → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘dom 𝐹))
60	59	3ad2ant2 1132	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘dom 𝐹))
61	57	fveq2d 6894	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐹 → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘𝐹))
62	61	3ad2ant2 1132	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘𝐹))
63	56, 60, 62	3brtr3d 5178	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom 𝐹) < (♯‘𝐹))
64	63	rexlimdv3a 3157	. . . . . . . . . 10 ⊢ (𝐹 ∈ Fin → (∃𝑥 ∈ 𝐹 ¬ 𝑥 ∈ (V × V) → (♯‘dom 𝐹) < (♯‘𝐹)))
65	14, 64	biimtrid 241	. . . . . . . . 9 ⊢ (𝐹 ∈ Fin → (¬ Rel 𝐹 → (♯‘dom 𝐹) < (♯‘𝐹)))
66	65	imp 405	. . . . . . . 8 ⊢ ((𝐹 ∈ Fin ∧ ¬ Rel 𝐹) → (♯‘dom 𝐹) < (♯‘𝐹))
67	8, 66	gtned 11353	. . . . . . 7 ⊢ ((𝐹 ∈ Fin ∧ ¬ Rel 𝐹) → (♯‘𝐹) ≠ (♯‘dom 𝐹))
68	67	ex 411	. . . . . 6 ⊢ (𝐹 ∈ Fin → (¬ Rel 𝐹 → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
69	68	necon4bd 2958	. . . . 5 ⊢ (𝐹 ∈ Fin → ((♯‘𝐹) = (♯‘dom 𝐹) → Rel 𝐹))
70	69	imp 405	. . . 4 ⊢ ((𝐹 ∈ Fin ∧ (♯‘𝐹) = (♯‘dom 𝐹)) → Rel 𝐹)
71		2nalexn 1828	. . . . . . . 8 ⊢ (¬ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥∃𝑦 ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
72		df-ne 2939	. . . . . . . . . . . . 13 ⊢ (𝑦 ≠ 𝑧 ↔ ¬ 𝑦 = 𝑧)
73	72	anbi2i 621	. . . . . . . . . . . 12 ⊢ (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))
74		annim 402	. . . . . . . . . . . 12 ⊢ (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧) ↔ ¬ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
75	73, 74	bitri 274	. . . . . . . . . . 11 ⊢ (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) ↔ ¬ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
76	75	exbii 1848	. . . . . . . . . 10 ⊢ (∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) ↔ ∃𝑧 ¬ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
77		exnal 1827	. . . . . . . . . 10 ⊢ (∃𝑧 ¬ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
78	76, 77	bitr2i 275	. . . . . . . . 9 ⊢ (¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧))
79	78	2exbii 1849	. . . . . . . 8 ⊢ (∃𝑥∃𝑦 ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥∃𝑦∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧))
80	71, 79	bitri 274	. . . . . . 7 ⊢ (¬ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥∃𝑦∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧))
81	7	adantr 479	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘dom 𝐹) ∈ ℝ)
82		2re 12290	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℝ
83		diffi 9181	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ Fin → (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin)
84		dmfi 9332	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin)
85	83, 84	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ Fin → dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin)
86		hashcl 14320	. . . . . . . . . . . . . . . 16 ⊢ (dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℕ0)
87	85, 86	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℕ0)
88	87	nn0red 12537	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ)
89	88	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ)
90		readdcl 11195	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℝ ∧ (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
91	82, 89, 90	sylancr 585	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
92		hashcl 14320	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ Fin → (♯‘𝐹) ∈ ℕ0)
93	92	nn0red 12537	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ Fin → (♯‘𝐹) ∈ ℝ)
94	93	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘𝐹) ∈ ℝ)
95		1re 11218	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ
96		readdcl 11195	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℝ ∧ (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ) → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
97	95, 88, 96	sylancr 585	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ Fin → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
98	97	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
99	82, 88, 90	sylancr 585	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ Fin → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
100	99	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
101		opex 5463	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ⟨𝑥, 𝑦⟩ ∈ V
102		opex 5463	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ⟨𝑥, 𝑧⟩ ∈ V
103	101, 102	prss 4822	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ↔ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ⊆ 𝐹)
104		undif 4480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ⊆ 𝐹 ↔ ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = 𝐹)
105	103, 104	sylbb 218	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = 𝐹)
106	105	dmeqd 5904	. . . . . . . . . . . . . . . . . 18 ⊢ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → dom ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = dom 𝐹)
107		dmun 5909	. . . . . . . . . . . . . . . . . 18 ⊢ dom ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = (dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))
108	106, 107	eqtr3di 2785	. . . . . . . . . . . . . . . . 17 ⊢ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → dom 𝐹 = (dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
109		vex 3476	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑦 ∈ V
110		vex 3476	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑧 ∈ V
111	109, 110	dmprop 6215	. . . . . . . . . . . . . . . . . . 19 ⊢ dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} = {𝑥, 𝑥}
112		dfsn2 4640	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑥} = {𝑥, 𝑥}
113	111, 112	eqtr4i 2761	. . . . . . . . . . . . . . . . . 18 ⊢ dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} = {𝑥}
114	113	uneq1i 4158	. . . . . . . . . . . . . . . . 17 ⊢ (dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = ({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))
115	108, 114	eqtrdi 2786	. . . . . . . . . . . . . . . 16 ⊢ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → dom 𝐹 = ({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
116	115	fveq2d 6894	. . . . . . . . . . . . . . 15 ⊢ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (♯‘dom 𝐹) = (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
117	116	ad2antrl 724	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘dom 𝐹) = (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
118		hashun2 14347	. . . . . . . . . . . . . . . . 17 ⊢ (({𝑥} ∈ Fin ∧ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin) → (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ ((♯‘{𝑥}) + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
119	46, 85, 118	sylancr 585	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ Fin → (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ ((♯‘{𝑥}) + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
120	52	oveq1i 7421	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘{𝑥}) + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
121	119, 120	breqtrdi 5188	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ Fin → (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
122	121	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
123	117, 122	eqbrtrd 5169	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘dom 𝐹) ≤ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
124		1lt2 12387	. . . . . . . . . . . . . . 15 ⊢ 1 < 2
125		ltadd1 11685	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ) → (1 < 2 ↔ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
126	95, 82, 88, 125	mp3an12i 1463	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ Fin → (1 < 2 ↔ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
127	124, 126	mpbii 232	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ Fin → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
128	127	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
129	81, 98, 100, 123, 128	lelttrd 11376	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘dom 𝐹) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
130		fidomdm 9331	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ≼ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))
131	83, 130	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ Fin → dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ≼ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))
132		hashdom 14343	. . . . . . . . . . . . . . . . 17 ⊢ ((dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin ∧ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin) → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ≼ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
133	85, 83, 132	syl2anc 582	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ Fin → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ≼ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
134	131, 133	mpbird 256	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
135		hashcl 14320	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℕ0)
136	83, 135	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℕ0)
137	136	nn0red 12537	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ)
138		leadd2 11687	. . . . . . . . . . . . . . . . 17 ⊢ (((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ ∧ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ ∧ 2 ∈ ℝ) → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
139	82, 138	mp3an3 1448	. . . . . . . . . . . . . . . 16 ⊢ (((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ ∧ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ) → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
140	88, 137, 139	syl2anc 582	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ Fin → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
141	134, 140	mpbid 231	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ Fin → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
142	141	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
143		prfi 9324	. . . . . . . . . . . . . . . . 17 ⊢ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∈ Fin
144		disjdif 4470	. . . . . . . . . . . . . . . . 17 ⊢ ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∩ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = ∅
145		hashun 14346	. . . . . . . . . . . . . . . . 17 ⊢ (({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∈ Fin ∧ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin ∧ ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∩ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = ∅) → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
146	143, 144, 145	mp3an13 1450	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
147	83, 146	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ Fin → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
148	147	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
149	105	fveq2d 6894	. . . . . . . . . . . . . . 15 ⊢ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (♯‘𝐹))
150	149	ad2antrl 724	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (♯‘𝐹))
151		vex 3476	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑥 ∈ V
152	151, 109	opth 5475	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑧⟩ ↔ (𝑥 = 𝑥 ∧ 𝑦 = 𝑧))
153	152	simprbi 495	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑧⟩ → 𝑦 = 𝑧)
154	153	necon3i 2971	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ≠ 𝑧 → ⟨𝑥, 𝑦⟩ ≠ ⟨𝑥, 𝑧⟩)
155		hashprg 14359	. . . . . . . . . . . . . . . . . 18 ⊢ ((⟨𝑥, 𝑦⟩ ∈ V ∧ ⟨𝑥, 𝑧⟩ ∈ V) → (⟨𝑥, 𝑦⟩ ≠ ⟨𝑥, 𝑧⟩ ↔ (♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) = 2))
156	101, 102, 155	mp2an 688	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑥, 𝑦⟩ ≠ ⟨𝑥, 𝑧⟩ ↔ (♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) = 2)
157	154, 156	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ≠ 𝑧 → (♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) = 2)
158	157	oveq1d 7426	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ≠ 𝑧 → ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
159	158	ad2antll 725	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
160	148, 150, 159	3eqtr3rd 2779	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (♯‘𝐹))
161	142, 160	breqtrd 5173	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (♯‘𝐹))
162	81, 91, 94, 129, 161	ltletrd 11378	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘dom 𝐹) < (♯‘𝐹))
163	81, 162	gtned 11353	. . . . . . . . . 10 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘𝐹) ≠ (♯‘dom 𝐹))
164	163	ex 411	. . . . . . . . 9 ⊢ (𝐹 ∈ Fin → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
165	164	exlimdv 1934	. . . . . . . 8 ⊢ (𝐹 ∈ Fin → (∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
166	165	exlimdvv 1935	. . . . . . 7 ⊢ (𝐹 ∈ Fin → (∃𝑥∃𝑦∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
167	80, 166	biimtrid 241	. . . . . 6 ⊢ (𝐹 ∈ Fin → (¬ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
168	167	necon4bd 2958	. . . . 5 ⊢ (𝐹 ∈ Fin → ((♯‘𝐹) = (♯‘dom 𝐹) → ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
169	168	imp 405	. . . 4 ⊢ ((𝐹 ∈ Fin ∧ (♯‘𝐹) = (♯‘dom 𝐹)) → ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
170		dffun4 6558	. . . 4 ⊢ (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
171	70, 169, 170	sylanbrc 581	. . 3 ⊢ ((𝐹 ∈ Fin ∧ (♯‘𝐹) = (♯‘dom 𝐹)) → Fun 𝐹)
172	171	ex 411	. 2 ⊢ (𝐹 ∈ Fin → ((♯‘𝐹) = (♯‘dom 𝐹) → Fun 𝐹))
173	3, 172	impbid2 225	1 ⊢ (𝐹 ∈ Fin → (Fun 𝐹 ↔ (♯‘𝐹) = (♯‘dom 𝐹)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1085  ∀wal 1537   = wceq 1539  ∃wex 1779   ∈ wcel 2104   ≠ wne 2938  ∀wral 3059  ∃wrex 3068  Vcvv 3472   ∖ cdif 3944   ∪ cun 3945   ∩ cin 3946   ⊆ wss 3947  ∅c0 4321  {csn 4627  {cpr 4629  ⟨cop 4633   class class class wbr 5147   × cxp 5673  dom cdm 5675  Rel wrel 5680  Fun wfun 6536   Fn wfn 6537  ‘cfv 6542  (class class class)co 7411   ≼ cdom 8939  Fincfn 8941  ℝcr 11111  1c1 11113   + caddc 11115   < clt 11252   ≤ cle 11253  2c2 12271  ℕ₀cn0 12476  ♯chash 14294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-oadd 8472  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-dju 9898  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-nn 12217  df-2 12279  df-n0 12477  df-xnn0 12549  df-z 12563  df-uz 12827  df-fz 13489  df-hash 14295

This theorem is referenced by:  hashres  14402  hashreshashfun  14403  hashfundm  14406  ccatalpha  14547  cycpmconjslem2  32584