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

Theorem hashfun 13436
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 6079 . . 3 (Fun 𝐹𝐹 Fn dom 𝐹)
2 hashfn 13376 . . 3 (𝐹 Fn dom 𝐹 → (♯‘𝐹) = (♯‘dom 𝐹))
31, 2sylbi 207 . 2 (Fun 𝐹 → (♯‘𝐹) = (♯‘dom 𝐹))
4 dmfi 8411 . . . . . . . . . . 11 (𝐹 ∈ Fin → dom 𝐹 ∈ Fin)
5 hashcl 13359 . . . . . . . . . . 11 (dom 𝐹 ∈ Fin → (♯‘dom 𝐹) ∈ ℕ0)
64, 5syl 17 . . . . . . . . . 10 (𝐹 ∈ Fin → (♯‘dom 𝐹) ∈ ℕ0)
76nn0red 11564 . . . . . . . . 9 (𝐹 ∈ Fin → (♯‘dom 𝐹) ∈ ℝ)
87adantr 472 . . . . . . . 8 ((𝐹 ∈ Fin ∧ ¬ Rel 𝐹) → (♯‘dom 𝐹) ∈ ℝ)
9 df-rel 5273 . . . . . . . . . . . . 13 (Rel 𝐹𝐹 ⊆ (V × V))
10 dfss3 3733 . . . . . . . . . . . . 13 (𝐹 ⊆ (V × V) ↔ ∀𝑥𝐹 𝑥 ∈ (V × V))
119, 10bitri 264 . . . . . . . . . . . 12 (Rel 𝐹 ↔ ∀𝑥𝐹 𝑥 ∈ (V × V))
1211notbii 309 . . . . . . . . . . 11 (¬ Rel 𝐹 ↔ ¬ ∀𝑥𝐹 𝑥 ∈ (V × V))
13 rexnal 3133 . . . . . . . . . . 11 (∃𝑥𝐹 ¬ 𝑥 ∈ (V × V) ↔ ¬ ∀𝑥𝐹 𝑥 ∈ (V × V))
1412, 13bitr4i 267 . . . . . . . . . 10 (¬ Rel 𝐹 ↔ ∃𝑥𝐹 ¬ 𝑥 ∈ (V × V))
15 dmun 5486 . . . . . . . . . . . . . . . 16 dom ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥})
1615fveq2i 6356 . . . . . . . . . . . . . . 15 (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘(dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}))
17 dmsnn0 5758 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (V × V) ↔ dom {𝑥} ≠ ∅)
1817biimpri 218 . . . . . . . . . . . . . . . . . . . 20 (dom {𝑥} ≠ ∅ → 𝑥 ∈ (V × V))
1918necon1bi 2960 . . . . . . . . . . . . . . . . . . 19 𝑥 ∈ (V × V) → dom {𝑥} = ∅)
20193ad2ant3 1130 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → dom {𝑥} = ∅)
2120uneq2d 3910 . . . . . . . . . . . . . . . . 17 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}) = (dom (𝐹 ∖ {𝑥}) ∪ ∅))
22 un0 4110 . . . . . . . . . . . . . . . . 17 (dom (𝐹 ∖ {𝑥}) ∪ ∅) = dom (𝐹 ∖ {𝑥})
2321, 22syl6eq 2810 . . . . . . . . . . . . . . . 16 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}) = dom (𝐹 ∖ {𝑥}))
2423fveq2d 6357 . . . . . . . . . . . . . . 15 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘(dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥})) = (♯‘dom (𝐹 ∖ {𝑥})))
2516, 24syl5eq 2806 . . . . . . . . . . . . . 14 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘dom (𝐹 ∖ {𝑥})))
26 diffi 8359 . . . . . . . . . . . . . . . . . . 19 (𝐹 ∈ Fin → (𝐹 ∖ {𝑥}) ∈ Fin)
27 dmfi 8411 . . . . . . . . . . . . . . . . . . 19 ((𝐹 ∖ {𝑥}) ∈ Fin → dom (𝐹 ∖ {𝑥}) ∈ Fin)
2826, 27syl 17 . . . . . . . . . . . . . . . . . 18 (𝐹 ∈ Fin → dom (𝐹 ∖ {𝑥}) ∈ Fin)
29 hashcl 13359 . . . . . . . . . . . . . . . . . 18 (dom (𝐹 ∖ {𝑥}) ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) ∈ ℕ0)
3028, 29syl 17 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) ∈ ℕ0)
3130nn0red 11564 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) ∈ ℝ)
32 hashcl 13359 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∖ {𝑥}) ∈ Fin → (♯‘(𝐹 ∖ {𝑥})) ∈ ℕ0)
3326, 32syl 17 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {𝑥})) ∈ ℕ0)
3433nn0red 11564 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {𝑥})) ∈ ℝ)
35 peano2re 10421 . . . . . . . . . . . . . . . . 17 ((♯‘(𝐹 ∖ {𝑥})) ∈ ℝ → ((♯‘(𝐹 ∖ {𝑥})) + 1) ∈ ℝ)
3634, 35syl 17 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → ((♯‘(𝐹 ∖ {𝑥})) + 1) ∈ ℝ)
37 fidomdm 8410 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∖ {𝑥}) ∈ Fin → dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥}))
3826, 37syl 17 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ Fin → dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥}))
39 hashdom 13380 . . . . . . . . . . . . . . . . . 18 ((dom (𝐹 ∖ {𝑥}) ∈ Fin ∧ (𝐹 ∖ {𝑥}) ∈ Fin) → ((♯‘dom (𝐹 ∖ {𝑥})) ≤ (♯‘(𝐹 ∖ {𝑥})) ↔ dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥})))
4028, 26, 39syl2anc 696 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ Fin → ((♯‘dom (𝐹 ∖ {𝑥})) ≤ (♯‘(𝐹 ∖ {𝑥})) ↔ dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥})))
4138, 40mpbird 247 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) ≤ (♯‘(𝐹 ∖ {𝑥})))
4234ltp1d 11166 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {𝑥})) < ((♯‘(𝐹 ∖ {𝑥})) + 1))
4331, 34, 36, 41, 42lelttrd 10407 . . . . . . . . . . . . . . 15 (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {𝑥})) < ((♯‘(𝐹 ∖ {𝑥})) + 1))
44433ad2ant1 1128 . . . . . . . . . . . . . 14 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom (𝐹 ∖ {𝑥})) < ((♯‘(𝐹 ∖ {𝑥})) + 1))
4525, 44eqbrtrd 4826 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) < ((♯‘(𝐹 ∖ {𝑥})) + 1))
46 snfi 8205 . . . . . . . . . . . . . . . . 17 {𝑥} ∈ Fin
47 incom 3948 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∖ {𝑥}) ∩ {𝑥}) = ({𝑥} ∩ (𝐹 ∖ {𝑥}))
48 disjdif 4184 . . . . . . . . . . . . . . . . . 18 ({𝑥} ∩ (𝐹 ∖ {𝑥})) = ∅
4947, 48eqtri 2782 . . . . . . . . . . . . . . . . 17 ((𝐹 ∖ {𝑥}) ∩ {𝑥}) = ∅
50 hashun 13383 . . . . . . . . . . . . . . . . 17 (((𝐹 ∖ {𝑥}) ∈ Fin ∧ {𝑥} ∈ Fin ∧ ((𝐹 ∖ {𝑥}) ∩ {𝑥}) = ∅) → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥})))
5146, 49, 50mp3an23 1565 . . . . . . . . . . . . . . . 16 ((𝐹 ∖ {𝑥}) ∈ Fin → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥})))
5226, 51syl 17 . . . . . . . . . . . . . . 15 (𝐹 ∈ Fin → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥})))
53 vex 3343 . . . . . . . . . . . . . . . . 17 𝑥 ∈ V
54 hashsng 13371 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ V → (♯‘{𝑥}) = 1)
5553, 54ax-mp 5 . . . . . . . . . . . . . . . 16 (♯‘{𝑥}) = 1
5655oveq2i 6825 . . . . . . . . . . . . . . 15 ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + 1)
5752, 56syl6req 2811 . . . . . . . . . . . . . 14 (𝐹 ∈ Fin → ((♯‘(𝐹 ∖ {𝑥})) + 1) = (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})))
58573ad2ant1 1128 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → ((♯‘(𝐹 ∖ {𝑥})) + 1) = (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})))
5945, 58breqtrd 4830 . . . . . . . . . . . 12 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) < (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})))
60 difsnid 4486 . . . . . . . . . . . . . . 15 (𝑥𝐹 → ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = 𝐹)
6160dmeqd 5481 . . . . . . . . . . . . . 14 (𝑥𝐹 → dom ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = dom 𝐹)
6261fveq2d 6357 . . . . . . . . . . . . 13 (𝑥𝐹 → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘dom 𝐹))
63623ad2ant2 1129 . . . . . . . . . . . 12 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘dom 𝐹))
6460fveq2d 6357 . . . . . . . . . . . . 13 (𝑥𝐹 → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘𝐹))
65643ad2ant2 1129 . . . . . . . . . . . 12 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘𝐹))
6659, 63, 653brtr3d 4835 . . . . . . . . . . 11 ((𝐹 ∈ Fin ∧ 𝑥𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (♯‘dom 𝐹) < (♯‘𝐹))
6766rexlimdv3a 3171 . . . . . . . . . 10 (𝐹 ∈ Fin → (∃𝑥𝐹 ¬ 𝑥 ∈ (V × V) → (♯‘dom 𝐹) < (♯‘𝐹)))
6814, 67syl5bi 232 . . . . . . . . 9 (𝐹 ∈ Fin → (¬ Rel 𝐹 → (♯‘dom 𝐹) < (♯‘𝐹)))
6968imp 444 . . . . . . . 8 ((𝐹 ∈ Fin ∧ ¬ Rel 𝐹) → (♯‘dom 𝐹) < (♯‘𝐹))
708, 69gtned 10384 . . . . . . 7 ((𝐹 ∈ Fin ∧ ¬ Rel 𝐹) → (♯‘𝐹) ≠ (♯‘dom 𝐹))
7170ex 449 . . . . . 6 (𝐹 ∈ Fin → (¬ Rel 𝐹 → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
7271necon4bd 2952 . . . . 5 (𝐹 ∈ Fin → ((♯‘𝐹) = (♯‘dom 𝐹) → Rel 𝐹))
7372imp 444 . . . 4 ((𝐹 ∈ Fin ∧ (♯‘𝐹) = (♯‘dom 𝐹)) → Rel 𝐹)
74 2nalexn 1904 . . . . . . . 8 (¬ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥𝑦 ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
75 df-ne 2933 . . . . . . . . . . . . 13 (𝑦𝑧 ↔ ¬ 𝑦 = 𝑧)
7675anbi2i 732 . . . . . . . . . . . 12 (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧))
77 annim 440 . . . . . . . . . . . 12 (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧) ↔ ¬ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
7876, 77bitri 264 . . . . . . . . . . 11 (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧) ↔ ¬ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
7978exbii 1923 . . . . . . . . . 10 (∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧) ↔ ∃𝑧 ¬ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
80 exnal 1903 . . . . . . . . . 10 (∃𝑧 ¬ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
8179, 80bitr2i 265 . . . . . . . . 9 (¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧))
82812exbii 1924 . . . . . . . 8 (∃𝑥𝑦 ¬ ∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧))
8374, 82bitri 264 . . . . . . 7 (¬ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧))
847adantr 472 . . . . . . . . . . 11 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘dom 𝐹) ∈ ℝ)
85 2re 11302 . . . . . . . . . . . . 13 2 ∈ ℝ
86 diffi 8359 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ Fin → (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin)
87 dmfi 8411 . . . . . . . . . . . . . . . . 17 ((𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin)
8886, 87syl 17 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin)
89 hashcl 13359 . . . . . . . . . . . . . . . 16 (dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℕ0)
9088, 89syl 17 . . . . . . . . . . . . . . 15 (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℕ0)
9190nn0red 11564 . . . . . . . . . . . . . 14 (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ)
9291adantr 472 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ)
93 readdcl 10231 . . . . . . . . . . . . 13 ((2 ∈ ℝ ∧ (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
9485, 92, 93sylancr 698 . . . . . . . . . . . 12 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
95 hashcl 13359 . . . . . . . . . . . . . 14 (𝐹 ∈ Fin → (♯‘𝐹) ∈ ℕ0)
9695nn0red 11564 . . . . . . . . . . . . 13 (𝐹 ∈ Fin → (♯‘𝐹) ∈ ℝ)
9796adantr 472 . . . . . . . . . . . 12 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘𝐹) ∈ ℝ)
98 1re 10251 . . . . . . . . . . . . . . 15 1 ∈ ℝ
99 readdcl 10231 . . . . . . . . . . . . . . 15 ((1 ∈ ℝ ∧ (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ) → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
10098, 91, 99sylancr 698 . . . . . . . . . . . . . 14 (𝐹 ∈ Fin → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
101100adantr 472 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
10285, 91, 93sylancr 698 . . . . . . . . . . . . . 14 (𝐹 ∈ Fin → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
103102adantr 472 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ∈ ℝ)
104 dmun 5486 . . . . . . . . . . . . . . . . . 18 dom ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = (dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))
105 opex 5081 . . . . . . . . . . . . . . . . . . . . 21 𝑥, 𝑦⟩ ∈ V
106 opex 5081 . . . . . . . . . . . . . . . . . . . . 21 𝑥, 𝑧⟩ ∈ V
107105, 106prss 4496 . . . . . . . . . . . . . . . . . . . 20 ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ↔ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ⊆ 𝐹)
108 undif 4193 . . . . . . . . . . . . . . . . . . . 20 ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ⊆ 𝐹 ↔ ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = 𝐹)
109107, 108sylbb 209 . . . . . . . . . . . . . . . . . . 19 ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = 𝐹)
110109dmeqd 5481 . . . . . . . . . . . . . . . . . 18 ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → dom ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = dom 𝐹)
111104, 110syl5reqr 2809 . . . . . . . . . . . . . . . . 17 ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → dom 𝐹 = (dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
112 vex 3343 . . . . . . . . . . . . . . . . . . . 20 𝑦 ∈ V
113 vex 3343 . . . . . . . . . . . . . . . . . . . 20 𝑧 ∈ V
114112, 113dmprop 5769 . . . . . . . . . . . . . . . . . . 19 dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} = {𝑥, 𝑥}
115 dfsn2 4334 . . . . . . . . . . . . . . . . . . 19 {𝑥} = {𝑥, 𝑥}
116114, 115eqtr4i 2785 . . . . . . . . . . . . . . . . . 18 dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} = {𝑥}
117116uneq1i 3906 . . . . . . . . . . . . . . . . 17 (dom {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = ({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))
118111, 117syl6eq 2810 . . . . . . . . . . . . . . . 16 ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → dom 𝐹 = ({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
119118fveq2d 6357 . . . . . . . . . . . . . . 15 ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (♯‘dom 𝐹) = (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
120119ad2antrl 766 . . . . . . . . . . . . . 14 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘dom 𝐹) = (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
121 hashun2 13384 . . . . . . . . . . . . . . . . 17 (({𝑥} ∈ Fin ∧ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin) → (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ ((♯‘{𝑥}) + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
12246, 88, 121sylancr 698 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ ((♯‘{𝑥}) + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
12355oveq1i 6824 . . . . . . . . . . . . . . . 16 ((♯‘{𝑥}) + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
124122, 123syl6breq 4845 . . . . . . . . . . . . . . 15 (𝐹 ∈ Fin → (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
125124adantr 472 . . . . . . . . . . . . . 14 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘({𝑥} ∪ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
126120, 125eqbrtrd 4826 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘dom 𝐹) ≤ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
127 1lt2 11406 . . . . . . . . . . . . . . 15 1 < 2
128 ltadd1 10707 . . . . . . . . . . . . . . . 16 ((1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ) → (1 < 2 ↔ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
12998, 85, 91, 128mp3an12i 1577 . . . . . . . . . . . . . . 15 (𝐹 ∈ Fin → (1 < 2 ↔ (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
130127, 129mpbii 223 . . . . . . . . . . . . . 14 (𝐹 ∈ Fin → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
131130adantr 472 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (1 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
13284, 101, 103, 126, 131lelttrd 10407 . . . . . . . . . . . 12 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘dom 𝐹) < (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
133 fidomdm 8410 . . . . . . . . . . . . . . . . 17 ((𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ≼ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))
13486, 133syl 17 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ≼ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))
135 hashdom 13380 . . . . . . . . . . . . . . . . 17 ((dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin ∧ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin) → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ≼ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
13688, 86, 135syl2anc 696 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ≼ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
137134, 136mpbird 247 . . . . . . . . . . . . . . 15 (𝐹 ∈ Fin → (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))
138 hashcl 13359 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℕ0)
13986, 138syl 17 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℕ0)
140139nn0red 11564 . . . . . . . . . . . . . . . 16 (𝐹 ∈ Fin → (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ)
141 leadd2 10709 . . . . . . . . . . . . . . . . 17 (((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ ∧ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ ∧ 2 ∈ ℝ) → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
14285, 141mp3an3 1562 . . . . . . . . . . . . . . . 16 (((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ ∧ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ∈ ℝ) → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
14391, 140, 142syl2anc 696 . . . . . . . . . . . . . . 15 (𝐹 ∈ Fin → ((♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ≤ (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) ↔ (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})))))
144137, 143mpbid 222 . . . . . . . . . . . . . 14 (𝐹 ∈ Fin → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
145144adantr 472 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
146 prfi 8402 . . . . . . . . . . . . . . . . 17 {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∈ Fin
147 disjdif 4184 . . . . . . . . . . . . . . . . 17 ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∩ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = ∅
148 hashun 13383 . . . . . . . . . . . . . . . . 17 (({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∈ Fin ∧ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin ∧ ({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∩ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩})) = ∅) → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
149146, 147, 148mp3an13 1564 . . . . . . . . . . . . . . . 16 ((𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) ∈ Fin → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
15086, 149syl 17 . . . . . . . . . . . . . . 15 (𝐹 ∈ Fin → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
151150adantr 472 . . . . . . . . . . . . . 14 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
152109fveq2d 6357 . . . . . . . . . . . . . . 15 ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (♯‘𝐹))
153152ad2antrl 766 . . . . . . . . . . . . . 14 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘({⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩} ∪ (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (♯‘𝐹))
15453, 112opth 5093 . . . . . . . . . . . . . . . . . . 19 (⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑧⟩ ↔ (𝑥 = 𝑥𝑦 = 𝑧))
155154simprbi 483 . . . . . . . . . . . . . . . . . 18 (⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑧⟩ → 𝑦 = 𝑧)
156155necon3i 2964 . . . . . . . . . . . . . . . . 17 (𝑦𝑧 → ⟨𝑥, 𝑦⟩ ≠ ⟨𝑥, 𝑧⟩)
157 hashprg 13394 . . . . . . . . . . . . . . . . . 18 ((⟨𝑥, 𝑦⟩ ∈ V ∧ ⟨𝑥, 𝑧⟩ ∈ V) → (⟨𝑥, 𝑦⟩ ≠ ⟨𝑥, 𝑧⟩ ↔ (♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) = 2))
158105, 106, 157mp2an 710 . . . . . . . . . . . . . . . . 17 (⟨𝑥, 𝑦⟩ ≠ ⟨𝑥, 𝑧⟩ ↔ (♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) = 2)
159156, 158sylib 208 . . . . . . . . . . . . . . . 16 (𝑦𝑧 → (♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) = 2)
160159oveq1d 6829 . . . . . . . . . . . . . . 15 (𝑦𝑧 → ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
161160ad2antll 767 . . . . . . . . . . . . . 14 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → ((♯‘{⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}) + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))))
162151, 153, 1613eqtr3rd 2803 . . . . . . . . . . . . 13 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (2 + (♯‘(𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) = (♯‘𝐹))
163145, 162breqtrd 4830 . . . . . . . . . . . 12 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (2 + (♯‘dom (𝐹 ∖ {⟨𝑥, 𝑦⟩, ⟨𝑥, 𝑧⟩}))) ≤ (♯‘𝐹))
16484, 94, 97, 132, 163ltletrd 10409 . . . . . . . . . . 11 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘dom 𝐹) < (♯‘𝐹))
16584, 164gtned 10384 . . . . . . . . . 10 ((𝐹 ∈ Fin ∧ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧)) → (♯‘𝐹) ≠ (♯‘dom 𝐹))
166165ex 449 . . . . . . . . 9 (𝐹 ∈ Fin → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
167166exlimdv 2010 . . . . . . . 8 (𝐹 ∈ Fin → (∃𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
168167exlimdvv 2011 . . . . . . 7 (𝐹 ∈ Fin → (∃𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∧ 𝑦𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
16983, 168syl5bi 232 . . . . . 6 (𝐹 ∈ Fin → (¬ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹)))
170169necon4bd 2952 . . . . 5 (𝐹 ∈ Fin → ((♯‘𝐹) = (♯‘dom 𝐹) → ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
171170imp 444 . . . 4 ((𝐹 ∈ Fin ∧ (♯‘𝐹) = (♯‘dom 𝐹)) → ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
172 dffun4 6061 . . . 4 (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
17373, 171, 172sylanbrc 701 . . 3 ((𝐹 ∈ Fin ∧ (♯‘𝐹) = (♯‘dom 𝐹)) → Fun 𝐹)
174173ex 449 . 2 (𝐹 ∈ Fin → ((♯‘𝐹) = (♯‘dom 𝐹) → Fun 𝐹))
1753, 174impbid2 216 1 (𝐹 ∈ Fin → (Fun 𝐹 ↔ (♯‘𝐹) = (♯‘dom 𝐹)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1072  wal 1630   = wceq 1632  wex 1853  wcel 2139  wne 2932  wral 3050  wrex 3051  Vcvv 3340  cdif 3712  cun 3713  cin 3714  wss 3715  c0 4058  {csn 4321  {cpr 4323  cop 4327   class class class wbr 4804   × cxp 5264  dom cdm 5266  Rel wrel 5271  Fun wfun 6043   Fn wfn 6044  cfv 6049  (class class class)co 6814  cdom 8121  Fincfn 8123  cr 10147  1c1 10149   + caddc 10151   < clt 10286  cle 10287  2c2 11282  0cn0 11504  chash 13331
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115  ax-cnex 10204  ax-resscn 10205  ax-1cn 10206  ax-icn 10207  ax-addcl 10208  ax-addrcl 10209  ax-mulcl 10210  ax-mulrcl 10211  ax-mulcom 10212  ax-addass 10213  ax-mulass 10214  ax-distr 10215  ax-i2m1 10216  ax-1ne0 10217  ax-1rid 10218  ax-rnegex 10219  ax-rrecex 10220  ax-cnre 10221  ax-pre-lttri 10222  ax-pre-lttrn 10223  ax-pre-ltadd 10224  ax-pre-mulgt0 10225
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6775  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-om 7232  df-1st 7334  df-2nd 7335  df-wrecs 7577  df-recs 7638  df-rdg 7676  df-1o 7730  df-oadd 7734  df-er 7913  df-en 8124  df-dom 8125  df-sdom 8126  df-fin 8127  df-card 8975  df-cda 9202  df-pnf 10288  df-mnf 10289  df-xr 10290  df-ltxr 10291  df-le 10292  df-sub 10480  df-neg 10481  df-nn 11233  df-2 11291  df-n0 11505  df-xnn0 11576  df-z 11590  df-uz 11900  df-fz 12540  df-hash 13332
This theorem is referenced by:  hashres  13437  hashreshashfun  13438  ccatalpha  13585
  Copyright terms: Public domain W3C validator