MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  hashfun Structured version   Visualization version   GIF version

Theorem hashfun 13634
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.
StepHypRef Expression
1 funfn 6247 . . 3 (Fun 𝐹𝐹 Fn dom 𝐹)
2 hashfn 13572 . . 3 (𝐹 Fn dom 𝐹 → (♯‘𝐹) = (♯‘dom 𝐹))
31, 2sylbi 218 . 2 (Fun 𝐹 → (♯‘𝐹) = (♯‘dom 𝐹))
4 dmfi 8638 . . . . . . . . . . 11 (𝐹 ∈ Fin → dom 𝐹 ∈ Fin)
5 hashcl 13555 . . . . . . . . . . 11 (dom 𝐹 ∈ Fin → (♯‘dom 𝐹) ∈ ℕ0)
64, 5syl 17 . . . . . . . . . 10 (𝐹 ∈ Fin → (♯‘dom 𝐹) ∈ ℕ0)
76nn0red 11793 . . . . . . . . 9 (𝐹 ∈ Fin → (♯‘dom 𝐹) ∈ ℝ)
87adantr 481 . . . . . . . 8 ((𝐹 ∈ Fin ∧ ¬ Rel 𝐹) → (♯‘dom 𝐹) ∈ ℝ)
9 df-rel 5442 . . . . . . . . . . . . 13 (Rel 𝐹𝐹 ⊆ (V × V))
10 dfss3 3873 . . . . . . . . . . . . 13 (𝐹 ⊆ (V × V) ↔ ∀𝑥𝐹 𝑥 ∈ (V × V))
119, 10bitri 276 . . . . . . . . . . . 12 (Rel 𝐹 ↔ ∀𝑥𝐹 𝑥 ∈ (V × V))
1211notbii 321 . . . . . . . . . . 11 (¬ Rel 𝐹 ↔ ¬ ∀𝑥𝐹 𝑥 ∈ (V × V))
13 rexnal 3200 . . . . . . . . . . 11 (∃𝑥𝐹 ¬ 𝑥 ∈ (V × V) ↔ ¬ ∀𝑥𝐹 𝑥 ∈ (V × V))
1412, 13bitr4i 279 . . . . . . . . . 10 (¬ Rel 𝐹 ↔ ∃𝑥𝐹 ¬ 𝑥 ∈ (V × V))
15 dmun 5657 . . . . . . . . . . . . . . . 16 dom ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥})
1615fveq2i 6533 . . . . . . . . . . . . . . 15 (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘(dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}))
17 dmsnn0 5931 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (V × V) ↔ dom {𝑥} ≠ ∅)
1817biimpri 229 . . . . . . . . . . . . . . . . . . . 20 (dom {𝑥} ≠ ∅ → 𝑥 ∈ (V × V))
1918necon1bi 3010 . . . . . . . . . . . . . . . . . . 19 𝑥 ∈ (V × V) → dom {𝑥} = ∅)
20193ad2ant3 1126 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → dom {𝑥} = ∅)
2120uneq2d 4055 . . . . . . . . . . . . . . . . 17 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}) = (dom (𝐹 ∖ {𝑥}) ∪ ∅))
22 un0 4258 . . . . . . . . . . . . . . . . 17 (dom (𝐹 ∖ {𝑥}) ∪ ∅) = dom (𝐹 ∖ {𝑥})
2321, 22syl6eq 2845 . . . . . . . . . . . . . . . 16 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}) = dom (𝐹 ∖ {𝑥}))
2423fveq2d 6534 . . . . . . . . . . . . . . 15 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘(dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥})) = (♯‘dom (𝐹 ∖ {𝑥})))
2516, 24syl5eq 2841 . . . . . . . . . . . . . 14 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘dom (𝐹 ∖ {𝑥})))
26 diffi 8586 . . . . . . . . . . . . . . . . . . 19 (𝐹 ∈ Fin → (𝐹 ∖ {𝑥}) ∈ Fin)
27 dmfi 8638 . . . . . . . . . . . . . . . . . . 19 ((𝐹 ∖ {𝑥}) ∈ Fin → dom (𝐹 ∖ {𝑥}) ∈ Fin)
2826, 27syl 17 . . . . . . . . . . . . . . . . . 18 (𝐹 ∈ Fin → dom (𝐹 ∖ {𝑥}) ∈ Fin)
29 hashcl 13555 . . . . . . . . . . . . . . . . . 18 (dom (𝐹 ∖ {𝑥}) ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) ∈ ℕ0)
3028, 29syl 17 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) ∈ ℕ0)
3130nn0red 11793 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) ∈ ℝ)
32 hashcl 13555 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∖ {𝑥}) ∈ Fin → (♯‘(𝐹 ∖ {𝑥})) ∈ ℕ0)
3326, 32syl 17 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {𝑥})) ∈ ℕ0)
3433nn0red 11793 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {𝑥})) ∈ ℝ)
35 peano2re 10649 . . . . . . . . . . . . . . . . 17 ((♯‘(𝐹 ∖ {𝑥})) ∈ ℝ → ((♯‘(𝐹 ∖ {𝑥})) + 1) ∈ ℝ)
3634, 35syl 17 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → ((♯‘(𝐹 ∖ {𝑥})) + 1) ∈ ℝ)
37 fidomdm 8637 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∖ {𝑥}) ∈ Fin → dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥}))
3826, 37syl 17 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ Fin → dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥}))
39 hashdom 13576 . . . . . . . . . . . . . . . . . 18 ((dom (𝐹 ∖ {𝑥}) ∈ Fin ∧ (𝐹 ∖ {𝑥}) ∈ Fin) → ((♯‘dom (𝐹 ∖ {𝑥})) ≤ (♯‘(𝐹 ∖ {𝑥})) ↔ dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥})))
4028, 26, 39syl2anc 584 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ Fin → ((♯‘dom (𝐹 ∖ {𝑥})) ≤ (♯‘(𝐹 ∖ {𝑥})) ↔ dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥})))
4138, 40mpbird 258 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) ≤ (♯‘(𝐹 ∖ {𝑥})))
4234ltp1d 11407 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {𝑥})) < ((♯‘(𝐹 ∖ {𝑥})) + 1))
4331, 34, 36, 41, 42lelttrd 10634 . . . . . . . . . . . . . . 15 (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) < ((♯‘(𝐹 ∖ {𝑥})) + 1))
44433ad2ant1 1124 . . . . . . . . . . . . . 14 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom (𝐹 ∖ {𝑥})) < ((♯‘(𝐹 ∖ {𝑥})) + 1))
4525, 44eqbrtrd 4978 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) < ((♯‘(𝐹 ∖ {𝑥})) + 1))
46 snfi 8432 . . . . . . . . . . . . . . . . 17 {𝑥} ∈ Fin
47 incom 4094 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∖ {𝑥}) ∩ {𝑥}) = ({𝑥} ∩ (𝐹 ∖ {𝑥}))
48 disjdif 4329 . . . . . . . . . . . . . . . . . 18 ({𝑥} ∩ (𝐹 ∖ {𝑥})) = ∅
4947, 48eqtri 2817 . . . . . . . . . . . . . . . . 17 ((𝐹 ∖ {𝑥}) ∩ {𝑥}) = ∅
50 hashun 13579 . . . . . . . . . . . . . . . . 17 (((𝐹 ∖ {𝑥}) ∈ Fin ∧ {𝑥} ∈ Fin ∧ ((𝐹 ∖ {𝑥}) ∩ {𝑥}) = ∅) → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥})))
5146, 49, 50mp3an23 1443 . . . . . . . . . . . . . . . 16 ((𝐹 ∖ {𝑥}) ∈ Fin → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥})))
5226, 51syl 17 . . . . . . . . . . . . . . 15 (𝐹 ∈ Fin → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥})))
53 hashsng 13567 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ V → (♯‘{𝑥}) = 1)
5453elv 3437 . . . . . . . . . . . . . . . 16 (♯‘{𝑥}) = 1
5554oveq2i 7018 . . . . . . . . . . . . . . 15 ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + 1)
5652, 55syl6req 2846 . . . . . . . . . . . . . 14 (𝐹 ∈ Fin → ((♯‘(𝐹 ∖ {𝑥})) + 1) = (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})))
57563ad2ant1 1124 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → ((♯‘(𝐹 ∖ {𝑥})) + 1) = (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})))
5845, 57breqtrd 4982 . . . . . . . . . . . 12 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) < (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})))
59 difsnid 4644 . . . . . . . . . . . . . . 15 (𝑥𝐹 → ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = 𝐹)
6059dmeqd 5652 . . . . . . . . . . . . . 14 (𝑥𝐹 → dom ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = dom 𝐹)
6160fveq2d 6534 . . . . . . . . . . . . 13 (𝑥𝐹 → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘dom 𝐹))
62613ad2ant2 1125 . . . . . . . . . . . 12 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘dom 𝐹))
6359fveq2d 6534 . . . . . . . . . . . . 13 (𝑥𝐹 → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘𝐹))
64633ad2ant2 1125 . . . . . . . . . . . 12 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘𝐹))
6558, 62, 643brtr3d 4987 . . . . . . . . . . 11 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom 𝐹) < (♯‘𝐹))
6665rexlimdv3a 3246 . . . . . . . . . 10 (𝐹 ∈ Fin → (∃𝑥𝐹 ¬ 𝑥 ∈ (V × V) → (♯‘dom 𝐹) < (♯‘𝐹)))
6714, 66syl5bi 243 . . . . . . . . 9 (𝐹 ∈ Fin → (¬ Rel 𝐹 → (♯‘dom 𝐹) < (♯‘𝐹)))
6867imp 407 . . . . . . . 8 ((𝐹 ∈ Fin ∧ ¬ Rel 𝐹) → (♯‘dom 𝐹) < (♯‘𝐹))
698, 68gtned 10611 . . . . . . 7 ((𝐹 ∈ Fin ∧ ¬ Rel 𝐹) → (♯‘𝐹) ≠ (♯‘dom 𝐹))
7069ex 413 . . . . . 6 (𝐹 ∈ Fin → (¬ Rel 𝐹 → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
7170necon4bd 3002 . . . . 5 (𝐹 ∈ Fin → ((♯‘𝐹) = (♯‘dom 𝐹) → Rel 𝐹))
7271imp 407 . . . 4 ((𝐹 ∈ Fin ∧ (♯‘𝐹) = (♯‘dom 𝐹)) → Rel 𝐹)
73 2nalexn 1807 . . . . . . . 8 (¬ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥𝑦 ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
74 df-ne 2983 . . . . . . . . . . . . 13 (𝑦𝑧 ↔ ¬ 𝑦 = 𝑧)
7574anbi2i 622 . . . . . . . . . . . 12 (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))
76 annim 404 . . . . . . . . . . . 12 (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧) ↔ ¬ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
7775, 76bitri 276 . . . . . . . . . . 11 (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧) ↔ ¬ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
7877exbii 1827 . . . . . . . . . 10 (∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧) ↔ ∃𝑧 ¬ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
79 exnal 1806 . . . . . . . . . 10 (∃𝑧 ¬ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
8078, 79bitr2i 277 . . . . . . . . 9 (¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧))
81802exbii 1828 . . . . . . . 8 (∃𝑥𝑦 ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧))
8273, 81bitri 276 . . . . . . 7 (¬ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧))
837adantr 481 . . . . . . . . . . 11 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘dom 𝐹) ∈ ℝ)
84 2re 11548 . . . . . . . . . . . . 13 2 ∈ ℝ
85 diffi 8586 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ Fin → (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin)
86 dmfi 8638 . . . . . . . . . . . . . . . . 17 ((𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin)
8785, 86syl 17 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin)
88 hashcl 13555 . . . . . . . . . . . . . . . 16 (dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℕ0)
8987, 88syl 17 . . . . . . . . . . . . . . 15 (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℕ0)
9089nn0red 11793 . . . . . . . . . . . . . 14 (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ)
9190adantr 481 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ)
92 readdcl 10455 . . . . . . . . . . . . 13 ((2 ∈ ℝ ∧ (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
9384, 91, 92sylancr 587 . . . . . . . . . . . 12 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
94 hashcl 13555 . . . . . . . . . . . . . 14 (𝐹 ∈ Fin → (♯‘𝐹) ∈ ℕ0)
9594nn0red 11793 . . . . . . . . . . . . 13 (𝐹 ∈ Fin → (♯‘𝐹) ∈ ℝ)
9695adantr 481 . . . . . . . . . . . 12 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘𝐹) ∈ ℝ)
97 1re 10476 . . . . . . . . . . . . . . 15 1 ∈ ℝ
98 readdcl 10455 . . . . . . . . . . . . . . 15 ((1 ∈ ℝ ∧ (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ) → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
9997, 90, 98sylancr 587 . . . . . . . . . . . . . 14 (𝐹 ∈ Fin → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
10099adantr 481 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
10184, 90, 92sylancr 587 . . . . . . . . . . . . . 14 (𝐹 ∈ Fin → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
102101adantr 481 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
103 dmun 5657 . . . . . . . . . . . . . . . . . 18 dom ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = (dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))
104 opex 5241 . . . . . . . . . . . . . . . . . . . . 21 𝑥, 𝑦⟩ ∈ V
105 opex 5241 . . . . . . . . . . . . . . . . . . . . 21 𝑥, 𝑧⟩ ∈ V
106104, 105prss 4654 . . . . . . . . . . . . . . . . . . . 20 ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ↔ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ⊆ 𝐹)
107 undif 4338 . . . . . . . . . . . . . . . . . . . 20 ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ⊆ 𝐹 ↔ ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = 𝐹)
108106, 107sylbb 220 . . . . . . . . . . . . . . . . . . 19 ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = 𝐹)
109108dmeqd 5652 . . . . . . . . . . . . . . . . . 18 ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → dom ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = dom 𝐹)
110103, 109syl5reqr 2844 . . . . . . . . . . . . . . . . 17 ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → dom 𝐹 = (dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
111 vex 3435 . . . . . . . . . . . . . . . . . . . 20 𝑦 ∈ V
112 vex 3435 . . . . . . . . . . . . . . . . . . . 20 𝑧 ∈ V
113111, 112dmprop 5941 . . . . . . . . . . . . . . . . . . 19 dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} = {𝑥, 𝑥}
114 dfsn2 4479 . . . . . . . . . . . . . . . . . . 19 {𝑥} = {𝑥, 𝑥}
115113, 114eqtr4i 2820 . . . . . . . . . . . . . . . . . 18 dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} = {𝑥}
116115uneq1i 4051 . . . . . . . . . . . . . . . . 17 (dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = ({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))
117110, 116syl6eq 2845 . . . . . . . . . . . . . . . 16 ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → dom 𝐹 = ({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
118117fveq2d 6534 . . . . . . . . . . . . . . 15 ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (♯‘dom 𝐹) = (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
119118ad2antrl 724 . . . . . . . . . . . . . 14 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘dom 𝐹) = (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
120 hashun2 13580 . . . . . . . . . . . . . . . . 17 (({𝑥} ∈ Fin ∧ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin) → (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ ((♯‘{𝑥}) + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
12146, 87, 120sylancr 587 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ ((♯‘{𝑥}) + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
12254oveq1i 7017 . . . . . . . . . . . . . . . 16 ((♯‘{𝑥}) + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
123121, 122syl6breq 4997 . . . . . . . . . . . . . . 15 (𝐹 ∈ Fin → (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
124123adantr 481 . . . . . . . . . . . . . 14 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
125119, 124eqbrtrd 4978 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘dom 𝐹) ≤ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
126 1lt2 11645 . . . . . . . . . . . . . . 15 1 < 2
127 ltadd1 10944 . . . . . . . . . . . . . . . 16 ((1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ) → (1 < 2 ↔ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
12897, 84, 90, 127mp3an12i 1455 . . . . . . . . . . . . . . 15 (𝐹 ∈ Fin → (1 < 2 ↔ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
129126, 128mpbii 234 . . . . . . . . . . . . . 14 (𝐹 ∈ Fin → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
130129adantr 481 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
13183, 100, 102, 125, 130lelttrd 10634 . . . . . . . . . . . 12 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘dom 𝐹) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
132 fidomdm 8637 . . . . . . . . . . . . . . . . 17 ((𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ≼ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))
13385, 132syl 17 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ≼ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))
134 hashdom 13576 . . . . . . . . . . . . . . . . 17 ((dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin ∧ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin) → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ≼ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
13587, 85, 134syl2anc 584 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ≼ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
136133, 135mpbird 258 . . . . . . . . . . . . . . 15 (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
137 hashcl 13555 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℕ0)
13885, 137syl 17 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℕ0)
139138nn0red 11793 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ)
140 leadd2 10946 . . . . . . . . . . . . . . . . 17 (((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ ∧ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ ∧ 2 ∈ ℝ) → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
14184, 140mp3an3 1440 . . . . . . . . . . . . . . . 16 (((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ ∧ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ) → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
14290, 139, 141syl2anc 584 . . . . . . . . . . . . . . 15 (𝐹 ∈ Fin → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
143136, 142mpbid 233 . . . . . . . . . . . . . 14 (𝐹 ∈ Fin → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
144143adantr 481 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
145 prfi 8629 . . . . . . . . . . . . . . . . 17 {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∈ Fin
146 disjdif 4329 . . . . . . . . . . . . . . . . 17 ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∩ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = ∅
147 hashun 13579 . . . . . . . . . . . . . . . . 17 (({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∈ Fin ∧ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin ∧ ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∩ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = ∅) → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
148145, 146, 147mp3an13 1442 . . . . . . . . . . . . . . . 16 ((𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
14985, 148syl 17 . . . . . . . . . . . . . . 15 (𝐹 ∈ Fin → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
150149adantr 481 . . . . . . . . . . . . . 14 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
151108fveq2d 6534 . . . . . . . . . . . . . . 15 ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (♯‘𝐹))
152151ad2antrl 724 . . . . . . . . . . . . . 14 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (♯‘𝐹))
153 vex 3435 . . . . . . . . . . . . . . . . . . . 20 𝑥 ∈ V
154153, 111opth 5253 . . . . . . . . . . . . . . . . . . 19 (⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑧⟩ ↔ (𝑥 = 𝑥𝑦 = 𝑧))
155154simprbi 497 . . . . . . . . . . . . . . . . . 18 (⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑧⟩ → 𝑦 = 𝑧)
156155necon3i 3014 . . . . . . . . . . . . . . . . 17 (𝑦𝑧 → ⟨𝑥, 𝑦⟩ ≠ ⟨𝑥, 𝑧⟩)
157 hashprg 13592 . . . . . . . . . . . . . . . . . 18 ((⟨𝑥, 𝑦⟩ ∈ V ∧ ⟨𝑥, 𝑧⟩ ∈ V) → (⟨𝑥, 𝑦⟩ ≠ ⟨𝑥, 𝑧⟩ ↔ (♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) = 2))
158104, 105, 157mp2an 688 . . . . . . . . . . . . . . . . 17 (⟨𝑥, 𝑦⟩ ≠ ⟨𝑥, 𝑧⟩ ↔ (♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) = 2)
159156, 158sylib 219 . . . . . . . . . . . . . . . 16 (𝑦𝑧 → (♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) = 2)
160159oveq1d 7022 . . . . . . . . . . . . . . 15 (𝑦𝑧 → ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
161160ad2antll 725 . . . . . . . . . . . . . 14 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
162150, 152, 1613eqtr3rd 2838 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (♯‘𝐹))
163144, 162breqtrd 4982 . . . . . . . . . . . 12 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (♯‘𝐹))
16483, 93, 96, 131, 163ltletrd 10636 . . . . . . . . . . 11 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘dom 𝐹) < (♯‘𝐹))
16583, 164gtned 10611 . . . . . . . . . 10 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘𝐹) ≠ (♯‘dom 𝐹))
166165ex 413 . . . . . . . . 9 (𝐹 ∈ Fin → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
167166exlimdv 1909 . . . . . . . 8 (𝐹 ∈ Fin → (∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
168167exlimdvv 1910 . . . . . . 7 (𝐹 ∈ Fin → (∃𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
16982, 168syl5bi 243 . . . . . 6 (𝐹 ∈ Fin → (¬ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
170169necon4bd 3002 . . . . 5 (𝐹 ∈ Fin → ((♯‘𝐹) = (♯‘dom 𝐹) → ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
171170imp 407 . . . 4 ((𝐹 ∈ Fin ∧ (♯‘𝐹) = (♯‘dom 𝐹)) → ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
172 dffun4 6229 . . . 4 (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
17372, 171, 172sylanbrc 583 . . 3 ((𝐹 ∈ Fin ∧ (♯‘𝐹) = (♯‘dom 𝐹)) → Fun 𝐹)
174173ex 413 . 2 (𝐹 ∈ Fin → ((♯‘𝐹) = (♯‘dom 𝐹) → Fun 𝐹))
1753, 174impbid2 227 1 (𝐹 ∈ Fin → (Fun 𝐹 ↔ (♯‘𝐹) = (♯‘dom 𝐹)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1078  wal 1518   = wceq 1520  wex 1759  wcel 2079  wne 2982  wral 3103  wrex 3104  Vcvv 3432  cdif 3851  cun 3852  cin 3853  wss 3854  c0 4206  {csn 4466  {cpr 4468  cop 4472   class class class wbr 4956   × cxp 5433  dom cdm 5435  Rel wrel 5440  Fun wfun 6211   Fn wfn 6212  cfv 6217  (class class class)co 7007  cdom 8345  Fincfn 8347  cr 10371  1c1 10373   + caddc 10375   < clt 10510  cle 10511  2c2 11529  0cn0 11734  chash 13528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-13 2342  ax-ext 2767  ax-rep 5075  ax-sep 5088  ax-nul 5095  ax-pow 5150  ax-pr 5214  ax-un 7310  ax-cnex 10428  ax-resscn 10429  ax-1cn 10430  ax-icn 10431  ax-addcl 10432  ax-addrcl 10433  ax-mulcl 10434  ax-mulrcl 10435  ax-mulcom 10436  ax-addass 10437  ax-mulass 10438  ax-distr 10439  ax-i2m1 10440  ax-1ne0 10441  ax-1rid 10442  ax-rnegex 10443  ax-rrecex 10444  ax-cnre 10445  ax-pre-lttri 10446  ax-pre-lttrn 10447  ax-pre-ltadd 10448  ax-pre-mulgt0 10449
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1079  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-mo 2574  df-eu 2610  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-ne 2983  df-nel 3089  df-ral 3108  df-rex 3109  df-reu 3110  df-rmo 3111  df-rab 3112  df-v 3434  df-sbc 3702  df-csb 3807  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-pss 3871  df-nul 4207  df-if 4376  df-pw 4449  df-sn 4467  df-pr 4469  df-tp 4471  df-op 4473  df-uni 4740  df-int 4777  df-iun 4821  df-br 4957  df-opab 5019  df-mpt 5036  df-tr 5058  df-id 5340  df-eprel 5345  df-po 5354  df-so 5355  df-fr 5394  df-we 5396  df-xp 5441  df-rel 5442  df-cnv 5443  df-co 5444  df-dm 5445  df-rn 5446  df-res 5447  df-ima 5448  df-pred 6015  df-ord 6061  df-on 6062  df-lim 6063  df-suc 6064  df-iota 6181  df-fun 6219  df-fn 6220  df-f 6221  df-f1 6222  df-fo 6223  df-f1o 6224  df-fv 6225  df-riota 6968  df-ov 7010  df-oprab 7011  df-mpo 7012  df-om 7428  df-1st 7536  df-2nd 7537  df-wrecs 7789  df-recs 7851  df-rdg 7889  df-1o 7944  df-oadd 7948  df-er 8130  df-en 8348  df-dom 8349  df-sdom 8350  df-fin 8351  df-dju 9165  df-card 9203  df-pnf 10512  df-mnf 10513  df-xr 10514  df-ltxr 10515  df-le 10516  df-sub 10708  df-neg 10709  df-nn 11476  df-2 11537  df-n0 11735  df-xnn0 11805  df-z 11819  df-uz 12083  df-fz 12732  df-hash 13529
This theorem is referenced by:  hashres  13635  hashreshashfun  13636  ccatalpha  13779  cycpmconjslem2  30393  hashfundm  31924
  Copyright terms: Public domain W3C validator