Theorem hashfun 14470

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 6564	. . 3 ⊢ (Fun 𝐹 ↔ 𝐹 Fn dom 𝐹)
2		hashfn 14407	. . 3 ⊢ (𝐹 Fn dom 𝐹 → (♯‘𝐹) = (♯‘dom 𝐹))
3	1, 2	sylbi 220	. 2 ⊢ (Fun 𝐹 → (♯‘𝐹) = (♯‘dom 𝐹))
4		dmfi 9288	. . . . . . . . . . 11 ⊢ (𝐹 ∈ Fin → dom 𝐹 ∈ Fin)
5		hashcl 14388	. . . . . . . . . . 11 ⊢ (dom 𝐹 ∈ Fin → (♯‘dom 𝐹) ∈ ℕ0)
6	4, 5	syl 18	. . . . . . . . . 10 ⊢ (𝐹 ∈ Fin → (♯‘dom 𝐹) ∈ ℕ0)
7	6	nn0red 12562	. . . . . . . . 9 ⊢ (𝐹 ∈ Fin → (♯‘dom 𝐹) ∈ ℝ)
8	7	adantr 485	. . . . . . . 8 ⊢ ((𝐹 ∈ Fin ∧ ¬ Rel 𝐹) → (♯‘dom 𝐹) ∈ ℝ)
9		df-rel 5666	. . . . . . . . . . . . 13 ⊢ (Rel 𝐹 ↔ 𝐹 ⊆ (V × V))
10		dfss3 3934	. . . . . . . . . . . . 13 ⊢ (𝐹 ⊆ (V × V) ↔ ∀𝑥 ∈ 𝐹 𝑥 ∈ (V × V))
11	9, 10	bitri 278	. . . . . . . . . . . 12 ⊢ (Rel 𝐹 ↔ ∀𝑥 ∈ 𝐹 𝑥 ∈ (V × V))
12	11	notbii 323	. . . . . . . . . . 11 ⊢ (¬ Rel 𝐹 ↔ ¬ ∀𝑥 ∈ 𝐹 𝑥 ∈ (V × V))
13		rexnal 3123	. . . . . . . . . . 11 ⊢ (∃𝑥 ∈ 𝐹 ¬ 𝑥 ∈ (V × V) ↔ ¬ ∀𝑥 ∈ 𝐹 𝑥 ∈ (V × V))
14	12, 13	bitr4i 281	. . . . . . . . . 10 ⊢ (¬ Rel 𝐹 ↔ ∃𝑥 ∈ 𝐹 ¬ 𝑥 ∈ (V × V))
15		dmun 5898	. . . . . . . . . . . . . . . 16 ⊢ dom ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥})
16	15	fveq2i 6882	. . . . . . . . . . . . . . 15 ⊢ (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘(dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}))
17		dmsnn0 6206	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (V × V) ↔ dom {𝑥} ≠ ∅)
18	17	biimpri 231	. . . . . . . . . . . . . . . . . . . 20 ⊢ (dom {𝑥} ≠ ∅ → 𝑥 ∈ (V × V))
19	18	necon1bi 2992	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑥 ∈ (V × V) → dom {𝑥} = ∅)
20	19	3ad2ant3 1151	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → dom {𝑥} = ∅)
21	20	uneq2d 4130	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}) = (dom (𝐹 ∖ {𝑥}) ∪ ∅))
22		un0 4357	. . . . . . . . . . . . . . . . 17 ⊢ (dom (𝐹 ∖ {𝑥}) ∪ ∅) = dom (𝐹 ∖ {𝑥})
23	21, 22	eqtrdi 2820	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}) = dom (𝐹 ∖ {𝑥}))
24	23	fveq2d 6883	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘(dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥})) = (♯‘dom (𝐹 ∖ {𝑥})))
25	16, 24	eqtrid 2816	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘dom (𝐹 ∖ {𝑥})))
26		diffi 9155	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ Fin → (𝐹 ∖ {𝑥}) ∈ Fin)
27		dmfi 9288	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹 ∖ {𝑥}) ∈ Fin → dom (𝐹 ∖ {𝑥}) ∈ Fin)
28	26, 27	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 ∈ Fin → dom (𝐹 ∖ {𝑥}) ∈ Fin)
29		hashcl 14388	. . . . . . . . . . . . . . . . . 18 ⊢ (dom (𝐹 ∖ {𝑥}) ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) ∈ ℕ0)
30	28, 29	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) ∈ ℕ0)
31	30	nn0red 12562	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) ∈ ℝ)
32		hashcl 14388	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∖ {𝑥}) ∈ Fin → (♯‘(𝐹 ∖ {𝑥})) ∈ ℕ0)
33	26, 32	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {𝑥})) ∈ ℕ0)
34	33	nn0red 12562	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {𝑥})) ∈ ℝ)
35		peano2re 11379	. . . . . . . . . . . . . . . . 17 ⊢ ((♯‘(𝐹 ∖ {𝑥})) ∈ ℝ → ((♯‘(𝐹 ∖ {𝑥})) + 1) ∈ ℝ)
36	34, 35	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ Fin → ((♯‘(𝐹 ∖ {𝑥})) + 1) ∈ ℝ)
37		fidomdm 9287	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∖ {𝑥}) ∈ Fin → dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥}))
38	26, 37	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ Fin → dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥}))
39		hashdom 14411	. . . . . . . . . . . . . . . . . 18 ⊢ ((dom (𝐹 ∖ {𝑥}) ∈ Fin ∧ (𝐹 ∖ {𝑥}) ∈ Fin) → ((♯‘dom (𝐹 ∖ {𝑥})) ≤ (♯‘(𝐹 ∖ {𝑥})) ↔ dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥})))
40	28, 26, 39	syl2anc 595	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ Fin → ((♯‘dom (𝐹 ∖ {𝑥})) ≤ (♯‘(𝐹 ∖ {𝑥})) ↔ dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥})))
41	38, 40	mpbird 260	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) ≤ (♯‘(𝐹 ∖ {𝑥})))
42	34	ltp1d 12141	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {𝑥})) < ((♯‘(𝐹 ∖ {𝑥})) + 1))
43	31, 34, 36, 41, 42	lelttrd 11364	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) < ((♯‘(𝐹 ∖ {𝑥})) + 1))
44	43	3ad2ant1 1149	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom (𝐹 ∖ {𝑥})) < ((♯‘(𝐹 ∖ {𝑥})) + 1))
45	25, 44	eqbrtrd 5134	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) < ((♯‘(𝐹 ∖ {𝑥})) + 1))
46		snfi 9036	. . . . . . . . . . . . . . . . 17 ⊢ {𝑥} ∈ Fin
47		disjdifr 4436	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ∖ {𝑥}) ∩ {𝑥}) = ∅
48		hashun 14414	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∖ {𝑥}) ∈ Fin ∧ {𝑥} ∈ Fin ∧ ((𝐹 ∖ {𝑥}) ∩ {𝑥}) = ∅) → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥})))
49	46, 47, 48	mp3an23 1479	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∖ {𝑥}) ∈ Fin → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥})))
50	26, 49	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ Fin → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥})))
51		hashsng 14401	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ V → (♯‘{𝑥}) = 1)
52	51	elv 3468	. . . . . . . . . . . . . . . 16 ⊢ (♯‘{𝑥}) = 1
53	52	oveq2i 7419	. . . . . . . . . . . . . . 15 ⊢ ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + 1)
54	50, 53	eqtr2di 2821	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ Fin → ((♯‘(𝐹 ∖ {𝑥})) + 1) = (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})))
55	54	3ad2ant1 1149	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → ((♯‘(𝐹 ∖ {𝑥})) + 1) = (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})))
56	45, 55	breqtrd 5138	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) < (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})))
57		difsnid 4777	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝐹 → ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = 𝐹)
58	57	dmeqd 5893	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐹 → dom ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = dom 𝐹)
59	58	fveq2d 6883	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐹 → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘dom 𝐹))
60	59	3ad2ant2 1150	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘dom 𝐹))
61	57	fveq2d 6883	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐹 → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘𝐹))
62	61	3ad2ant2 1150	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘𝐹))
63	56, 60, 62	3brtr3d 5143	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom 𝐹) < (♯‘𝐹))
64	63	rexlimdv3a 3176	. . . . . . . . . 10 ⊢ (𝐹 ∈ Fin → (∃𝑥 ∈ 𝐹 ¬ 𝑥 ∈ (V × V) → (♯‘dom 𝐹) < (♯‘𝐹)))
65	14, 64	biimtrid 245	. . . . . . . . 9 ⊢ (𝐹 ∈ Fin → (¬ Rel 𝐹 → (♯‘dom 𝐹) < (♯‘𝐹)))
66	65	imp 411	. . . . . . . 8 ⊢ ((𝐹 ∈ Fin ∧ ¬ Rel 𝐹) → (♯‘dom 𝐹) < (♯‘𝐹))
67	8, 66	gtned 11341	. . . . . . 7 ⊢ ((𝐹 ∈ Fin ∧ ¬ Rel 𝐹) → (♯‘𝐹) ≠ (♯‘dom 𝐹))
68	67	ex 417	. . . . . 6 ⊢ (𝐹 ∈ Fin → (¬ Rel 𝐹 → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
69	68	necon4bd 2984	. . . . 5 ⊢ (𝐹 ∈ Fin → ((♯‘𝐹) = (♯‘dom 𝐹) → Rel 𝐹))
70	69	imp 411	. . . 4 ⊢ ((𝐹 ∈ Fin ∧ (♯‘𝐹) = (♯‘dom 𝐹)) → Rel 𝐹)
71		2nalexn 1855	. . . . . . . 8 ⊢ (¬ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥∃𝑦 ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
72		df-ne 2965	. . . . . . . . . . . . 13 ⊢ (𝑦 ≠ 𝑧 ↔ ¬ 𝑦 = 𝑧)
73	72	anbi2i 634	. . . . . . . . . . . 12 ⊢ (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))
74		annim 408	. . . . . . . . . . . 12 ⊢ (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧) ↔ ¬ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
75	73, 74	bitri 278	. . . . . . . . . . 11 ⊢ (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) ↔ ¬ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
76	75	exbii 1875	. . . . . . . . . 10 ⊢ (∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) ↔ ∃𝑧 ¬ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
77		exnal 1854	. . . . . . . . . 10 ⊢ (∃𝑧 ¬ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
78	76, 77	bitr2i 279	. . . . . . . . 9 ⊢ (¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧))
79	78	2exbii 1876	. . . . . . . 8 ⊢ (∃𝑥∃𝑦 ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥∃𝑦∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧))
80	71, 79	bitri 278	. . . . . . 7 ⊢ (¬ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥∃𝑦∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧))
81	7	adantr 485	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘dom 𝐹) ∈ ℝ)
82		2re 12311	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℝ
83		diffi 9155	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ Fin → (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin)
84		dmfi 9288	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin)
85	83, 84	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ Fin → dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin)
86		hashcl 14388	. . . . . . . . . . . . . . . 16 ⊢ (dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℕ0)
87	85, 86	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℕ0)
88	87	nn0red 12562	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ)
89	88	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ)
90		readdcl 11179	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℝ ∧ (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
91	82, 89, 90	sylancr 598	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
92		hashcl 14388	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ Fin → (♯‘𝐹) ∈ ℕ0)
93	92	nn0red 12562	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ Fin → (♯‘𝐹) ∈ ℝ)
94	93	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘𝐹) ∈ ℝ)
95		1re 11204	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ
96		readdcl 11179	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℝ ∧ (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ) → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
97	95, 88, 96	sylancr 598	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ Fin → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
98	97	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
99	82, 88, 90	sylancr 598	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ Fin → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
100	99	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
101		opex 5443	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ⟨𝑥, 𝑦⟩ ∈ V
102		opex 5443	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ⟨𝑥, 𝑧⟩ ∈ V
103	101, 102	prss 4787	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ↔ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ⊆ 𝐹)
104		undif 4445	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ⊆ 𝐹 ↔ ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = 𝐹)
105	103, 104	sylbb 222	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = 𝐹)
106	105	dmeqd 5893	. . . . . . . . . . . . . . . . . 18 ⊢ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → dom ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = dom 𝐹)
107		dmun 5898	. . . . . . . . . . . . . . . . . 18 ⊢ dom ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = (dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))
108	106, 107	eqtr3di 2819	. . . . . . . . . . . . . . . . 17 ⊢ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → dom 𝐹 = (dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
109		vex 3467	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑦 ∈ V
110		vex 3467	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑧 ∈ V
111	109, 110	dmprop 6216	. . . . . . . . . . . . . . . . . . 19 ⊢ dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} = {𝑥, 𝑥}
112		dfsn2 4604	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑥} = {𝑥, 𝑥}
113	111, 112	eqtr4i 2795	. . . . . . . . . . . . . . . . . 18 ⊢ dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} = {𝑥}
114	113	uneq1i 4126	. . . . . . . . . . . . . . . . 17 ⊢ (dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = ({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))
115	108, 114	eqtrdi 2820	. . . . . . . . . . . . . . . 16 ⊢ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → dom 𝐹 = ({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
116	115	fveq2d 6883	. . . . . . . . . . . . . . 15 ⊢ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (♯‘dom 𝐹) = (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
117	116	ad2antrl 740	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘dom 𝐹) = (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
118		hashun2 14415	. . . . . . . . . . . . . . . . 17 ⊢ (({𝑥} ∈ Fin ∧ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin) → (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ ((♯‘{𝑥}) + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
119	46, 85, 118	sylancr 598	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ Fin → (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ ((♯‘{𝑥}) + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
120	52	oveq1i 7418	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘{𝑥}) + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
121	119, 120	breqtrdi 5153	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ Fin → (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
122	121	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
123	117, 122	eqbrtrd 5134	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘dom 𝐹) ≤ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
124		1lt2 12409	. . . . . . . . . . . . . . 15 ⊢ 1 < 2
125		ltadd1 11677	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ) → (1 < 2 ↔ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
126	95, 82, 88, 125	mp3an12i 1491	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ Fin → (1 < 2 ↔ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
127	124, 126	mpbii 236	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ Fin → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
128	127	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
129	81, 98, 100, 123, 128	lelttrd 11364	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘dom 𝐹) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
130		fidomdm 9287	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ≼ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))
131	83, 130	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ Fin → dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ≼ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))
132		hashdom 14411	. . . . . . . . . . . . . . . . 17 ⊢ ((dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin ∧ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin) → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ≼ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
133	85, 83, 132	syl2anc 595	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ Fin → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ≼ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
134	131, 133	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
135		hashcl 14388	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℕ0)
136	83, 135	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℕ0)
137	136	nn0red 12562	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ)
138		leadd2 11679	. . . . . . . . . . . . . . . . 17 ⊢ (((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ ∧ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ ∧ 2 ∈ ℝ) → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
139	82, 138	mp3an3 1476	. . . . . . . . . . . . . . . 16 ⊢ (((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ ∧ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ) → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
140	88, 137, 139	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ Fin → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
141	134, 140	mpbid 235	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ Fin → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
142	141	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
143		prfi 9279	. . . . . . . . . . . . . . . . 17 ⊢ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∈ Fin
144		disjdif 4435	. . . . . . . . . . . . . . . . 17 ⊢ ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∩ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = ∅
145		hashun 14414	. . . . . . . . . . . . . . . . 17 ⊢ (({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∈ Fin ∧ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin ∧ ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∩ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = ∅) → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
146	143, 144, 145	mp3an13 1478	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
147	83, 146	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ Fin → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
148	147	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
149	105	fveq2d 6883	. . . . . . . . . . . . . . 15 ⊢ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (♯‘𝐹))
150	149	ad2antrl 740	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (♯‘𝐹))
151		vex 3467	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑥 ∈ V
152	151, 109	opth 5456	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑧⟩ ↔ (𝑥 = 𝑥 ∧ 𝑦 = 𝑧))
153	152	simprbi 502	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑧⟩ → 𝑦 = 𝑧)
154	153	necon3i 2996	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ≠ 𝑧 → ⟨𝑥, 𝑦⟩ ≠ ⟨𝑥, 𝑧⟩)
155		hashprg 14427	. . . . . . . . . . . . . . . . . 18 ⊢ ((⟨𝑥, 𝑦⟩ ∈ V ∧ ⟨𝑥, 𝑧⟩ ∈ V) → (⟨𝑥, 𝑦⟩ ≠ ⟨𝑥, 𝑧⟩ ↔ (♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) = 2))
156	101, 102, 155	mp2an 704	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑥, 𝑦⟩ ≠ ⟨𝑥, 𝑧⟩ ↔ (♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) = 2)
157	154, 156	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ≠ 𝑧 → (♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) = 2)
158	157	oveq1d 7423	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ≠ 𝑧 → ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
159	158	ad2antll 741	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
160	148, 150, 159	3eqtr3rd 2813	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (♯‘𝐹))
161	142, 160	breqtrd 5138	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (♯‘𝐹))
162	81, 91, 94, 129, 161	ltletrd 11366	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘dom 𝐹) < (♯‘𝐹))
163	81, 162	gtned 11341	. . . . . . . . . 10 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘𝐹) ≠ (♯‘dom 𝐹))
164	163	ex 417	. . . . . . . . 9 ⊢ (𝐹 ∈ Fin → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
165	164	exlimdv 1960	. . . . . . . 8 ⊢ (𝐹 ∈ Fin → (∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
166	165	exlimdvv 1961	. . . . . . 7 ⊢ (𝐹 ∈ Fin → (∃𝑥∃𝑦∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
167	80, 166	biimtrid 245	. . . . . 6 ⊢ (𝐹 ∈ Fin → (¬ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
168	167	necon4bd 2984	. . . . 5 ⊢ (𝐹 ∈ Fin → ((♯‘𝐹) = (♯‘dom 𝐹) → ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
169	168	imp 411	. . . 4 ⊢ ((𝐹 ∈ Fin ∧ (♯‘𝐹) = (♯‘dom 𝐹)) → ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
170		dffun4 6547	. . . 4 ⊢ (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
171	70, 169, 170	sylanbrc 594	. . 3 ⊢ ((𝐹 ∈ Fin ∧ (♯‘𝐹) = (♯‘dom 𝐹)) → Fun 𝐹)
172	171	ex 417	. 2 ⊢ (𝐹 ∈ Fin → ((♯‘𝐹) = (♯‘dom 𝐹) → Fun 𝐹))
173	3, 172	impbid2 229	1 ⊢ (𝐹 ∈ Fin → (Fun 𝐹 ↔ (♯‘𝐹) = (♯‘dom 𝐹)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101  ∀wal 1565   = wceq 1567  ∃wex 1806   ∈ wcel 2149   ≠ wne 2964  ∀wral 3085  ∃wrex 3095  Vcvv 3463   ∖ cdif 3910   ∪ cun 3911   ∩ cin 3912   ⊆ wss 3913  ∅c0 4294  {csn 4591  {cpr 4593  ⟨cop 4597   class class class wbr 5110   × cxp 5657  dom cdm 5659  Rel wrel 5664  Fun wfun 6528   Fn wfn 6529  ‘cfv 6534  (class class class)co 7408   ≼ cdom 8937  Fincfn 8939  ℝcr 11095  1c1 11097   + caddc 11099   < clt 11239   ≤ cle 11240  2c2 12291  ℕ₀cn0 12500  ♯chash 14362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5239  ax-sep 5258  ax-nul 5268  ax-pow 5334  ax-pr 5402  ax-un 7730  ax-cnex 11152  ax-resscn 11153  ax-1cn 11154  ax-icn 11155  ax-addcl 11156  ax-addrcl 11157  ax-mulcl 11158  ax-mulrcl 11159  ax-mulcom 11160  ax-addass 11161  ax-mulass 11162  ax-distr 11163  ax-i2m1 11164  ax-1ne0 11165  ax-1rid 11166  ax-rnegex 11167  ax-rrecex 11168  ax-cnre 11169  ax-pre-lttri 11170  ax-pre-lttrn 11171  ax-pre-ltadd 11172  ax-pre-mulgt0 11173

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-int 4914  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6300  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6490  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-riota 7365  df-ov 7411  df-oprab 7412  df-mpo 7413  df-om 7859  df-1st 7982  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-1o 8449  df-2o 8450  df-oadd 8453  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-dju 9883  df-card 9921  df-pnf 11241  df-mnf 11242  df-xr 11243  df-ltxr 11244  df-le 11245  df-sub 11439  df-neg 11440  df-nn 12230  df-2 12299  df-n0 12501  df-xnn0 12574  df-z 12588  df-uz 12859  df-fz 13532  df-hash 14363

This theorem is referenced by:  hashres  14471  hashreshashfun  14472  hashfundm  14475  ccatalpha  14627