Step | Hyp | Ref
| Expression |
1 | | funfn 5833 |
. . 3
⊢ (Fun
𝐹 ↔ 𝐹 Fn dom 𝐹) |
2 | | hashfn 13025 |
. . 3
⊢ (𝐹 Fn dom 𝐹 → (#‘𝐹) = (#‘dom 𝐹)) |
3 | 1, 2 | sylbi 206 |
. 2
⊢ (Fun
𝐹 → (#‘𝐹) = (#‘dom 𝐹)) |
4 | | dmfi 8129 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ Fin → dom 𝐹 ∈ Fin) |
5 | | hashcl 13009 |
. . . . . . . . . . 11
⊢ (dom
𝐹 ∈ Fin →
(#‘dom 𝐹) ∈
ℕ0) |
6 | 4, 5 | syl 17 |
. . . . . . . . . 10
⊢ (𝐹 ∈ Fin → (#‘dom
𝐹) ∈
ℕ0) |
7 | 6 | nn0red 11229 |
. . . . . . . . 9
⊢ (𝐹 ∈ Fin → (#‘dom
𝐹) ∈
ℝ) |
8 | 7 | adantr 480 |
. . . . . . . 8
⊢ ((𝐹 ∈ Fin ∧ ¬ Rel
𝐹) → (#‘dom
𝐹) ∈
ℝ) |
9 | | df-rel 5045 |
. . . . . . . . . . . . 13
⊢ (Rel
𝐹 ↔ 𝐹 ⊆ (V × V)) |
10 | | dfss3 3558 |
. . . . . . . . . . . . 13
⊢ (𝐹 ⊆ (V × V) ↔
∀𝑥 ∈ 𝐹 𝑥 ∈ (V × V)) |
11 | 9, 10 | bitri 263 |
. . . . . . . . . . . 12
⊢ (Rel
𝐹 ↔ ∀𝑥 ∈ 𝐹 𝑥 ∈ (V × V)) |
12 | 11 | notbii 309 |
. . . . . . . . . . 11
⊢ (¬
Rel 𝐹 ↔ ¬
∀𝑥 ∈ 𝐹 𝑥 ∈ (V × V)) |
13 | | rexnal 2978 |
. . . . . . . . . . 11
⊢
(∃𝑥 ∈
𝐹 ¬ 𝑥 ∈ (V × V) ↔ ¬
∀𝑥 ∈ 𝐹 𝑥 ∈ (V × V)) |
14 | 12, 13 | bitr4i 266 |
. . . . . . . . . 10
⊢ (¬
Rel 𝐹 ↔ ∃𝑥 ∈ 𝐹 ¬ 𝑥 ∈ (V × V)) |
15 | | dmun 5253 |
. . . . . . . . . . . . . . . 16
⊢ dom
((𝐹 ∖ {𝑥}) ∪ {𝑥}) = (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}) |
16 | 15 | fveq2i 6106 |
. . . . . . . . . . . . . . 15
⊢
(#‘dom ((𝐹
∖ {𝑥}) ∪ {𝑥})) = (#‘(dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥})) |
17 | | dmsnn0 5518 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (V × V) ↔ dom
{𝑥} ≠
∅) |
18 | 17 | biimpri 217 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (dom
{𝑥} ≠ ∅ →
𝑥 ∈ (V ×
V)) |
19 | 18 | necon1bi 2810 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑥 ∈ (V × V)
→ dom {𝑥} =
∅) |
20 | 19 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → dom {𝑥} = ∅) |
21 | 20 | uneq2d 3729 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}) = (dom (𝐹 ∖ {𝑥}) ∪ ∅)) |
22 | | un0 3919 |
. . . . . . . . . . . . . . . . 17
⊢ (dom
(𝐹 ∖ {𝑥}) ∪ ∅) = dom (𝐹 ∖ {𝑥}) |
23 | 21, 22 | syl6eq 2660 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}) = dom (𝐹 ∖ {𝑥})) |
24 | 23 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (#‘(dom
(𝐹 ∖ {𝑥}) ∪ dom {𝑥})) = (#‘dom (𝐹 ∖ {𝑥}))) |
25 | 16, 24 | syl5eq 2656 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (#‘dom
((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (#‘dom (𝐹 ∖ {𝑥}))) |
26 | | diffi 8077 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 ∈ Fin → (𝐹 ∖ {𝑥}) ∈ Fin) |
27 | | dmfi 8129 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 ∖ {𝑥}) ∈ Fin → dom (𝐹 ∖ {𝑥}) ∈ Fin) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ Fin → dom (𝐹 ∖ {𝑥}) ∈ Fin) |
29 | | hashcl 13009 |
. . . . . . . . . . . . . . . . . 18
⊢ (dom
(𝐹 ∖ {𝑥}) ∈ Fin →
(#‘dom (𝐹 ∖
{𝑥})) ∈
ℕ0) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ Fin → (#‘dom
(𝐹 ∖ {𝑥})) ∈
ℕ0) |
31 | 30 | nn0red 11229 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin → (#‘dom
(𝐹 ∖ {𝑥})) ∈
ℝ) |
32 | | hashcl 13009 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∖ {𝑥}) ∈ Fin → (#‘(𝐹 ∖ {𝑥})) ∈
ℕ0) |
33 | 26, 32 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ Fin →
(#‘(𝐹 ∖ {𝑥})) ∈
ℕ0) |
34 | 33 | nn0red 11229 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin →
(#‘(𝐹 ∖ {𝑥})) ∈
ℝ) |
35 | | peano2re 10088 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘(𝐹 ∖
{𝑥})) ∈ ℝ →
((#‘(𝐹 ∖ {𝑥})) + 1) ∈
ℝ) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin →
((#‘(𝐹 ∖ {𝑥})) + 1) ∈
ℝ) |
37 | | fidomdm 8128 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∖ {𝑥}) ∈ Fin → dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥})) |
38 | 26, 37 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ Fin → dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥})) |
39 | | hashdom 13029 |
. . . . . . . . . . . . . . . . . 18
⊢ ((dom
(𝐹 ∖ {𝑥}) ∈ Fin ∧ (𝐹 ∖ {𝑥}) ∈ Fin) → ((#‘dom (𝐹 ∖ {𝑥})) ≤ (#‘(𝐹 ∖ {𝑥})) ↔ dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥}))) |
40 | 28, 26, 39 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ Fin → ((#‘dom
(𝐹 ∖ {𝑥})) ≤ (#‘(𝐹 ∖ {𝑥})) ↔ dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥}))) |
41 | 38, 40 | mpbird 246 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin → (#‘dom
(𝐹 ∖ {𝑥})) ≤ (#‘(𝐹 ∖ {𝑥}))) |
42 | 34 | ltp1d 10833 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin →
(#‘(𝐹 ∖ {𝑥})) < ((#‘(𝐹 ∖ {𝑥})) + 1)) |
43 | 31, 34, 36, 41, 42 | lelttrd 10074 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Fin → (#‘dom
(𝐹 ∖ {𝑥})) < ((#‘(𝐹 ∖ {𝑥})) + 1)) |
44 | 43 | 3ad2ant1 1075 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (#‘dom
(𝐹 ∖ {𝑥})) < ((#‘(𝐹 ∖ {𝑥})) + 1)) |
45 | 25, 44 | eqbrtrd 4605 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (#‘dom
((𝐹 ∖ {𝑥}) ∪ {𝑥})) < ((#‘(𝐹 ∖ {𝑥})) + 1)) |
46 | | snfi 7923 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑥} ∈ Fin |
47 | | incom 3767 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∖ {𝑥}) ∩ {𝑥}) = ({𝑥} ∩ (𝐹 ∖ {𝑥})) |
48 | | disjdif 3992 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝑥} ∩ (𝐹 ∖ {𝑥})) = ∅ |
49 | 47, 48 | eqtri 2632 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∖ {𝑥}) ∩ {𝑥}) = ∅ |
50 | | hashun 13032 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∖ {𝑥}) ∈ Fin ∧ {𝑥} ∈ Fin ∧ ((𝐹 ∖ {𝑥}) ∩ {𝑥}) = ∅) → (#‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((#‘(𝐹 ∖ {𝑥})) + (#‘{𝑥}))) |
51 | 46, 49, 50 | mp3an23 1408 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∖ {𝑥}) ∈ Fin → (#‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((#‘(𝐹 ∖ {𝑥})) + (#‘{𝑥}))) |
52 | 26, 51 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Fin →
(#‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((#‘(𝐹 ∖ {𝑥})) + (#‘{𝑥}))) |
53 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑥 ∈ V |
54 | | hashsng 13020 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ V → (#‘{𝑥}) = 1) |
55 | 53, 54 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(#‘{𝑥}) =
1 |
56 | 55 | oveq2i 6560 |
. . . . . . . . . . . . . . 15
⊢
((#‘(𝐹 ∖
{𝑥})) + (#‘{𝑥})) = ((#‘(𝐹 ∖ {𝑥})) + 1) |
57 | 52, 56 | syl6req 2661 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Fin →
((#‘(𝐹 ∖ {𝑥})) + 1) = (#‘((𝐹 ∖ {𝑥}) ∪ {𝑥}))) |
58 | 57 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) →
((#‘(𝐹 ∖ {𝑥})) + 1) = (#‘((𝐹 ∖ {𝑥}) ∪ {𝑥}))) |
59 | 45, 58 | breqtrd 4609 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (#‘dom
((𝐹 ∖ {𝑥}) ∪ {𝑥})) < (#‘((𝐹 ∖ {𝑥}) ∪ {𝑥}))) |
60 | | difsnid 4282 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝐹 → ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = 𝐹) |
61 | 60 | dmeqd 5248 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐹 → dom ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = dom 𝐹) |
62 | 61 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐹 → (#‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (#‘dom 𝐹)) |
63 | 62 | 3ad2ant2 1076 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (#‘dom
((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (#‘dom 𝐹)) |
64 | 60 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐹 → (#‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (#‘𝐹)) |
65 | 64 | 3ad2ant2 1076 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) →
(#‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (#‘𝐹)) |
66 | 59, 63, 65 | 3brtr3d 4614 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (#‘dom
𝐹) < (#‘𝐹)) |
67 | 66 | rexlimdv3a 3015 |
. . . . . . . . . 10
⊢ (𝐹 ∈ Fin → (∃𝑥 ∈ 𝐹 ¬ 𝑥 ∈ (V × V) → (#‘dom
𝐹) < (#‘𝐹))) |
68 | 14, 67 | syl5bi 231 |
. . . . . . . . 9
⊢ (𝐹 ∈ Fin → (¬ Rel
𝐹 → (#‘dom 𝐹) < (#‘𝐹))) |
69 | 68 | imp 444 |
. . . . . . . 8
⊢ ((𝐹 ∈ Fin ∧ ¬ Rel
𝐹) → (#‘dom
𝐹) < (#‘𝐹)) |
70 | 8, 69 | gtned 10051 |
. . . . . . 7
⊢ ((𝐹 ∈ Fin ∧ ¬ Rel
𝐹) → (#‘𝐹) ≠ (#‘dom 𝐹)) |
71 | 70 | ex 449 |
. . . . . 6
⊢ (𝐹 ∈ Fin → (¬ Rel
𝐹 → (#‘𝐹) ≠ (#‘dom 𝐹))) |
72 | 71 | necon4bd 2802 |
. . . . 5
⊢ (𝐹 ∈ Fin →
((#‘𝐹) = (#‘dom
𝐹) → Rel 𝐹)) |
73 | 72 | imp 444 |
. . . 4
⊢ ((𝐹 ∈ Fin ∧ (#‘𝐹) = (#‘dom 𝐹)) → Rel 𝐹) |
74 | | 2nalexn 1745 |
. . . . . . . 8
⊢ (¬
∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥∃𝑦 ¬ ∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧)) |
75 | | df-ne 2782 |
. . . . . . . . . . . . 13
⊢ (𝑦 ≠ 𝑧 ↔ ¬ 𝑦 = 𝑧) |
76 | 75 | anbi2i 726 |
. . . . . . . . . . . 12
⊢
(((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) ↔ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)) |
77 | | annim 440 |
. . . . . . . . . . . 12
⊢
(((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧) ↔ ¬ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧)) |
78 | 76, 77 | bitri 263 |
. . . . . . . . . . 11
⊢
(((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) ↔ ¬ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧)) |
79 | 78 | exbii 1764 |
. . . . . . . . . 10
⊢
(∃𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) ↔ ∃𝑧 ¬ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧)) |
80 | | exnal 1744 |
. . . . . . . . . 10
⊢
(∃𝑧 ¬
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧)) |
81 | 79, 80 | bitr2i 264 |
. . . . . . . . 9
⊢ (¬
∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) |
82 | 81 | 2exbii 1765 |
. . . . . . . 8
⊢
(∃𝑥∃𝑦 ¬ ∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥∃𝑦∃𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) |
83 | 74, 82 | bitri 263 |
. . . . . . 7
⊢ (¬
∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥∃𝑦∃𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) |
84 | 7 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (#‘dom 𝐹) ∈ ℝ) |
85 | | 2re 10967 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ |
86 | | diffi 8077 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ Fin → (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin) |
87 | | dmfi 8129 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin → dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin) |
88 | 86, 87 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin → dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin) |
89 | | hashcl 13009 |
. . . . . . . . . . . . . . . 16
⊢ (dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin → (#‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈
ℕ0) |
90 | 88, 89 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Fin → (#‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈
ℕ0) |
91 | 90 | nn0red 11229 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Fin → (#‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ) |
92 | 91 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ) |
93 | | readdcl 9898 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℝ ∧ (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ) → (2 +
(#‘dom (𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ∈ ℝ) |
94 | 85, 92, 93 | sylancr 694 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ∈ ℝ) |
95 | | hashcl 13009 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Fin →
(#‘𝐹) ∈
ℕ0) |
96 | 95 | nn0red 11229 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ Fin →
(#‘𝐹) ∈
ℝ) |
97 | 96 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (#‘𝐹) ∈ ℝ) |
98 | | 1re 9918 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ |
99 | | readdcl 9898 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℝ ∧ (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ) → (1 +
(#‘dom (𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ∈ ℝ) |
100 | 98, 91, 99 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Fin → (1 +
(#‘dom (𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ∈ ℝ) |
101 | 100 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (1 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ∈ ℝ) |
102 | 85, 91, 93 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Fin → (2 +
(#‘dom (𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ∈ ℝ) |
103 | 102 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ∈ ℝ) |
104 | | dmun 5253 |
. . . . . . . . . . . . . . . . . 18
⊢ dom
({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) = (dom {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) |
105 | | opex 4859 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
〈𝑥, 𝑦〉 ∈ V |
106 | | opex 4859 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
〈𝑥, 𝑧〉 ∈ V |
107 | 105, 106 | prss 4291 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ↔ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ⊆ 𝐹) |
108 | | undif 4001 |
. . . . . . . . . . . . . . . . . . . 20
⊢
({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ⊆ 𝐹 ↔ ({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) = 𝐹) |
109 | 107, 108 | sylbb 208 |
. . . . . . . . . . . . . . . . . . 19
⊢
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → ({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) = 𝐹) |
110 | 109 | dmeqd 5248 |
. . . . . . . . . . . . . . . . . 18
⊢
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → dom ({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) = dom 𝐹) |
111 | 104, 110 | syl5reqr 2659 |
. . . . . . . . . . . . . . . . 17
⊢
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → dom 𝐹 = (dom {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) |
112 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑦 ∈ V |
113 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑧 ∈ V |
114 | 112, 113 | dmprop 5528 |
. . . . . . . . . . . . . . . . . . 19
⊢ dom
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} = {𝑥, 𝑥} |
115 | | dfsn2 4138 |
. . . . . . . . . . . . . . . . . . 19
⊢ {𝑥} = {𝑥, 𝑥} |
116 | 114, 115 | eqtr4i 2635 |
. . . . . . . . . . . . . . . . . 18
⊢ dom
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} = {𝑥} |
117 | 116 | uneq1i 3725 |
. . . . . . . . . . . . . . . . 17
⊢ (dom
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) = ({𝑥} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) |
118 | 111, 117 | syl6eq 2660 |
. . . . . . . . . . . . . . . 16
⊢
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → dom 𝐹 = ({𝑥} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) |
119 | 118 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → (#‘dom 𝐹) = (#‘({𝑥} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
120 | 119 | ad2antrl 760 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (#‘dom 𝐹) = (#‘({𝑥} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
121 | | hashun2 13033 |
. . . . . . . . . . . . . . . . 17
⊢ (({𝑥} ∈ Fin ∧ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin) → (#‘({𝑥} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ ((#‘{𝑥}) + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
122 | 46, 88, 121 | sylancr 694 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin →
(#‘({𝑥} ∪ dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ ((#‘{𝑥}) + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
123 | 55 | oveq1i 6559 |
. . . . . . . . . . . . . . . 16
⊢
((#‘{𝑥}) +
(#‘dom (𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = (1 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) |
124 | 122, 123 | syl6breq 4624 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Fin →
(#‘({𝑥} ∪ dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ (1 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
125 | 124 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (#‘({𝑥} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ (1 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
126 | 120, 125 | eqbrtrd 4605 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (#‘dom 𝐹) ≤ (1 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
127 | | 1lt2 11071 |
. . . . . . . . . . . . . . 15
⊢ 1 <
2 |
128 | | ltadd1 10374 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℝ ∧ 2 ∈ ℝ ∧ (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ) → (1 < 2
↔ (1 + (#‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) < (2 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))))) |
129 | 98, 85, 91, 128 | mp3an12i 1420 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Fin → (1 < 2
↔ (1 + (#‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) < (2 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))))) |
130 | 127, 129 | mpbii 222 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Fin → (1 +
(#‘dom (𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) < (2 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
131 | 130 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (1 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) < (2 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
132 | 84, 101, 103, 126, 131 | lelttrd 10074 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (#‘dom 𝐹) < (2 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
133 | | fidomdm 8128 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin → dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ≼ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) |
134 | 86, 133 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin → dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ≼ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) |
135 | | hashdom 13029 |
. . . . . . . . . . . . . . . . 17
⊢ ((dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin ∧ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin) → ((#‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ≤ (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ↔ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ≼ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) |
136 | 88, 86, 135 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin → ((#‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ≤ (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ↔ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ≼ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) |
137 | 134, 136 | mpbird 246 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Fin → (#‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ≤ (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) |
138 | | hashcl 13009 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin → (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈
ℕ0) |
139 | 86, 138 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ Fin →
(#‘(𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈
ℕ0) |
140 | 139 | nn0red 11229 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin →
(#‘(𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ) |
141 | | leadd2 10376 |
. . . . . . . . . . . . . . . . 17
⊢
(((#‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ ∧
(#‘(𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ ∧ 2 ∈
ℝ) → ((#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ≤ (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ↔ (2 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ (2 + (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))))) |
142 | 85, 141 | mp3an3 1405 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ ∧
(#‘(𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ) →
((#‘dom (𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ≤ (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ↔ (2 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ (2 + (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))))) |
143 | 91, 140, 142 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Fin → ((#‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ≤ (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ↔ (2 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ (2 + (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))))) |
144 | 137, 143 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Fin → (2 +
(#‘dom (𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ (2 + (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
145 | 144 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ (2 + (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
146 | | prfi 8120 |
. . . . . . . . . . . . . . . . 17
⊢
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∈ Fin |
147 | | disjdif 3992 |
. . . . . . . . . . . . . . . . 17
⊢
({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∩ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) = ∅ |
148 | | hashun 13032 |
. . . . . . . . . . . . . . . . 17
⊢
(({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∈ Fin ∧ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin ∧ ({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∩ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) = ∅) →
(#‘({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = ((#‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) + (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
149 | 146, 147,
148 | mp3an13 1407 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin →
(#‘({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = ((#‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) + (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
150 | 86, 149 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Fin →
(#‘({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = ((#‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) + (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
151 | 150 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (#‘({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = ((#‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) + (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
152 | 109 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → (#‘({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = (#‘𝐹)) |
153 | 152 | ad2antrl 760 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (#‘({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = (#‘𝐹)) |
154 | 53, 112 | opth 4871 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈𝑥, 𝑦〉 = 〈𝑥, 𝑧〉 ↔ (𝑥 = 𝑥 ∧ 𝑦 = 𝑧)) |
155 | 154 | simprbi 479 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑥, 𝑦〉 = 〈𝑥, 𝑧〉 → 𝑦 = 𝑧) |
156 | 155 | necon3i 2814 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ≠ 𝑧 → 〈𝑥, 𝑦〉 ≠ 〈𝑥, 𝑧〉) |
157 | | hashprg 13043 |
. . . . . . . . . . . . . . . . . 18
⊢
((〈𝑥, 𝑦〉 ∈ V ∧
〈𝑥, 𝑧〉 ∈ V) → (〈𝑥, 𝑦〉 ≠ 〈𝑥, 𝑧〉 ↔ (#‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) = 2)) |
158 | 105, 106,
157 | mp2an 704 |
. . . . . . . . . . . . . . . . 17
⊢
(〈𝑥, 𝑦〉 ≠ 〈𝑥, 𝑧〉 ↔ (#‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) = 2) |
159 | 156, 158 | sylib 207 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ≠ 𝑧 → (#‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) = 2) |
160 | 159 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ≠ 𝑧 → ((#‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) + (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = (2 + (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
161 | 160 | ad2antll 761 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → ((#‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) + (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = (2 + (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
162 | 151, 153,
161 | 3eqtr3rd 2653 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (#‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = (#‘𝐹)) |
163 | 145, 162 | breqtrd 4609 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (#‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ (#‘𝐹)) |
164 | 84, 94, 97, 132, 163 | ltletrd 10076 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (#‘dom 𝐹) < (#‘𝐹)) |
165 | 84, 164 | gtned 10051 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (#‘𝐹) ≠ (#‘dom 𝐹)) |
166 | 165 | ex 449 |
. . . . . . . . 9
⊢ (𝐹 ∈ Fin →
(((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) → (#‘𝐹) ≠ (#‘dom 𝐹))) |
167 | 166 | exlimdv 1848 |
. . . . . . . 8
⊢ (𝐹 ∈ Fin → (∃𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) → (#‘𝐹) ≠ (#‘dom 𝐹))) |
168 | 167 | exlimdvv 1849 |
. . . . . . 7
⊢ (𝐹 ∈ Fin → (∃𝑥∃𝑦∃𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) → (#‘𝐹) ≠ (#‘dom 𝐹))) |
169 | 83, 168 | syl5bi 231 |
. . . . . 6
⊢ (𝐹 ∈ Fin → (¬
∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧) → (#‘𝐹) ≠ (#‘dom 𝐹))) |
170 | 169 | necon4bd 2802 |
. . . . 5
⊢ (𝐹 ∈ Fin →
((#‘𝐹) = (#‘dom
𝐹) → ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧))) |
171 | 170 | imp 444 |
. . . 4
⊢ ((𝐹 ∈ Fin ∧ (#‘𝐹) = (#‘dom 𝐹)) → ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧)) |
172 | | dffun4 5816 |
. . . 4
⊢ (Fun
𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧))) |
173 | 73, 171, 172 | sylanbrc 695 |
. . 3
⊢ ((𝐹 ∈ Fin ∧ (#‘𝐹) = (#‘dom 𝐹)) → Fun 𝐹) |
174 | 173 | ex 449 |
. 2
⊢ (𝐹 ∈ Fin →
((#‘𝐹) = (#‘dom
𝐹) → Fun 𝐹)) |
175 | 3, 174 | impbid2 215 |
1
⊢ (𝐹 ∈ Fin → (Fun 𝐹 ↔ (#‘𝐹) = (#‘dom 𝐹))) |