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

Theorem hashfun 14472
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 6597 . . 3 (Fun 𝐹𝐹 Fn dom 𝐹)
2 hashfn 14410 . . 3 (𝐹 Fn dom 𝐹 → (♯‘𝐹) = (♯‘dom 𝐹))
31, 2sylbi 217 . 2 (Fun 𝐹 → (♯‘𝐹) = (♯‘dom 𝐹))
4 dmfi 9372 . . . . . . . . . . 11 (𝐹 ∈ Fin → dom 𝐹 ∈ Fin)
5 hashcl 14391 . . . . . . . . . . 11 (dom 𝐹 ∈ Fin → (♯‘dom 𝐹) ∈ ℕ0)
64, 5syl 17 . . . . . . . . . 10 (𝐹 ∈ Fin → (♯‘dom 𝐹) ∈ ℕ0)
76nn0red 12585 . . . . . . . . 9 (𝐹 ∈ Fin → (♯‘dom 𝐹) ∈ ℝ)
87adantr 480 . . . . . . . 8 ((𝐹 ∈ Fin ∧ ¬ Rel 𝐹) → (♯‘dom 𝐹) ∈ ℝ)
9 df-rel 5695 . . . . . . . . . . . . 13 (Rel 𝐹𝐹 ⊆ (V × V))
10 dfss3 3983 . . . . . . . . . . . . 13 (𝐹 ⊆ (V × V) ↔ ∀𝑥𝐹 𝑥 ∈ (V × V))
119, 10bitri 275 . . . . . . . . . . . 12 (Rel 𝐹 ↔ ∀𝑥𝐹 𝑥 ∈ (V × V))
1211notbii 320 . . . . . . . . . . 11 (¬ Rel 𝐹 ↔ ¬ ∀𝑥𝐹 𝑥 ∈ (V × V))
13 rexnal 3097 . . . . . . . . . . 11 (∃𝑥𝐹 ¬ 𝑥 ∈ (V × V) ↔ ¬ ∀𝑥𝐹 𝑥 ∈ (V × V))
1412, 13bitr4i 278 . . . . . . . . . 10 (¬ Rel 𝐹 ↔ ∃𝑥𝐹 ¬ 𝑥 ∈ (V × V))
15 dmun 5923 . . . . . . . . . . . . . . . 16 dom ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥})
1615fveq2i 6909 . . . . . . . . . . . . . . 15 (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘(dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}))
17 dmsnn0 6228 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (V × V) ↔ dom {𝑥} ≠ ∅)
1817biimpri 228 . . . . . . . . . . . . . . . . . . . 20 (dom {𝑥} ≠ ∅ → 𝑥 ∈ (V × V))
1918necon1bi 2966 . . . . . . . . . . . . . . . . . . 19 𝑥 ∈ (V × V) → dom {𝑥} = ∅)
20193ad2ant3 1134 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → dom {𝑥} = ∅)
2120uneq2d 4177 . . . . . . . . . . . . . . . . 17 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}) = (dom (𝐹 ∖ {𝑥}) ∪ ∅))
22 un0 4399 . . . . . . . . . . . . . . . . 17 (dom (𝐹 ∖ {𝑥}) ∪ ∅) = dom (𝐹 ∖ {𝑥})
2321, 22eqtrdi 2790 . . . . . . . . . . . . . . . 16 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}) = dom (𝐹 ∖ {𝑥}))
2423fveq2d 6910 . . . . . . . . . . . . . . 15 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘(dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥})) = (♯‘dom (𝐹 ∖ {𝑥})))
2516, 24eqtrid 2786 . . . . . . . . . . . . . 14 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘dom (𝐹 ∖ {𝑥})))
26 diffi 9213 . . . . . . . . . . . . . . . . . . 19 (𝐹 ∈ Fin → (𝐹 ∖ {𝑥}) ∈ Fin)
27 dmfi 9372 . . . . . . . . . . . . . . . . . . 19 ((𝐹 ∖ {𝑥}) ∈ Fin → dom (𝐹 ∖ {𝑥}) ∈ Fin)
2826, 27syl 17 . . . . . . . . . . . . . . . . . 18 (𝐹 ∈ Fin → dom (𝐹 ∖ {𝑥}) ∈ Fin)
29 hashcl 14391 . . . . . . . . . . . . . . . . . 18 (dom (𝐹 ∖ {𝑥}) ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) ∈ ℕ0)
3028, 29syl 17 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) ∈ ℕ0)
3130nn0red 12585 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) ∈ ℝ)
32 hashcl 14391 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∖ {𝑥}) ∈ Fin → (♯‘(𝐹 ∖ {𝑥})) ∈ ℕ0)
3326, 32syl 17 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {𝑥})) ∈ ℕ0)
3433nn0red 12585 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {𝑥})) ∈ ℝ)
35 peano2re 11431 . . . . . . . . . . . . . . . . 17 ((♯‘(𝐹 ∖ {𝑥})) ∈ ℝ → ((♯‘(𝐹 ∖ {𝑥})) + 1) ∈ ℝ)
3634, 35syl 17 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → ((♯‘(𝐹 ∖ {𝑥})) + 1) ∈ ℝ)
37 fidomdm 9371 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∖ {𝑥}) ∈ Fin → dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥}))
3826, 37syl 17 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ Fin → dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥}))
39 hashdom 14414 . . . . . . . . . . . . . . . . . 18 ((dom (𝐹 ∖ {𝑥}) ∈ Fin ∧ (𝐹 ∖ {𝑥}) ∈ Fin) → ((♯‘dom (𝐹 ∖ {𝑥})) ≤ (♯‘(𝐹 ∖ {𝑥})) ↔ dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥})))
4028, 26, 39syl2anc 584 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ Fin → ((♯‘dom (𝐹 ∖ {𝑥})) ≤ (♯‘(𝐹 ∖ {𝑥})) ↔ dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥})))
4138, 40mpbird 257 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) ≤ (♯‘(𝐹 ∖ {𝑥})))
4234ltp1d 12195 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {𝑥})) < ((♯‘(𝐹 ∖ {𝑥})) + 1))
4331, 34, 36, 41, 42lelttrd 11416 . . . . . . . . . . . . . . 15 (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) < ((♯‘(𝐹 ∖ {𝑥})) + 1))
44433ad2ant1 1132 . . . . . . . . . . . . . 14 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom (𝐹 ∖ {𝑥})) < ((♯‘(𝐹 ∖ {𝑥})) + 1))
4525, 44eqbrtrd 5169 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) < ((♯‘(𝐹 ∖ {𝑥})) + 1))
46 snfi 9081 . . . . . . . . . . . . . . . . 17 {𝑥} ∈ Fin
47 disjdifr 4478 . . . . . . . . . . . . . . . . 17 ((𝐹 ∖ {𝑥}) ∩ {𝑥}) = ∅
48 hashun 14417 . . . . . . . . . . . . . . . . 17 (((𝐹 ∖ {𝑥}) ∈ Fin ∧ {𝑥} ∈ Fin ∧ ((𝐹 ∖ {𝑥}) ∩ {𝑥}) = ∅) → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥})))
4946, 47, 48mp3an23 1452 . . . . . . . . . . . . . . . 16 ((𝐹 ∖ {𝑥}) ∈ Fin → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥})))
5026, 49syl 17 . . . . . . . . . . . . . . 15 (𝐹 ∈ Fin → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥})))
51 hashsng 14404 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ V → (♯‘{𝑥}) = 1)
5251elv 3482 . . . . . . . . . . . . . . . 16 (♯‘{𝑥}) = 1
5352oveq2i 7441 . . . . . . . . . . . . . . 15 ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + 1)
5450, 53eqtr2di 2791 . . . . . . . . . . . . . 14 (𝐹 ∈ Fin → ((♯‘(𝐹 ∖ {𝑥})) + 1) = (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})))
55543ad2ant1 1132 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → ((♯‘(𝐹 ∖ {𝑥})) + 1) = (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})))
5645, 55breqtrd 5173 . . . . . . . . . . . 12 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) < (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})))
57 difsnid 4814 . . . . . . . . . . . . . . 15 (𝑥𝐹 → ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = 𝐹)
5857dmeqd 5918 . . . . . . . . . . . . . 14 (𝑥𝐹 → dom ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = dom 𝐹)
5958fveq2d 6910 . . . . . . . . . . . . 13 (𝑥𝐹 → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘dom 𝐹))
60593ad2ant2 1133 . . . . . . . . . . . 12 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘dom 𝐹))
6157fveq2d 6910 . . . . . . . . . . . . 13 (𝑥𝐹 → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘𝐹))
62613ad2ant2 1133 . . . . . . . . . . . 12 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘𝐹))
6356, 60, 623brtr3d 5178 . . . . . . . . . . 11 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom 𝐹) < (♯‘𝐹))
6463rexlimdv3a 3156 . . . . . . . . . 10 (𝐹 ∈ Fin → (∃𝑥𝐹 ¬ 𝑥 ∈ (V × V) → (♯‘dom 𝐹) < (♯‘𝐹)))
6514, 64biimtrid 242 . . . . . . . . 9 (𝐹 ∈ Fin → (¬ Rel 𝐹 → (♯‘dom 𝐹) < (♯‘𝐹)))
6665imp 406 . . . . . . . 8 ((𝐹 ∈ Fin ∧ ¬ Rel 𝐹) → (♯‘dom 𝐹) < (♯‘𝐹))
678, 66gtned 11393 . . . . . . 7 ((𝐹 ∈ Fin ∧ ¬ Rel 𝐹) → (♯‘𝐹) ≠ (♯‘dom 𝐹))
6867ex 412 . . . . . 6 (𝐹 ∈ Fin → (¬ Rel 𝐹 → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
6968necon4bd 2957 . . . . 5 (𝐹 ∈ Fin → ((♯‘𝐹) = (♯‘dom 𝐹) → Rel 𝐹))
7069imp 406 . . . 4 ((𝐹 ∈ Fin ∧ (♯‘𝐹) = (♯‘dom 𝐹)) → Rel 𝐹)
71 2nalexn 1824 . . . . . . . 8 (¬ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥𝑦 ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
72 df-ne 2938 . . . . . . . . . . . . 13 (𝑦𝑧 ↔ ¬ 𝑦 = 𝑧)
7372anbi2i 623 . . . . . . . . . . . 12 (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))
74 annim 403 . . . . . . . . . . . 12 (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧) ↔ ¬ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
7573, 74bitri 275 . . . . . . . . . . 11 (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧) ↔ ¬ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
7675exbii 1844 . . . . . . . . . 10 (∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧) ↔ ∃𝑧 ¬ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
77 exnal 1823 . . . . . . . . . 10 (∃𝑧 ¬ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
7876, 77bitr2i 276 . . . . . . . . 9 (¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧))
79782exbii 1845 . . . . . . . 8 (∃𝑥𝑦 ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧))
8071, 79bitri 275 . . . . . . 7 (¬ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧))
817adantr 480 . . . . . . . . . . 11 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘dom 𝐹) ∈ ℝ)
82 2re 12337 . . . . . . . . . . . . 13 2 ∈ ℝ
83 diffi 9213 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ Fin → (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin)
84 dmfi 9372 . . . . . . . . . . . . . . . . 17 ((𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin)
8583, 84syl 17 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin)
86 hashcl 14391 . . . . . . . . . . . . . . . 16 (dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℕ0)
8785, 86syl 17 . . . . . . . . . . . . . . 15 (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℕ0)
8887nn0red 12585 . . . . . . . . . . . . . 14 (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ)
8988adantr 480 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ)
90 readdcl 11235 . . . . . . . . . . . . 13 ((2 ∈ ℝ ∧ (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
9182, 89, 90sylancr 587 . . . . . . . . . . . 12 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
92 hashcl 14391 . . . . . . . . . . . . . 14 (𝐹 ∈ Fin → (♯‘𝐹) ∈ ℕ0)
9392nn0red 12585 . . . . . . . . . . . . 13 (𝐹 ∈ Fin → (♯‘𝐹) ∈ ℝ)
9493adantr 480 . . . . . . . . . . . 12 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘𝐹) ∈ ℝ)
95 1re 11258 . . . . . . . . . . . . . . 15 1 ∈ ℝ
96 readdcl 11235 . . . . . . . . . . . . . . 15 ((1 ∈ ℝ ∧ (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ) → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
9795, 88, 96sylancr 587 . . . . . . . . . . . . . 14 (𝐹 ∈ Fin → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
9897adantr 480 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
9982, 88, 90sylancr 587 . . . . . . . . . . . . . 14 (𝐹 ∈ Fin → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
10099adantr 480 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
101 opex 5474 . . . . . . . . . . . . . . . . . . . . 21 𝑥, 𝑦⟩ ∈ V
102 opex 5474 . . . . . . . . . . . . . . . . . . . . 21 𝑥, 𝑧⟩ ∈ V
103101, 102prss 4824 . . . . . . . . . . . . . . . . . . . 20 ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ↔ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ⊆ 𝐹)
104 undif 4487 . . . . . . . . . . . . . . . . . . . 20 ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ⊆ 𝐹 ↔ ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = 𝐹)
105103, 104sylbb 219 . . . . . . . . . . . . . . . . . . 19 ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = 𝐹)
106105dmeqd 5918 . . . . . . . . . . . . . . . . . 18 ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → dom ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = dom 𝐹)
107 dmun 5923 . . . . . . . . . . . . . . . . . 18 dom ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = (dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))
108106, 107eqtr3di 2789 . . . . . . . . . . . . . . . . 17 ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → dom 𝐹 = (dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
109 vex 3481 . . . . . . . . . . . . . . . . . . . 20 𝑦 ∈ V
110 vex 3481 . . . . . . . . . . . . . . . . . . . 20 𝑧 ∈ V
111109, 110dmprop 6238 . . . . . . . . . . . . . . . . . . 19 dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} = {𝑥, 𝑥}
112 dfsn2 4643 . . . . . . . . . . . . . . . . . . 19 {𝑥} = {𝑥, 𝑥}
113111, 112eqtr4i 2765 . . . . . . . . . . . . . . . . . 18 dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} = {𝑥}
114113uneq1i 4173 . . . . . . . . . . . . . . . . 17 (dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = ({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))
115108, 114eqtrdi 2790 . . . . . . . . . . . . . . . 16 ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → dom 𝐹 = ({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
116115fveq2d 6910 . . . . . . . . . . . . . . 15 ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (♯‘dom 𝐹) = (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
117116ad2antrl 728 . . . . . . . . . . . . . 14 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘dom 𝐹) = (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
118 hashun2 14418 . . . . . . . . . . . . . . . . 17 (({𝑥} ∈ Fin ∧ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin) → (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ ((♯‘{𝑥}) + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
11946, 85, 118sylancr 587 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ ((♯‘{𝑥}) + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
12052oveq1i 7440 . . . . . . . . . . . . . . . 16 ((♯‘{𝑥}) + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
121119, 120breqtrdi 5188 . . . . . . . . . . . . . . 15 (𝐹 ∈ Fin → (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
122121adantr 480 . . . . . . . . . . . . . 14 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
123117, 122eqbrtrd 5169 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘dom 𝐹) ≤ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
124 1lt2 12434 . . . . . . . . . . . . . . 15 1 < 2
125 ltadd1 11727 . . . . . . . . . . . . . . . 16 ((1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ) → (1 < 2 ↔ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
12695, 82, 88, 125mp3an12i 1464 . . . . . . . . . . . . . . 15 (𝐹 ∈ Fin → (1 < 2 ↔ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
127124, 126mpbii 233 . . . . . . . . . . . . . 14 (𝐹 ∈ Fin → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
128127adantr 480 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
12981, 98, 100, 123, 128lelttrd 11416 . . . . . . . . . . . 12 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘dom 𝐹) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
130 fidomdm 9371 . . . . . . . . . . . . . . . . 17 ((𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ≼ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))
13183, 130syl 17 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ≼ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))
132 hashdom 14414 . . . . . . . . . . . . . . . . 17 ((dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin ∧ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin) → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ≼ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
13385, 83, 132syl2anc 584 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ≼ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
134131, 133mpbird 257 . . . . . . . . . . . . . . 15 (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
135 hashcl 14391 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℕ0)
13683, 135syl 17 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℕ0)
137136nn0red 12585 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ)
138 leadd2 11729 . . . . . . . . . . . . . . . . 17 (((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ ∧ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ ∧ 2 ∈ ℝ) → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
13982, 138mp3an3 1449 . . . . . . . . . . . . . . . 16 (((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ ∧ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ) → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
14088, 137, 139syl2anc 584 . . . . . . . . . . . . . . 15 (𝐹 ∈ Fin → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
141134, 140mpbid 232 . . . . . . . . . . . . . 14 (𝐹 ∈ Fin → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
142141adantr 480 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
143 prfi 9360 . . . . . . . . . . . . . . . . 17 {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∈ Fin
144 disjdif 4477 . . . . . . . . . . . . . . . . 17 ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∩ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = ∅
145 hashun 14417 . . . . . . . . . . . . . . . . 17 (({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∈ Fin ∧ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin ∧ ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∩ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = ∅) → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
146143, 144, 145mp3an13 1451 . . . . . . . . . . . . . . . 16 ((𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
14783, 146syl 17 . . . . . . . . . . . . . . 15 (𝐹 ∈ Fin → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
148147adantr 480 . . . . . . . . . . . . . 14 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
149105fveq2d 6910 . . . . . . . . . . . . . . 15 ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (♯‘𝐹))
150149ad2antrl 728 . . . . . . . . . . . . . 14 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (♯‘𝐹))
151 vex 3481 . . . . . . . . . . . . . . . . . . . 20 𝑥 ∈ V
152151, 109opth 5486 . . . . . . . . . . . . . . . . . . 19 (⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑧⟩ ↔ (𝑥 = 𝑥𝑦 = 𝑧))
153152simprbi 496 . . . . . . . . . . . . . . . . . 18 (⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑧⟩ → 𝑦 = 𝑧)
154153necon3i 2970 . . . . . . . . . . . . . . . . 17 (𝑦𝑧 → ⟨𝑥, 𝑦⟩ ≠ ⟨𝑥, 𝑧⟩)
155 hashprg 14430 . . . . . . . . . . . . . . . . . 18 ((⟨𝑥, 𝑦⟩ ∈ V ∧ ⟨𝑥, 𝑧⟩ ∈ V) → (⟨𝑥, 𝑦⟩ ≠ ⟨𝑥, 𝑧⟩ ↔ (♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) = 2))
156101, 102, 155mp2an 692 . . . . . . . . . . . . . . . . 17 (⟨𝑥, 𝑦⟩ ≠ ⟨𝑥, 𝑧⟩ ↔ (♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) = 2)
157154, 156sylib 218 . . . . . . . . . . . . . . . 16 (𝑦𝑧 → (♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) = 2)
158157oveq1d 7445 . . . . . . . . . . . . . . 15 (𝑦𝑧 → ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
159158ad2antll 729 . . . . . . . . . . . . . 14 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
160148, 150, 1593eqtr3rd 2783 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (♯‘𝐹))
161142, 160breqtrd 5173 . . . . . . . . . . . 12 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (♯‘𝐹))
16281, 91, 94, 129, 161ltletrd 11418 . . . . . . . . . . 11 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘dom 𝐹) < (♯‘𝐹))
16381, 162gtned 11393 . . . . . . . . . 10 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘𝐹) ≠ (♯‘dom 𝐹))
164163ex 412 . . . . . . . . 9 (𝐹 ∈ Fin → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
165164exlimdv 1930 . . . . . . . 8 (𝐹 ∈ Fin → (∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
166165exlimdvv 1931 . . . . . . 7 (𝐹 ∈ Fin → (∃𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
16780, 166biimtrid 242 . . . . . 6 (𝐹 ∈ Fin → (¬ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
168167necon4bd 2957 . . . . 5 (𝐹 ∈ Fin → ((♯‘𝐹) = (♯‘dom 𝐹) → ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
169168imp 406 . . . 4 ((𝐹 ∈ Fin ∧ (♯‘𝐹) = (♯‘dom 𝐹)) → ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
170 dffun4 6578 . . . 4 (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
17170, 169, 170sylanbrc 583 . . 3 ((𝐹 ∈ Fin ∧ (♯‘𝐹) = (♯‘dom 𝐹)) → Fun 𝐹)
172171ex 412 . 2 (𝐹 ∈ Fin → ((♯‘𝐹) = (♯‘dom 𝐹) → Fun 𝐹))
1733, 172impbid2 226 1 (𝐹 ∈ Fin → (Fun 𝐹 ↔ (♯‘𝐹) = (♯‘dom 𝐹)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086  wal 1534   = wceq 1536  wex 1775  wcel 2105  wne 2937  wral 3058  wrex 3067  Vcvv 3477  cdif 3959  cun 3960  cin 3961  wss 3962  c0 4338  {csn 4630  {cpr 4632  cop 4636   class class class wbr 5147   × cxp 5686  dom cdm 5688  Rel wrel 5693  Fun wfun 6556   Fn wfn 6557  cfv 6562  (class class class)co 7430  cdom 8981  Fincfn 8983  cr 11151  1c1 11153   + caddc 11155   < clt 11292  cle 11293  2c2 12318  0cn0 12523  chash 14365
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-2o 8505  df-oadd 8508  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-dju 9938  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-nn 12264  df-2 12326  df-n0 12524  df-xnn0 12597  df-z 12611  df-uz 12876  df-fz 13544  df-hash 14366
This theorem is referenced by:  hashres  14473  hashreshashfun  14474  hashfundm  14477  ccatalpha  14627  cycpmconjslem2  33157
  Copyright terms: Public domain W3C validator