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

Theorem hashfun 13805
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 6375 . . 3 (Fun 𝐹𝐹 Fn dom 𝐹)
2 hashfn 13743 . . 3 (𝐹 Fn dom 𝐹 → (♯‘𝐹) = (♯‘dom 𝐹))
31, 2sylbi 220 . 2 (Fun 𝐹 → (♯‘𝐹) = (♯‘dom 𝐹))
4 dmfi 8801 . . . . . . . . . . 11 (𝐹 ∈ Fin → dom 𝐹 ∈ Fin)
5 hashcl 13724 . . . . . . . . . . 11 (dom 𝐹 ∈ Fin → (♯‘dom 𝐹) ∈ ℕ0)
64, 5syl 17 . . . . . . . . . 10 (𝐹 ∈ Fin → (♯‘dom 𝐹) ∈ ℕ0)
76nn0red 11955 . . . . . . . . 9 (𝐹 ∈ Fin → (♯‘dom 𝐹) ∈ ℝ)
87adantr 484 . . . . . . . 8 ((𝐹 ∈ Fin ∧ ¬ Rel 𝐹) → (♯‘dom 𝐹) ∈ ℝ)
9 df-rel 5550 . . . . . . . . . . . . 13 (Rel 𝐹𝐹 ⊆ (V × V))
10 dfss3 3941 . . . . . . . . . . . . 13 (𝐹 ⊆ (V × V) ↔ ∀𝑥𝐹 𝑥 ∈ (V × V))
119, 10bitri 278 . . . . . . . . . . . 12 (Rel 𝐹 ↔ ∀𝑥𝐹 𝑥 ∈ (V × V))
1211notbii 323 . . . . . . . . . . 11 (¬ Rel 𝐹 ↔ ¬ ∀𝑥𝐹 𝑥 ∈ (V × V))
13 rexnal 3232 . . . . . . . . . . 11 (∃𝑥𝐹 ¬ 𝑥 ∈ (V × V) ↔ ¬ ∀𝑥𝐹 𝑥 ∈ (V × V))
1412, 13bitr4i 281 . . . . . . . . . 10 (¬ Rel 𝐹 ↔ ∃𝑥𝐹 ¬ 𝑥 ∈ (V × V))
15 dmun 5767 . . . . . . . . . . . . . . . 16 dom ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥})
1615fveq2i 6666 . . . . . . . . . . . . . . 15 (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘(dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}))
17 dmsnn0 6053 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (V × V) ↔ dom {𝑥} ≠ ∅)
1817biimpri 231 . . . . . . . . . . . . . . . . . . . 20 (dom {𝑥} ≠ ∅ → 𝑥 ∈ (V × V))
1918necon1bi 3042 . . . . . . . . . . . . . . . . . . 19 𝑥 ∈ (V × V) → dom {𝑥} = ∅)
20193ad2ant3 1132 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → dom {𝑥} = ∅)
2120uneq2d 4125 . . . . . . . . . . . . . . . . 17 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}) = (dom (𝐹 ∖ {𝑥}) ∪ ∅))
22 un0 4327 . . . . . . . . . . . . . . . . 17 (dom (𝐹 ∖ {𝑥}) ∪ ∅) = dom (𝐹 ∖ {𝑥})
2321, 22syl6eq 2875 . . . . . . . . . . . . . . . 16 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}) = dom (𝐹 ∖ {𝑥}))
2423fveq2d 6667 . . . . . . . . . . . . . . 15 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘(dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥})) = (♯‘dom (𝐹 ∖ {𝑥})))
2516, 24syl5eq 2871 . . . . . . . . . . . . . 14 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘dom (𝐹 ∖ {𝑥})))
26 diffi 8749 . . . . . . . . . . . . . . . . . . 19 (𝐹 ∈ Fin → (𝐹 ∖ {𝑥}) ∈ Fin)
27 dmfi 8801 . . . . . . . . . . . . . . . . . . 19 ((𝐹 ∖ {𝑥}) ∈ Fin → dom (𝐹 ∖ {𝑥}) ∈ Fin)
2826, 27syl 17 . . . . . . . . . . . . . . . . . 18 (𝐹 ∈ Fin → dom (𝐹 ∖ {𝑥}) ∈ Fin)
29 hashcl 13724 . . . . . . . . . . . . . . . . . 18 (dom (𝐹 ∖ {𝑥}) ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) ∈ ℕ0)
3028, 29syl 17 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) ∈ ℕ0)
3130nn0red 11955 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) ∈ ℝ)
32 hashcl 13724 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∖ {𝑥}) ∈ Fin → (♯‘(𝐹 ∖ {𝑥})) ∈ ℕ0)
3326, 32syl 17 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {𝑥})) ∈ ℕ0)
3433nn0red 11955 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {𝑥})) ∈ ℝ)
35 peano2re 10813 . . . . . . . . . . . . . . . . 17 ((♯‘(𝐹 ∖ {𝑥})) ∈ ℝ → ((♯‘(𝐹 ∖ {𝑥})) + 1) ∈ ℝ)
3634, 35syl 17 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → ((♯‘(𝐹 ∖ {𝑥})) + 1) ∈ ℝ)
37 fidomdm 8800 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∖ {𝑥}) ∈ Fin → dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥}))
3826, 37syl 17 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ Fin → dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥}))
39 hashdom 13747 . . . . . . . . . . . . . . . . . 18 ((dom (𝐹 ∖ {𝑥}) ∈ Fin ∧ (𝐹 ∖ {𝑥}) ∈ Fin) → ((♯‘dom (𝐹 ∖ {𝑥})) ≤ (♯‘(𝐹 ∖ {𝑥})) ↔ dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥})))
4028, 26, 39syl2anc 587 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ Fin → ((♯‘dom (𝐹 ∖ {𝑥})) ≤ (♯‘(𝐹 ∖ {𝑥})) ↔ dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥})))
4138, 40mpbird 260 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) ≤ (♯‘(𝐹 ∖ {𝑥})))
4234ltp1d 11570 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {𝑥})) < ((♯‘(𝐹 ∖ {𝑥})) + 1))
4331, 34, 36, 41, 42lelttrd 10798 . . . . . . . . . . . . . . 15 (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) < ((♯‘(𝐹 ∖ {𝑥})) + 1))
44433ad2ant1 1130 . . . . . . . . . . . . . 14 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom (𝐹 ∖ {𝑥})) < ((♯‘(𝐹 ∖ {𝑥})) + 1))
4525, 44eqbrtrd 5075 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) < ((♯‘(𝐹 ∖ {𝑥})) + 1))
46 snfi 8592 . . . . . . . . . . . . . . . . 17 {𝑥} ∈ Fin
47 incom 4163 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∖ {𝑥}) ∩ {𝑥}) = ({𝑥} ∩ (𝐹 ∖ {𝑥}))
48 disjdif 4404 . . . . . . . . . . . . . . . . . 18 ({𝑥} ∩ (𝐹 ∖ {𝑥})) = ∅
4947, 48eqtri 2847 . . . . . . . . . . . . . . . . 17 ((𝐹 ∖ {𝑥}) ∩ {𝑥}) = ∅
50 hashun 13750 . . . . . . . . . . . . . . . . 17 (((𝐹 ∖ {𝑥}) ∈ Fin ∧ {𝑥} ∈ Fin ∧ ((𝐹 ∖ {𝑥}) ∩ {𝑥}) = ∅) → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥})))
5146, 49, 50mp3an23 1450 . . . . . . . . . . . . . . . 16 ((𝐹 ∖ {𝑥}) ∈ Fin → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥})))
5226, 51syl 17 . . . . . . . . . . . . . . 15 (𝐹 ∈ Fin → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥})))
53 hashsng 13737 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ V → (♯‘{𝑥}) = 1)
5453elv 3485 . . . . . . . . . . . . . . . 16 (♯‘{𝑥}) = 1
5554oveq2i 7162 . . . . . . . . . . . . . . 15 ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + 1)
5652, 55syl6req 2876 . . . . . . . . . . . . . 14 (𝐹 ∈ Fin → ((♯‘(𝐹 ∖ {𝑥})) + 1) = (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})))
57563ad2ant1 1130 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → ((♯‘(𝐹 ∖ {𝑥})) + 1) = (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})))
5845, 57breqtrd 5079 . . . . . . . . . . . 12 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) < (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})))
59 difsnid 4727 . . . . . . . . . . . . . . 15 (𝑥𝐹 → ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = 𝐹)
6059dmeqd 5762 . . . . . . . . . . . . . 14 (𝑥𝐹 → dom ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = dom 𝐹)
6160fveq2d 6667 . . . . . . . . . . . . 13 (𝑥𝐹 → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘dom 𝐹))
62613ad2ant2 1131 . . . . . . . . . . . 12 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘dom 𝐹))
6359fveq2d 6667 . . . . . . . . . . . . 13 (𝑥𝐹 → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘𝐹))
64633ad2ant2 1131 . . . . . . . . . . . 12 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘𝐹))
6558, 62, 643brtr3d 5084 . . . . . . . . . . 11 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom 𝐹) < (♯‘𝐹))
6665rexlimdv3a 3278 . . . . . . . . . 10 (𝐹 ∈ Fin → (∃𝑥𝐹 ¬ 𝑥 ∈ (V × V) → (♯‘dom 𝐹) < (♯‘𝐹)))
6714, 66syl5bi 245 . . . . . . . . 9 (𝐹 ∈ Fin → (¬ Rel 𝐹 → (♯‘dom 𝐹) < (♯‘𝐹)))
6867imp 410 . . . . . . . 8 ((𝐹 ∈ Fin ∧ ¬ Rel 𝐹) → (♯‘dom 𝐹) < (♯‘𝐹))
698, 68gtned 10775 . . . . . . 7 ((𝐹 ∈ Fin ∧ ¬ Rel 𝐹) → (♯‘𝐹) ≠ (♯‘dom 𝐹))
7069ex 416 . . . . . 6 (𝐹 ∈ Fin → (¬ Rel 𝐹 → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
7170necon4bd 3034 . . . . 5 (𝐹 ∈ Fin → ((♯‘𝐹) = (♯‘dom 𝐹) → Rel 𝐹))
7271imp 410 . . . 4 ((𝐹 ∈ Fin ∧ (♯‘𝐹) = (♯‘dom 𝐹)) → Rel 𝐹)
73 2nalexn 1829 . . . . . . . 8 (¬ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥𝑦 ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
74 df-ne 3015 . . . . . . . . . . . . 13 (𝑦𝑧 ↔ ¬ 𝑦 = 𝑧)
7574anbi2i 625 . . . . . . . . . . . 12 (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))
76 annim 407 . . . . . . . . . . . 12 (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧) ↔ ¬ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
7775, 76bitri 278 . . . . . . . . . . 11 (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧) ↔ ¬ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
7877exbii 1849 . . . . . . . . . 10 (∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧) ↔ ∃𝑧 ¬ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
79 exnal 1828 . . . . . . . . . 10 (∃𝑧 ¬ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
8078, 79bitr2i 279 . . . . . . . . 9 (¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧))
81802exbii 1850 . . . . . . . 8 (∃𝑥𝑦 ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧))
8273, 81bitri 278 . . . . . . 7 (¬ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧))
837adantr 484 . . . . . . . . . . 11 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘dom 𝐹) ∈ ℝ)
84 2re 11710 . . . . . . . . . . . . 13 2 ∈ ℝ
85 diffi 8749 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ Fin → (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin)
86 dmfi 8801 . . . . . . . . . . . . . . . . 17 ((𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin)
8785, 86syl 17 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin)
88 hashcl 13724 . . . . . . . . . . . . . . . 16 (dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℕ0)
8987, 88syl 17 . . . . . . . . . . . . . . 15 (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℕ0)
9089nn0red 11955 . . . . . . . . . . . . . 14 (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ)
9190adantr 484 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ)
92 readdcl 10620 . . . . . . . . . . . . 13 ((2 ∈ ℝ ∧ (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
9384, 91, 92sylancr 590 . . . . . . . . . . . 12 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
94 hashcl 13724 . . . . . . . . . . . . . 14 (𝐹 ∈ Fin → (♯‘𝐹) ∈ ℕ0)
9594nn0red 11955 . . . . . . . . . . . . 13 (𝐹 ∈ Fin → (♯‘𝐹) ∈ ℝ)
9695adantr 484 . . . . . . . . . . . 12 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘𝐹) ∈ ℝ)
97 1re 10641 . . . . . . . . . . . . . . 15 1 ∈ ℝ
98 readdcl 10620 . . . . . . . . . . . . . . 15 ((1 ∈ ℝ ∧ (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ) → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
9997, 90, 98sylancr 590 . . . . . . . . . . . . . 14 (𝐹 ∈ Fin → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
10099adantr 484 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
10184, 90, 92sylancr 590 . . . . . . . . . . . . . 14 (𝐹 ∈ Fin → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
102101adantr 484 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
103 dmun 5767 . . . . . . . . . . . . . . . . . 18 dom ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = (dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))
104 opex 5344 . . . . . . . . . . . . . . . . . . . . 21 𝑥, 𝑦⟩ ∈ V
105 opex 5344 . . . . . . . . . . . . . . . . . . . . 21 𝑥, 𝑧⟩ ∈ V
106104, 105prss 4737 . . . . . . . . . . . . . . . . . . . 20 ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ↔ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ⊆ 𝐹)
107 undif 4413 . . . . . . . . . . . . . . . . . . . 20 ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ⊆ 𝐹 ↔ ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = 𝐹)
108106, 107sylbb 222 . . . . . . . . . . . . . . . . . . 19 ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = 𝐹)
109108dmeqd 5762 . . . . . . . . . . . . . . . . . 18 ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → dom ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = dom 𝐹)
110103, 109syl5reqr 2874 . . . . . . . . . . . . . . . . 17 ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → dom 𝐹 = (dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
111 vex 3483 . . . . . . . . . . . . . . . . . . . 20 𝑦 ∈ V
112 vex 3483 . . . . . . . . . . . . . . . . . . . 20 𝑧 ∈ V
113111, 112dmprop 6063 . . . . . . . . . . . . . . . . . . 19 dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} = {𝑥, 𝑥}
114 dfsn2 4563 . . . . . . . . . . . . . . . . . . 19 {𝑥} = {𝑥, 𝑥}
115113, 114eqtr4i 2850 . . . . . . . . . . . . . . . . . 18 dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} = {𝑥}
116115uneq1i 4121 . . . . . . . . . . . . . . . . 17 (dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = ({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))
117110, 116syl6eq 2875 . . . . . . . . . . . . . . . 16 ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → dom 𝐹 = ({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
118117fveq2d 6667 . . . . . . . . . . . . . . 15 ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (♯‘dom 𝐹) = (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
119118ad2antrl 727 . . . . . . . . . . . . . 14 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘dom 𝐹) = (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
120 hashun2 13751 . . . . . . . . . . . . . . . . 17 (({𝑥} ∈ Fin ∧ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin) → (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ ((♯‘{𝑥}) + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
12146, 87, 120sylancr 590 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ ((♯‘{𝑥}) + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
12254oveq1i 7161 . . . . . . . . . . . . . . . 16 ((♯‘{𝑥}) + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
123121, 122breqtrdi 5094 . . . . . . . . . . . . . . 15 (𝐹 ∈ Fin → (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
124123adantr 484 . . . . . . . . . . . . . 14 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
125119, 124eqbrtrd 5075 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘dom 𝐹) ≤ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
126 1lt2 11807 . . . . . . . . . . . . . . 15 1 < 2
127 ltadd1 11107 . . . . . . . . . . . . . . . 16 ((1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ) → (1 < 2 ↔ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
12897, 84, 90, 127mp3an12i 1462 . . . . . . . . . . . . . . 15 (𝐹 ∈ Fin → (1 < 2 ↔ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
129126, 128mpbii 236 . . . . . . . . . . . . . 14 (𝐹 ∈ Fin → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
130129adantr 484 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
13183, 100, 102, 125, 130lelttrd 10798 . . . . . . . . . . . 12 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘dom 𝐹) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
132 fidomdm 8800 . . . . . . . . . . . . . . . . 17 ((𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ≼ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))
13385, 132syl 17 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ≼ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))
134 hashdom 13747 . . . . . . . . . . . . . . . . 17 ((dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin ∧ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin) → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ≼ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
13587, 85, 134syl2anc 587 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ≼ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
136133, 135mpbird 260 . . . . . . . . . . . . . . 15 (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
137 hashcl 13724 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℕ0)
13885, 137syl 17 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℕ0)
139138nn0red 11955 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ)
140 leadd2 11109 . . . . . . . . . . . . . . . . 17 (((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ ∧ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ ∧ 2 ∈ ℝ) → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
14184, 140mp3an3 1447 . . . . . . . . . . . . . . . 16 (((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ ∧ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ) → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
14290, 139, 141syl2anc 587 . . . . . . . . . . . . . . 15 (𝐹 ∈ Fin → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
143136, 142mpbid 235 . . . . . . . . . . . . . 14 (𝐹 ∈ Fin → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
144143adantr 484 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
145 prfi 8792 . . . . . . . . . . . . . . . . 17 {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∈ Fin
146 disjdif 4404 . . . . . . . . . . . . . . . . 17 ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∩ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = ∅
147 hashun 13750 . . . . . . . . . . . . . . . . 17 (({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∈ Fin ∧ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin ∧ ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∩ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = ∅) → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
148145, 146, 147mp3an13 1449 . . . . . . . . . . . . . . . 16 ((𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
14985, 148syl 17 . . . . . . . . . . . . . . 15 (𝐹 ∈ Fin → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
150149adantr 484 . . . . . . . . . . . . . 14 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
151108fveq2d 6667 . . . . . . . . . . . . . . 15 ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (♯‘𝐹))
152151ad2antrl 727 . . . . . . . . . . . . . 14 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (♯‘𝐹))
153 vex 3483 . . . . . . . . . . . . . . . . . . . 20 𝑥 ∈ V
154153, 111opth 5356 . . . . . . . . . . . . . . . . . . 19 (⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑧⟩ ↔ (𝑥 = 𝑥𝑦 = 𝑧))
155154simprbi 500 . . . . . . . . . . . . . . . . . 18 (⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑧⟩ → 𝑦 = 𝑧)
156155necon3i 3046 . . . . . . . . . . . . . . . . 17 (𝑦𝑧 → ⟨𝑥, 𝑦⟩ ≠ ⟨𝑥, 𝑧⟩)
157 hashprg 13763 . . . . . . . . . . . . . . . . . 18 ((⟨𝑥, 𝑦⟩ ∈ V ∧ ⟨𝑥, 𝑧⟩ ∈ V) → (⟨𝑥, 𝑦⟩ ≠ ⟨𝑥, 𝑧⟩ ↔ (♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) = 2))
158104, 105, 157mp2an 691 . . . . . . . . . . . . . . . . 17 (⟨𝑥, 𝑦⟩ ≠ ⟨𝑥, 𝑧⟩ ↔ (♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) = 2)
159156, 158sylib 221 . . . . . . . . . . . . . . . 16 (𝑦𝑧 → (♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) = 2)
160159oveq1d 7166 . . . . . . . . . . . . . . 15 (𝑦𝑧 → ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
161160ad2antll 728 . . . . . . . . . . . . . 14 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
162150, 152, 1613eqtr3rd 2868 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (♯‘𝐹))
163144, 162breqtrd 5079 . . . . . . . . . . . 12 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (♯‘𝐹))
16483, 93, 96, 131, 163ltletrd 10800 . . . . . . . . . . 11 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘dom 𝐹) < (♯‘𝐹))
16583, 164gtned 10775 . . . . . . . . . 10 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘𝐹) ≠ (♯‘dom 𝐹))
166165ex 416 . . . . . . . . 9 (𝐹 ∈ Fin → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
167166exlimdv 1935 . . . . . . . 8 (𝐹 ∈ Fin → (∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
168167exlimdvv 1936 . . . . . . 7 (𝐹 ∈ Fin → (∃𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
16982, 168syl5bi 245 . . . . . 6 (𝐹 ∈ Fin → (¬ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
170169necon4bd 3034 . . . . 5 (𝐹 ∈ Fin → ((♯‘𝐹) = (♯‘dom 𝐹) → ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
171170imp 410 . . . 4 ((𝐹 ∈ Fin ∧ (♯‘𝐹) = (♯‘dom 𝐹)) → ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
172 dffun4 6357 . . . 4 (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
17372, 171, 172sylanbrc 586 . . 3 ((𝐹 ∈ Fin ∧ (♯‘𝐹) = (♯‘dom 𝐹)) → Fun 𝐹)
174173ex 416 . 2 (𝐹 ∈ Fin → ((♯‘𝐹) = (♯‘dom 𝐹) → Fun 𝐹))
1753, 174impbid2 229 1 (𝐹 ∈ Fin → (Fun 𝐹 ↔ (♯‘𝐹) = (♯‘dom 𝐹)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1084  wal 1536   = wceq 1538  wex 1781  wcel 2115  wne 3014  wral 3133  wrex 3134  Vcvv 3480  cdif 3916  cun 3917  cin 3918  wss 3919  c0 4276  {csn 4550  {cpr 4552  cop 4556   class class class wbr 5053   × cxp 5541  dom cdm 5543  Rel wrel 5548  Fun wfun 6339   Fn wfn 6340  cfv 6345  (class class class)co 7151  cdom 8505  Fincfn 8507  cr 10536  1c1 10538   + caddc 10540   < clt 10675  cle 10676  2c2 11691  0cn0 11896  chash 13697
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5177  ax-sep 5190  ax-nul 5197  ax-pow 5254  ax-pr 5318  ax-un 7457  ax-cnex 10593  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613  ax-pre-mulgt0 10614
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-int 4863  df-iun 4907  df-br 5054  df-opab 5116  df-mpt 5134  df-tr 5160  df-id 5448  df-eprel 5453  df-po 5462  df-so 5463  df-fr 5502  df-we 5504  df-xp 5549  df-rel 5550  df-cnv 5551  df-co 5552  df-dm 5553  df-rn 5554  df-res 5555  df-ima 5556  df-pred 6137  df-ord 6183  df-on 6184  df-lim 6185  df-suc 6186  df-iota 6304  df-fun 6347  df-fn 6348  df-f 6349  df-f1 6350  df-fo 6351  df-f1o 6352  df-fv 6353  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7577  df-1st 7686  df-2nd 7687  df-wrecs 7945  df-recs 8006  df-rdg 8044  df-1o 8100  df-oadd 8104  df-er 8287  df-en 8508  df-dom 8509  df-sdom 8510  df-fin 8511  df-dju 9329  df-card 9367  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-sub 10872  df-neg 10873  df-nn 11637  df-2 11699  df-n0 11897  df-xnn0 11967  df-z 11981  df-uz 12243  df-fz 12897  df-hash 13698
This theorem is referenced by:  hashres  13806  hashreshashfun  13807  ccatalpha  13949  cycpmconjslem2  30839  hashfundm  32439
  Copyright terms: Public domain W3C validator