Step | Hyp | Ref
| Expression |
1 | | funfn 5956 |
. . 3
⊢ (Fun
𝐹 ↔ 𝐹 Fn dom 𝐹) |
2 | | hashfn 13202 |
. . 3
⊢ (𝐹 Fn dom 𝐹 → (#‘𝐹) = (#‘dom 𝐹)) |
3 | 1, 2 | sylbi 207 |
. 2
⊢ (Fun
𝐹 → (#‘𝐹) = (#‘dom 𝐹)) |
4 | | dmfi 8285 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ Fin → dom 𝐹 ∈ Fin) |
5 | | hashcl 13185 |
. . . . . . . . . . 11
⊢ (dom
𝐹 ∈ Fin →
(#‘dom 𝐹) ∈
ℕ0) |
6 | 4, 5 | syl 17 |
. . . . . . . . . 10
⊢ (𝐹 ∈ Fin → (#‘dom
𝐹) ∈
ℕ0) |
7 | 6 | nn0red 11390 |
. . . . . . . . 9
⊢ (𝐹 ∈ Fin → (#‘dom
𝐹) ∈
ℝ) |
8 | 7 | adantr 480 |
. . . . . . . 8
⊢ ((𝐹 ∈ Fin ∧ ¬ Rel
𝐹) → (#‘dom
𝐹) ∈
ℝ) |
9 | | df-rel 5150 |
. . . . . . . . . . . . 13
⊢ (Rel
𝐹 ↔ 𝐹 ⊆ (V × V)) |
10 | | dfss3 3625 |
. . . . . . . . . . . . 13
⊢ (𝐹 ⊆ (V × V) ↔
∀𝑥 ∈ 𝐹 𝑥 ∈ (V × V)) |
11 | 9, 10 | bitri 264 |
. . . . . . . . . . . 12
⊢ (Rel
𝐹 ↔ ∀𝑥 ∈ 𝐹 𝑥 ∈ (V × V)) |
12 | 11 | notbii 309 |
. . . . . . . . . . 11
⊢ (¬
Rel 𝐹 ↔ ¬
∀𝑥 ∈ 𝐹 𝑥 ∈ (V × V)) |
13 | | rexnal 3024 |
. . . . . . . . . . 11
⊢
(∃𝑥 ∈
𝐹 ¬ 𝑥 ∈ (V × V) ↔ ¬
∀𝑥 ∈ 𝐹 𝑥 ∈ (V × V)) |
14 | 12, 13 | bitr4i 267 |
. . . . . . . . . 10
⊢ (¬
Rel 𝐹 ↔ ∃𝑥 ∈ 𝐹 ¬ 𝑥 ∈ (V × V)) |
15 | | dmun 5363 |
. . . . . . . . . . . . . . . 16
⊢ dom
((𝐹 ∖ {𝑥}) ∪ {𝑥}) = (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}) |
16 | 15 | fveq2i 6232 |
. . . . . . . . . . . . . . 15
⊢
(#‘dom ((𝐹
∖ {𝑥}) ∪ {𝑥})) = (#‘(dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥})) |
17 | | dmsnn0 5635 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (V × V) ↔ dom
{𝑥} ≠
∅) |
18 | 17 | biimpri 218 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (dom
{𝑥} ≠ ∅ →
𝑥 ∈ (V ×
V)) |
19 | 18 | necon1bi 2851 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑥 ∈ (V × V)
→ dom {𝑥} =
∅) |
20 | 19 | 3ad2ant3 1104 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → dom {𝑥} = ∅) |
21 | 20 | uneq2d 3800 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}) = (dom (𝐹 ∖ {𝑥}) ∪ ∅)) |
22 | | un0 4000 |
. . . . . . . . . . . . . . . . 17
⊢ (dom
(𝐹 ∖ {𝑥}) ∪ ∅) = dom (𝐹 ∖ {𝑥}) |
23 | 21, 22 | syl6eq 2701 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}) = dom (𝐹 ∖ {𝑥})) |
24 | 23 | fveq2d 6233 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (#‘(dom
(𝐹 ∖ {𝑥}) ∪ dom {𝑥})) = (#‘dom (𝐹 ∖ {𝑥}))) |
25 | 16, 24 | syl5eq 2697 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (#‘dom
((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (#‘dom (𝐹 ∖ {𝑥}))) |
26 | | diffi 8233 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 ∈ Fin → (𝐹 ∖ {𝑥}) ∈ Fin) |
27 | | dmfi 8285 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 ∖ {𝑥}) ∈ Fin → dom (𝐹 ∖ {𝑥}) ∈ Fin) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ Fin → dom (𝐹 ∖ {𝑥}) ∈ Fin) |
29 | | hashcl 13185 |
. . . . . . . . . . . . . . . . . 18
⊢ (dom
(𝐹 ∖ {𝑥}) ∈ Fin →
(#‘dom (𝐹 ∖
{𝑥})) ∈
ℕ0) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ Fin → (#‘dom
(𝐹 ∖ {𝑥})) ∈
ℕ0) |
31 | 30 | nn0red 11390 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin → (#‘dom
(𝐹 ∖ {𝑥})) ∈
ℝ) |
32 | | hashcl 13185 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∖ {𝑥}) ∈ Fin → (#‘(𝐹 ∖ {𝑥})) ∈
ℕ0) |
33 | 26, 32 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ Fin →
(#‘(𝐹 ∖ {𝑥})) ∈
ℕ0) |
34 | 33 | nn0red 11390 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin →
(#‘(𝐹 ∖ {𝑥})) ∈
ℝ) |
35 | | peano2re 10247 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘(𝐹 ∖
{𝑥})) ∈ ℝ →
((#‘(𝐹 ∖ {𝑥})) + 1) ∈
ℝ) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin →
((#‘(𝐹 ∖ {𝑥})) + 1) ∈
ℝ) |
37 | | fidomdm 8284 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∖ {𝑥}) ∈ Fin → dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥})) |
38 | 26, 37 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ Fin → dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥})) |
39 | | hashdom 13206 |
. . . . . . . . . . . . . . . . . 18
⊢ ((dom
(𝐹 ∖ {𝑥}) ∈ Fin ∧ (𝐹 ∖ {𝑥}) ∈ Fin) → ((#‘dom (𝐹 ∖ {𝑥})) ≤ (#‘(𝐹 ∖ {𝑥})) ↔ dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥}))) |
40 | 28, 26, 39 | syl2anc 694 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ Fin → ((#‘dom
(𝐹 ∖ {𝑥})) ≤ (#‘(𝐹 ∖ {𝑥})) ↔ dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥}))) |
41 | 38, 40 | mpbird 247 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin → (#‘dom
(𝐹 ∖ {𝑥})) ≤ (#‘(𝐹 ∖ {𝑥}))) |
42 | 34 | ltp1d 10992 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin →
(#‘(𝐹 ∖ {𝑥})) < ((#‘(𝐹 ∖ {𝑥})) + 1)) |
43 | 31, 34, 36, 41, 42 | lelttrd 10233 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Fin → (#‘dom
(𝐹 ∖ {𝑥})) < ((#‘(𝐹 ∖ {𝑥})) + 1)) |
44 | 43 | 3ad2ant1 1102 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (#‘dom
(𝐹 ∖ {𝑥})) < ((#‘(𝐹 ∖ {𝑥})) + 1)) |
45 | 25, 44 | eqbrtrd 4707 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (#‘dom
((𝐹 ∖ {𝑥}) ∪ {𝑥})) < ((#‘(𝐹 ∖ {𝑥})) + 1)) |
46 | | snfi 8079 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑥} ∈ Fin |
47 | | incom 3838 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∖ {𝑥}) ∩ {𝑥}) = ({𝑥} ∩ (𝐹 ∖ {𝑥})) |
48 | | disjdif 4073 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝑥} ∩ (𝐹 ∖ {𝑥})) = ∅ |
49 | 47, 48 | eqtri 2673 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∖ {𝑥}) ∩ {𝑥}) = ∅ |
50 | | hashun 13209 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∖ {𝑥}) ∈ Fin ∧ {𝑥} ∈ Fin ∧ ((𝐹 ∖ {𝑥}) ∩ {𝑥}) = ∅) → (#‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((#‘(𝐹 ∖ {𝑥})) + (#‘{𝑥}))) |
51 | 46, 49, 50 | mp3an23 1456 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∖ {𝑥}) ∈ Fin → (#‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((#‘(𝐹 ∖ {𝑥})) + (#‘{𝑥}))) |
52 | 26, 51 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Fin →
(#‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((#‘(𝐹 ∖ {𝑥})) + (#‘{𝑥}))) |
53 | | vex 3234 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑥 ∈ V |
54 | | hashsng 13197 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ V → (#‘{𝑥}) = 1) |
55 | 53, 54 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(#‘{𝑥}) =
1 |
56 | 55 | oveq2i 6701 |
. . . . . . . . . . . . . . 15
⊢
((#‘(𝐹 ∖
{𝑥})) + (#‘{𝑥})) = ((#‘(𝐹 ∖ {𝑥})) + 1) |
57 | 52, 56 | syl6req 2702 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Fin →
((#‘(𝐹 ∖ {𝑥})) + 1) = (#‘((𝐹 ∖ {𝑥}) ∪ {𝑥}))) |
58 | 57 | 3ad2ant1 1102 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) →
((#‘(𝐹 ∖ {𝑥})) + 1) = (#‘((𝐹 ∖ {𝑥}) ∪ {𝑥}))) |
59 | 45, 58 | breqtrd 4711 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (#‘dom
((𝐹 ∖ {𝑥}) ∪ {𝑥})) < (#‘((𝐹 ∖ {𝑥}) ∪ {𝑥}))) |
60 | | difsnid 4373 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝐹 → ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = 𝐹) |
61 | 60 | dmeqd 5358 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐹 → dom ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = dom 𝐹) |
62 | 61 | fveq2d 6233 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐹 → (#‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (#‘dom 𝐹)) |
63 | 62 | 3ad2ant2 1103 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (#‘dom
((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (#‘dom 𝐹)) |
64 | 60 | fveq2d 6233 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐹 → (#‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (#‘𝐹)) |
65 | 64 | 3ad2ant2 1103 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) →
(#‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (#‘𝐹)) |
66 | 59, 63, 65 | 3brtr3d 4716 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (#‘dom
𝐹) < (#‘𝐹)) |
67 | 66 | rexlimdv3a 3062 |
. . . . . . . . . 10
⊢ (𝐹 ∈ Fin → (∃𝑥 ∈ 𝐹 ¬ 𝑥 ∈ (V × V) → (#‘dom
𝐹) < (#‘𝐹))) |
68 | 14, 67 | syl5bi 232 |
. . . . . . . . 9
⊢ (𝐹 ∈ Fin → (¬ Rel
𝐹 → (#‘dom 𝐹) < (#‘𝐹))) |
69 | 68 | imp 444 |
. . . . . . . 8
⊢ ((𝐹 ∈ Fin ∧ ¬ Rel
𝐹) → (#‘dom
𝐹) < (#‘𝐹)) |
70 | 8, 69 | gtned 10210 |
. . . . . . 7
⊢ ((𝐹 ∈ Fin ∧ ¬ Rel
𝐹) → (#‘𝐹) ≠ (#‘dom 𝐹)) |
71 | 70 | ex 449 |
. . . . . 6
⊢ (𝐹 ∈ Fin → (¬ Rel
𝐹 → (#‘𝐹) ≠ (#‘dom 𝐹))) |
72 | 71 | necon4bd 2843 |
. . . . 5
⊢ (𝐹 ∈ Fin →
((#‘𝐹) = (#‘dom
𝐹) → Rel 𝐹)) |
73 | 72 | imp 444 |
. . . 4
⊢ ((𝐹 ∈ Fin ∧ (#‘𝐹) = (#‘dom 𝐹)) → Rel 𝐹) |
74 | | 2nalexn 1795 |
. . . . . . . 8
⊢ (¬
∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥∃𝑦 ¬ ∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧)) |
75 | | df-ne 2824 |
. . . . . . . . . . . . 13
⊢ (𝑦 ≠ 𝑧 ↔ ¬ 𝑦 = 𝑧) |
76 | 75 | anbi2i 730 |
. . . . . . . . . . . 12
⊢
(((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) ↔ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)) |
77 | | annim 440 |
. . . . . . . . . . . 12
⊢
(((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧) ↔ ¬ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧)) |
78 | 76, 77 | bitri 264 |
. . . . . . . . . . 11
⊢
(((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) ↔ ¬ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧)) |
79 | 78 | exbii 1814 |
. . . . . . . . . 10
⊢
(∃𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) ↔ ∃𝑧 ¬ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧)) |
80 | | exnal 1794 |
. . . . . . . . . 10
⊢
(∃𝑧 ¬
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧)) |
81 | 79, 80 | bitr2i 265 |
. . . . . . . . 9
⊢ (¬
∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) |
82 | 81 | 2exbii 1815 |
. . . . . . . 8
⊢
(∃𝑥∃𝑦 ¬ ∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥∃𝑦∃𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) |
83 | 74, 82 | bitri 264 |
. . . . . . 7
⊢ (¬
∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥∃𝑦∃𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) |
84 | 7 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (#‘dom 𝐹) ∈ ℝ) |
85 | | 2re 11128 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ |
86 | | diffi 8233 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ Fin → (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin) |
87 | | dmfi 8285 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin → dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin) |
88 | 86, 87 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin → dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin) |
89 | | hashcl 13185 |
. . . . . . . . . . . . . . . 16
⊢ (dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin → (#‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈
ℕ0) |
90 | 88, 89 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Fin → (#‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈
ℕ0) |
91 | 90 | nn0red 11390 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Fin → (#‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ) |
92 | 91 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ) |
93 | | readdcl 10057 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℝ ∧ (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ) → (2 +
(#‘dom (𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ∈ ℝ) |
94 | 85, 92, 93 | sylancr 696 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ∈ ℝ) |
95 | | hashcl 13185 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Fin →
(#‘𝐹) ∈
ℕ0) |
96 | 95 | nn0red 11390 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ Fin →
(#‘𝐹) ∈
ℝ) |
97 | 96 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (#‘𝐹) ∈ ℝ) |
98 | | 1re 10077 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ |
99 | | readdcl 10057 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℝ ∧ (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ) → (1 +
(#‘dom (𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ∈ ℝ) |
100 | 98, 91, 99 | sylancr 696 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Fin → (1 +
(#‘dom (𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ∈ ℝ) |
101 | 100 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (1 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ∈ ℝ) |
102 | 85, 91, 93 | sylancr 696 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Fin → (2 +
(#‘dom (𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ∈ ℝ) |
103 | 102 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ∈ ℝ) |
104 | | dmun 5363 |
. . . . . . . . . . . . . . . . . 18
⊢ dom
({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) = (dom {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) |
105 | | opex 4962 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
〈𝑥, 𝑦〉 ∈ V |
106 | | opex 4962 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
〈𝑥, 𝑧〉 ∈ V |
107 | 105, 106 | prss 4383 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ↔ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ⊆ 𝐹) |
108 | | undif 4082 |
. . . . . . . . . . . . . . . . . . . 20
⊢
({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ⊆ 𝐹 ↔ ({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) = 𝐹) |
109 | 107, 108 | sylbb 209 |
. . . . . . . . . . . . . . . . . . 19
⊢
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → ({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) = 𝐹) |
110 | 109 | dmeqd 5358 |
. . . . . . . . . . . . . . . . . 18
⊢
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → dom ({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) = dom 𝐹) |
111 | 104, 110 | syl5reqr 2700 |
. . . . . . . . . . . . . . . . 17
⊢
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → dom 𝐹 = (dom {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) |
112 | | vex 3234 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑦 ∈ V |
113 | | vex 3234 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑧 ∈ V |
114 | 112, 113 | dmprop 5646 |
. . . . . . . . . . . . . . . . . . 19
⊢ dom
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} = {𝑥, 𝑥} |
115 | | dfsn2 4223 |
. . . . . . . . . . . . . . . . . . 19
⊢ {𝑥} = {𝑥, 𝑥} |
116 | 114, 115 | eqtr4i 2676 |
. . . . . . . . . . . . . . . . . 18
⊢ dom
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} = {𝑥} |
117 | 116 | uneq1i 3796 |
. . . . . . . . . . . . . . . . 17
⊢ (dom
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) = ({𝑥} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) |
118 | 111, 117 | syl6eq 2701 |
. . . . . . . . . . . . . . . 16
⊢
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → dom 𝐹 = ({𝑥} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) |
119 | 118 | fveq2d 6233 |
. . . . . . . . . . . . . . 15
⊢
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → (#‘dom 𝐹) = (#‘({𝑥} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
120 | 119 | ad2antrl 764 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (#‘dom 𝐹) = (#‘({𝑥} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
121 | | hashun2 13210 |
. . . . . . . . . . . . . . . . 17
⊢ (({𝑥} ∈ Fin ∧ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin) → (#‘({𝑥} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ ((#‘{𝑥}) + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
122 | 46, 88, 121 | sylancr 696 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin →
(#‘({𝑥} ∪ dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ ((#‘{𝑥}) + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
123 | 55 | oveq1i 6700 |
. . . . . . . . . . . . . . . 16
⊢
((#‘{𝑥}) +
(#‘dom (𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = (1 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) |
124 | 122, 123 | syl6breq 4726 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Fin →
(#‘({𝑥} ∪ dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ (1 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
125 | 124 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (#‘({𝑥} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ (1 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
126 | 120, 125 | eqbrtrd 4707 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (#‘dom 𝐹) ≤ (1 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
127 | | 1lt2 11232 |
. . . . . . . . . . . . . . 15
⊢ 1 <
2 |
128 | | ltadd1 10533 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℝ ∧ 2 ∈ ℝ ∧ (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ) → (1 < 2
↔ (1 + (#‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) < (2 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))))) |
129 | 98, 85, 91, 128 | mp3an12i 1468 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Fin → (1 < 2
↔ (1 + (#‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) < (2 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))))) |
130 | 127, 129 | mpbii 223 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Fin → (1 +
(#‘dom (𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) < (2 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
131 | 130 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (1 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) < (2 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
132 | 84, 101, 103, 126, 131 | lelttrd 10233 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (#‘dom 𝐹) < (2 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
133 | | fidomdm 8284 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin → dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ≼ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) |
134 | 86, 133 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin → dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ≼ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) |
135 | | hashdom 13206 |
. . . . . . . . . . . . . . . . 17
⊢ ((dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin ∧ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin) → ((#‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ≤ (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ↔ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ≼ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) |
136 | 88, 86, 135 | syl2anc 694 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin → ((#‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ≤ (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ↔ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ≼ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) |
137 | 134, 136 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Fin → (#‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ≤ (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) |
138 | | hashcl 13185 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin → (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈
ℕ0) |
139 | 86, 138 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ Fin →
(#‘(𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈
ℕ0) |
140 | 139 | nn0red 11390 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin →
(#‘(𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ) |
141 | | leadd2 10535 |
. . . . . . . . . . . . . . . . 17
⊢
(((#‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ ∧
(#‘(𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ ∧ 2 ∈
ℝ) → ((#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ≤ (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ↔ (2 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ (2 + (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))))) |
142 | 85, 141 | mp3an3 1453 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ ∧
(#‘(𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ) →
((#‘dom (𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ≤ (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ↔ (2 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ (2 + (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))))) |
143 | 91, 140, 142 | syl2anc 694 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Fin → ((#‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ≤ (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ↔ (2 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ (2 + (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))))) |
144 | 137, 143 | mpbid 222 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Fin → (2 +
(#‘dom (𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ (2 + (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
145 | 144 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ (2 + (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
146 | | prfi 8276 |
. . . . . . . . . . . . . . . . 17
⊢
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∈ Fin |
147 | | disjdif 4073 |
. . . . . . . . . . . . . . . . 17
⊢
({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∩ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) = ∅ |
148 | | hashun 13209 |
. . . . . . . . . . . . . . . . 17
⊢
(({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∈ Fin ∧ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin ∧ ({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∩ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) = ∅) →
(#‘({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = ((#‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) + (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
149 | 146, 147,
148 | mp3an13 1455 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin →
(#‘({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = ((#‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) + (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
150 | 86, 149 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Fin →
(#‘({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = ((#‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) + (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
151 | 150 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (#‘({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = ((#‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) + (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
152 | 109 | fveq2d 6233 |
. . . . . . . . . . . . . . 15
⊢
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → (#‘({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = (#‘𝐹)) |
153 | 152 | ad2antrl 764 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (#‘({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = (#‘𝐹)) |
154 | 53, 112 | opth 4974 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈𝑥, 𝑦〉 = 〈𝑥, 𝑧〉 ↔ (𝑥 = 𝑥 ∧ 𝑦 = 𝑧)) |
155 | 154 | simprbi 479 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑥, 𝑦〉 = 〈𝑥, 𝑧〉 → 𝑦 = 𝑧) |
156 | 155 | necon3i 2855 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ≠ 𝑧 → 〈𝑥, 𝑦〉 ≠ 〈𝑥, 𝑧〉) |
157 | | hashprg 13220 |
. . . . . . . . . . . . . . . . . 18
⊢
((〈𝑥, 𝑦〉 ∈ V ∧
〈𝑥, 𝑧〉 ∈ V) → (〈𝑥, 𝑦〉 ≠ 〈𝑥, 𝑧〉 ↔ (#‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) = 2)) |
158 | 105, 106,
157 | mp2an 708 |
. . . . . . . . . . . . . . . . 17
⊢
(〈𝑥, 𝑦〉 ≠ 〈𝑥, 𝑧〉 ↔ (#‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) = 2) |
159 | 156, 158 | sylib 208 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ≠ 𝑧 → (#‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) = 2) |
160 | 159 | oveq1d 6705 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ≠ 𝑧 → ((#‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) + (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = (2 + (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
161 | 160 | ad2antll 765 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → ((#‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) + (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = (2 + (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
162 | 151, 153,
161 | 3eqtr3rd 2694 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = (#‘𝐹)) |
163 | 145, 162 | breqtrd 4711 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ (#‘𝐹)) |
164 | 84, 94, 97, 132, 163 | ltletrd 10235 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (#‘dom 𝐹) < (#‘𝐹)) |
165 | 84, 164 | gtned 10210 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (#‘𝐹) ≠ (#‘dom 𝐹)) |
166 | 165 | ex 449 |
. . . . . . . . 9
⊢ (𝐹 ∈ Fin →
(((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) → (#‘𝐹) ≠ (#‘dom 𝐹))) |
167 | 166 | exlimdv 1901 |
. . . . . . . 8
⊢ (𝐹 ∈ Fin → (∃𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) → (#‘𝐹) ≠ (#‘dom 𝐹))) |
168 | 167 | exlimdvv 1902 |
. . . . . . 7
⊢ (𝐹 ∈ Fin → (∃𝑥∃𝑦∃𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) → (#‘𝐹) ≠ (#‘dom 𝐹))) |
169 | 83, 168 | syl5bi 232 |
. . . . . 6
⊢ (𝐹 ∈ Fin → (¬
∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧) → (#‘𝐹) ≠ (#‘dom 𝐹))) |
170 | 169 | necon4bd 2843 |
. . . . 5
⊢ (𝐹 ∈ Fin →
((#‘𝐹) = (#‘dom
𝐹) → ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧))) |
171 | 170 | imp 444 |
. . . 4
⊢ ((𝐹 ∈ Fin ∧ (#‘𝐹) = (#‘dom 𝐹)) → ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧)) |
172 | | dffun4 5938 |
. . . 4
⊢ (Fun
𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧))) |
173 | 73, 171, 172 | sylanbrc 699 |
. . 3
⊢ ((𝐹 ∈ Fin ∧ (#‘𝐹) = (#‘dom 𝐹)) → Fun 𝐹) |
174 | 173 | ex 449 |
. 2
⊢ (𝐹 ∈ Fin →
((#‘𝐹) = (#‘dom
𝐹) → Fun 𝐹)) |
175 | 3, 174 | impbid2 216 |
1
⊢ (𝐹 ∈ Fin → (Fun 𝐹 ↔ (#‘𝐹) = (#‘dom 𝐹))) |