Theorem hashfun 14476

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 6596	. . 3 ⊢ (Fun 𝐹 ↔ 𝐹 Fn dom 𝐹)
2		hashfn 14414	. . 3 ⊢ (𝐹 Fn dom 𝐹 → (♯‘𝐹) = (♯‘dom 𝐹))
3	1, 2	sylbi 217	. 2 ⊢ (Fun 𝐹 → (♯‘𝐹) = (♯‘dom 𝐹))
4		dmfi 9375	. . . . . . . . . . 11 ⊢ (𝐹 ∈ Fin → dom 𝐹 ∈ Fin)
5		hashcl 14395	. . . . . . . . . . 11 ⊢ (dom 𝐹 ∈ Fin → (♯‘dom 𝐹) ∈ ℕ0)
6	4, 5	syl 17	. . . . . . . . . 10 ⊢ (𝐹 ∈ Fin → (♯‘dom 𝐹) ∈ ℕ0)
7	6	nn0red 12588	. . . . . . . . 9 ⊢ (𝐹 ∈ Fin → (♯‘dom 𝐹) ∈ ℝ)
8	7	adantr 480	. . . . . . . 8 ⊢ ((𝐹 ∈ Fin ∧ ¬ Rel 𝐹) → (♯‘dom 𝐹) ∈ ℝ)
9		df-rel 5692	. . . . . . . . . . . . 13 ⊢ (Rel 𝐹 ↔ 𝐹 ⊆ (V × V))
10		dfss3 3972	. . . . . . . . . . . . 13 ⊢ (𝐹 ⊆ (V × V) ↔ ∀𝑥 ∈ 𝐹 𝑥 ∈ (V × V))
11	9, 10	bitri 275	. . . . . . . . . . . 12 ⊢ (Rel 𝐹 ↔ ∀𝑥 ∈ 𝐹 𝑥 ∈ (V × V))
12	11	notbii 320	. . . . . . . . . . 11 ⊢ (¬ Rel 𝐹 ↔ ¬ ∀𝑥 ∈ 𝐹 𝑥 ∈ (V × V))
13		rexnal 3100	. . . . . . . . . . 11 ⊢ (∃𝑥 ∈ 𝐹 ¬ 𝑥 ∈ (V × V) ↔ ¬ ∀𝑥 ∈ 𝐹 𝑥 ∈ (V × V))
14	12, 13	bitr4i 278	. . . . . . . . . 10 ⊢ (¬ Rel 𝐹 ↔ ∃𝑥 ∈ 𝐹 ¬ 𝑥 ∈ (V × V))
15		dmun 5921	. . . . . . . . . . . . . . . 16 ⊢ dom ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥})
16	15	fveq2i 6909	. . . . . . . . . . . . . . 15 ⊢ (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘(dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}))
17		dmsnn0 6227	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (V × V) ↔ dom {𝑥} ≠ ∅)
18	17	biimpri 228	. . . . . . . . . . . . . . . . . . . 20 ⊢ (dom {𝑥} ≠ ∅ → 𝑥 ∈ (V × V))
19	18	necon1bi 2969	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑥 ∈ (V × V) → dom {𝑥} = ∅)
20	19	3ad2ant3 1136	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → dom {𝑥} = ∅)
21	20	uneq2d 4168	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}) = (dom (𝐹 ∖ {𝑥}) ∪ ∅))
22		un0 4394	. . . . . . . . . . . . . . . . 17 ⊢ (dom (𝐹 ∖ {𝑥}) ∪ ∅) = dom (𝐹 ∖ {𝑥})
23	21, 22	eqtrdi 2793	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}) = dom (𝐹 ∖ {𝑥}))
24	23	fveq2d 6910	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘(dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥})) = (♯‘dom (𝐹 ∖ {𝑥})))
25	16, 24	eqtrid 2789	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘dom (𝐹 ∖ {𝑥})))
26		diffi 9215	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ Fin → (𝐹 ∖ {𝑥}) ∈ Fin)
27		dmfi 9375	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹 ∖ {𝑥}) ∈ Fin → dom (𝐹 ∖ {𝑥}) ∈ Fin)
28	26, 27	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 ∈ Fin → dom (𝐹 ∖ {𝑥}) ∈ Fin)
29		hashcl 14395	. . . . . . . . . . . . . . . . . 18 ⊢ (dom (𝐹 ∖ {𝑥}) ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) ∈ ℕ0)
30	28, 29	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) ∈ ℕ0)
31	30	nn0red 12588	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) ∈ ℝ)
32		hashcl 14395	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∖ {𝑥}) ∈ Fin → (♯‘(𝐹 ∖ {𝑥})) ∈ ℕ0)
33	26, 32	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {𝑥})) ∈ ℕ0)
34	33	nn0red 12588	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {𝑥})) ∈ ℝ)
35		peano2re 11434	. . . . . . . . . . . . . . . . 17 ⊢ ((♯‘(𝐹 ∖ {𝑥})) ∈ ℝ → ((♯‘(𝐹 ∖ {𝑥})) + 1) ∈ ℝ)
36	34, 35	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ Fin → ((♯‘(𝐹 ∖ {𝑥})) + 1) ∈ ℝ)
37		fidomdm 9374	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∖ {𝑥}) ∈ Fin → dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥}))
38	26, 37	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ Fin → dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥}))
39		hashdom 14418	. . . . . . . . . . . . . . . . . 18 ⊢ ((dom (𝐹 ∖ {𝑥}) ∈ Fin ∧ (𝐹 ∖ {𝑥}) ∈ Fin) → ((♯‘dom (𝐹 ∖ {𝑥})) ≤ (♯‘(𝐹 ∖ {𝑥})) ↔ dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥})))
40	28, 26, 39	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ Fin → ((♯‘dom (𝐹 ∖ {𝑥})) ≤ (♯‘(𝐹 ∖ {𝑥})) ↔ dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥})))
41	38, 40	mpbird 257	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) ≤ (♯‘(𝐹 ∖ {𝑥})))
42	34	ltp1d 12198	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {𝑥})) < ((♯‘(𝐹 ∖ {𝑥})) + 1))
43	31, 34, 36, 41, 42	lelttrd 11419	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) < ((♯‘(𝐹 ∖ {𝑥})) + 1))
44	43	3ad2ant1 1134	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom (𝐹 ∖ {𝑥})) < ((♯‘(𝐹 ∖ {𝑥})) + 1))
45	25, 44	eqbrtrd 5165	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) < ((♯‘(𝐹 ∖ {𝑥})) + 1))
46		snfi 9083	. . . . . . . . . . . . . . . . 17 ⊢ {𝑥} ∈ Fin
47		disjdifr 4473	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ∖ {𝑥}) ∩ {𝑥}) = ∅
48		hashun 14421	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∖ {𝑥}) ∈ Fin ∧ {𝑥} ∈ Fin ∧ ((𝐹 ∖ {𝑥}) ∩ {𝑥}) = ∅) → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥})))
49	46, 47, 48	mp3an23 1455	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∖ {𝑥}) ∈ Fin → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥})))
50	26, 49	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ Fin → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥})))
51		hashsng 14408	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ V → (♯‘{𝑥}) = 1)
52	51	elv 3485	. . . . . . . . . . . . . . . 16 ⊢ (♯‘{𝑥}) = 1
53	52	oveq2i 7442	. . . . . . . . . . . . . . 15 ⊢ ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + 1)
54	50, 53	eqtr2di 2794	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ Fin → ((♯‘(𝐹 ∖ {𝑥})) + 1) = (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})))
55	54	3ad2ant1 1134	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → ((♯‘(𝐹 ∖ {𝑥})) + 1) = (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})))
56	45, 55	breqtrd 5169	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) < (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})))
57		difsnid 4810	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝐹 → ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = 𝐹)
58	57	dmeqd 5916	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐹 → dom ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = dom 𝐹)
59	58	fveq2d 6910	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐹 → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘dom 𝐹))
60	59	3ad2ant2 1135	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘dom 𝐹))
61	57	fveq2d 6910	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐹 → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘𝐹))
62	61	3ad2ant2 1135	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘𝐹))
63	56, 60, 62	3brtr3d 5174	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom 𝐹) < (♯‘𝐹))
64	63	rexlimdv3a 3159	. . . . . . . . . 10 ⊢ (𝐹 ∈ Fin → (∃𝑥 ∈ 𝐹 ¬ 𝑥 ∈ (V × V) → (♯‘dom 𝐹) < (♯‘𝐹)))
65	14, 64	biimtrid 242	. . . . . . . . 9 ⊢ (𝐹 ∈ Fin → (¬ Rel 𝐹 → (♯‘dom 𝐹) < (♯‘𝐹)))
66	65	imp 406	. . . . . . . 8 ⊢ ((𝐹 ∈ Fin ∧ ¬ Rel 𝐹) → (♯‘dom 𝐹) < (♯‘𝐹))
67	8, 66	gtned 11396	. . . . . . 7 ⊢ ((𝐹 ∈ Fin ∧ ¬ Rel 𝐹) → (♯‘𝐹) ≠ (♯‘dom 𝐹))
68	67	ex 412	. . . . . 6 ⊢ (𝐹 ∈ Fin → (¬ Rel 𝐹 → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
69	68	necon4bd 2960	. . . . 5 ⊢ (𝐹 ∈ Fin → ((♯‘𝐹) = (♯‘dom 𝐹) → Rel 𝐹))
70	69	imp 406	. . . 4 ⊢ ((𝐹 ∈ Fin ∧ (♯‘𝐹) = (♯‘dom 𝐹)) → Rel 𝐹)
71		2nalexn 1828	. . . . . . . 8 ⊢ (¬ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥∃𝑦 ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
72		df-ne 2941	. . . . . . . . . . . . 13 ⊢ (𝑦 ≠ 𝑧 ↔ ¬ 𝑦 = 𝑧)
73	72	anbi2i 623	. . . . . . . . . . . 12 ⊢ (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))
74		annim 403	. . . . . . . . . . . 12 ⊢ (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧) ↔ ¬ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
75	73, 74	bitri 275	. . . . . . . . . . 11 ⊢ (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) ↔ ¬ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
76	75	exbii 1848	. . . . . . . . . 10 ⊢ (∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) ↔ ∃𝑧 ¬ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
77		exnal 1827	. . . . . . . . . 10 ⊢ (∃𝑧 ¬ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
78	76, 77	bitr2i 276	. . . . . . . . 9 ⊢ (¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧))
79	78	2exbii 1849	. . . . . . . 8 ⊢ (∃𝑥∃𝑦 ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥∃𝑦∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧))
80	71, 79	bitri 275	. . . . . . 7 ⊢ (¬ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥∃𝑦∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧))
81	7	adantr 480	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘dom 𝐹) ∈ ℝ)
82		2re 12340	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℝ
83		diffi 9215	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ Fin → (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin)
84		dmfi 9375	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin)
85	83, 84	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ Fin → dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin)
86		hashcl 14395	. . . . . . . . . . . . . . . 16 ⊢ (dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℕ0)
87	85, 86	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℕ0)
88	87	nn0red 12588	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ)
89	88	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ)
90		readdcl 11238	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℝ ∧ (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
91	82, 89, 90	sylancr 587	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
92		hashcl 14395	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ Fin → (♯‘𝐹) ∈ ℕ0)
93	92	nn0red 12588	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ Fin → (♯‘𝐹) ∈ ℝ)
94	93	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘𝐹) ∈ ℝ)
95		1re 11261	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ
96		readdcl 11238	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℝ ∧ (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ) → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
97	95, 88, 96	sylancr 587	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ Fin → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
98	97	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
99	82, 88, 90	sylancr 587	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ Fin → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
100	99	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
101		opex 5469	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ⟨𝑥, 𝑦⟩ ∈ V
102		opex 5469	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ⟨𝑥, 𝑧⟩ ∈ V
103	101, 102	prss 4820	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ↔ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ⊆ 𝐹)
104		undif 4482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ⊆ 𝐹 ↔ ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = 𝐹)
105	103, 104	sylbb 219	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = 𝐹)
106	105	dmeqd 5916	. . . . . . . . . . . . . . . . . 18 ⊢ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → dom ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = dom 𝐹)
107		dmun 5921	. . . . . . . . . . . . . . . . . 18 ⊢ dom ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = (dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))
108	106, 107	eqtr3di 2792	. . . . . . . . . . . . . . . . 17 ⊢ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → dom 𝐹 = (dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
109		vex 3484	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑦 ∈ V
110		vex 3484	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑧 ∈ V
111	109, 110	dmprop 6237	. . . . . . . . . . . . . . . . . . 19 ⊢ dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} = {𝑥, 𝑥}
112		dfsn2 4639	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑥} = {𝑥, 𝑥}
113	111, 112	eqtr4i 2768	. . . . . . . . . . . . . . . . . 18 ⊢ dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} = {𝑥}
114	113	uneq1i 4164	. . . . . . . . . . . . . . . . 17 ⊢ (dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = ({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))
115	108, 114	eqtrdi 2793	. . . . . . . . . . . . . . . 16 ⊢ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → dom 𝐹 = ({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
116	115	fveq2d 6910	. . . . . . . . . . . . . . 15 ⊢ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (♯‘dom 𝐹) = (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
117	116	ad2antrl 728	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘dom 𝐹) = (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
118		hashun2 14422	. . . . . . . . . . . . . . . . 17 ⊢ (({𝑥} ∈ Fin ∧ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin) → (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ ((♯‘{𝑥}) + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
119	46, 85, 118	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ Fin → (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ ((♯‘{𝑥}) + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
120	52	oveq1i 7441	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘{𝑥}) + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
121	119, 120	breqtrdi 5184	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ Fin → (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
122	121	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
123	117, 122	eqbrtrd 5165	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘dom 𝐹) ≤ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
124		1lt2 12437	. . . . . . . . . . . . . . 15 ⊢ 1 < 2
125		ltadd1 11730	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ) → (1 < 2 ↔ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
126	95, 82, 88, 125	mp3an12i 1467	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ Fin → (1 < 2 ↔ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
127	124, 126	mpbii 233	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ Fin → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
128	127	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
129	81, 98, 100, 123, 128	lelttrd 11419	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘dom 𝐹) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
130		fidomdm 9374	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ≼ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))
131	83, 130	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ Fin → dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ≼ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))
132		hashdom 14418	. . . . . . . . . . . . . . . . 17 ⊢ ((dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin ∧ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin) → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ≼ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
133	85, 83, 132	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ Fin → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ≼ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
134	131, 133	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
135		hashcl 14395	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℕ0)
136	83, 135	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℕ0)
137	136	nn0red 12588	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ)
138		leadd2 11732	. . . . . . . . . . . . . . . . 17 ⊢ (((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ ∧ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ ∧ 2 ∈ ℝ) → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
139	82, 138	mp3an3 1452	. . . . . . . . . . . . . . . 16 ⊢ (((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ ∧ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ) → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
140	88, 137, 139	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ Fin → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
141	134, 140	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ Fin → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
142	141	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
143		prfi 9363	. . . . . . . . . . . . . . . . 17 ⊢ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∈ Fin
144		disjdif 4472	. . . . . . . . . . . . . . . . 17 ⊢ ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∩ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = ∅
145		hashun 14421	. . . . . . . . . . . . . . . . 17 ⊢ (({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∈ Fin ∧ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin ∧ ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∩ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = ∅) → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
146	143, 144, 145	mp3an13 1454	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
147	83, 146	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ Fin → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
148	147	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
149	105	fveq2d 6910	. . . . . . . . . . . . . . 15 ⊢ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (♯‘𝐹))
150	149	ad2antrl 728	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (♯‘𝐹))
151		vex 3484	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑥 ∈ V
152	151, 109	opth 5481	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑧⟩ ↔ (𝑥 = 𝑥 ∧ 𝑦 = 𝑧))
153	152	simprbi 496	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑧⟩ → 𝑦 = 𝑧)
154	153	necon3i 2973	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ≠ 𝑧 → ⟨𝑥, 𝑦⟩ ≠ ⟨𝑥, 𝑧⟩)
155		hashprg 14434	. . . . . . . . . . . . . . . . . 18 ⊢ ((⟨𝑥, 𝑦⟩ ∈ V ∧ ⟨𝑥, 𝑧⟩ ∈ V) → (⟨𝑥, 𝑦⟩ ≠ ⟨𝑥, 𝑧⟩ ↔ (♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) = 2))
156	101, 102, 155	mp2an 692	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑥, 𝑦⟩ ≠ ⟨𝑥, 𝑧⟩ ↔ (♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) = 2)
157	154, 156	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ≠ 𝑧 → (♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) = 2)
158	157	oveq1d 7446	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ≠ 𝑧 → ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
159	158	ad2antll 729	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
160	148, 150, 159	3eqtr3rd 2786	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (♯‘𝐹))
161	142, 160	breqtrd 5169	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (♯‘𝐹))
162	81, 91, 94, 129, 161	ltletrd 11421	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘dom 𝐹) < (♯‘𝐹))
163	81, 162	gtned 11396	. . . . . . . . . 10 ⊢ ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘𝐹) ≠ (♯‘dom 𝐹))
164	163	ex 412	. . . . . . . . 9 ⊢ (𝐹 ∈ Fin → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
165	164	exlimdv 1933	. . . . . . . 8 ⊢ (𝐹 ∈ Fin → (∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
166	165	exlimdvv 1934	. . . . . . 7 ⊢ (𝐹 ∈ Fin → (∃𝑥∃𝑦∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
167	80, 166	biimtrid 242	. . . . . 6 ⊢ (𝐹 ∈ Fin → (¬ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
168	167	necon4bd 2960	. . . . 5 ⊢ (𝐹 ∈ Fin → ((♯‘𝐹) = (♯‘dom 𝐹) → ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
169	168	imp 406	. . . 4 ⊢ ((𝐹 ∈ Fin ∧ (♯‘𝐹) = (♯‘dom 𝐹)) → ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
170		dffun4 6577	. . . 4 ⊢ (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
171	70, 169, 170	sylanbrc 583	. . 3 ⊢ ((𝐹 ∈ Fin ∧ (♯‘𝐹) = (♯‘dom 𝐹)) → Fun 𝐹)
172	171	ex 412	. 2 ⊢ (𝐹 ∈ Fin → ((♯‘𝐹) = (♯‘dom 𝐹) → Fun 𝐹))
173	3, 172	impbid2 226	1 ⊢ (𝐹 ∈ Fin → (Fun 𝐹 ↔ (♯‘𝐹) = (♯‘dom 𝐹)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2108   ≠ wne 2940  ∀wral 3061  ∃wrex 3070  Vcvv 3480   ∖ cdif 3948   ∪ cun 3949   ∩ cin 3950   ⊆ wss 3951  ∅c0 4333  {csn 4626  {cpr 4628  ⟨cop 4632   class class class wbr 5143   × cxp 5683  dom cdm 5685  Rel wrel 5690  Fun wfun 6555   Fn wfn 6556  ‘cfv 6561  (class class class)co 7431   ≼ cdom 8983  Fincfn 8985  ℝcr 11154  1c1 11156   + caddc 11158   < clt 11295   ≤ cle 11296  2c2 12321  ℕ₀cn0 12526  ♯chash 14369

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-oadd 8510  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-dju 9941  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-2 12329  df-n0 12527  df-xnn0 12600  df-z 12614  df-uz 12879  df-fz 13548  df-hash 14370

This theorem is referenced by:  hashres  14477  hashreshashfun  14478  hashfundm  14481  ccatalpha  14631  cycpmconjslem2  33175