Step | Hyp | Ref
| Expression |
1 | | funfn 6247 |
. . 3
⊢ (Fun
𝐹 ↔ 𝐹 Fn dom 𝐹) |
2 | | hashfn 13572 |
. . 3
⊢ (𝐹 Fn dom 𝐹 → (♯‘𝐹) = (♯‘dom 𝐹)) |
3 | 1, 2 | sylbi 218 |
. 2
⊢ (Fun
𝐹 →
(♯‘𝐹) =
(♯‘dom 𝐹)) |
4 | | dmfi 8638 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ Fin → dom 𝐹 ∈ Fin) |
5 | | hashcl 13555 |
. . . . . . . . . . 11
⊢ (dom
𝐹 ∈ Fin →
(♯‘dom 𝐹)
∈ ℕ0) |
6 | 4, 5 | syl 17 |
. . . . . . . . . 10
⊢ (𝐹 ∈ Fin →
(♯‘dom 𝐹)
∈ ℕ0) |
7 | 6 | nn0red 11793 |
. . . . . . . . 9
⊢ (𝐹 ∈ Fin →
(♯‘dom 𝐹)
∈ ℝ) |
8 | 7 | adantr 481 |
. . . . . . . 8
⊢ ((𝐹 ∈ Fin ∧ ¬ Rel
𝐹) →
(♯‘dom 𝐹)
∈ ℝ) |
9 | | df-rel 5442 |
. . . . . . . . . . . . 13
⊢ (Rel
𝐹 ↔ 𝐹 ⊆ (V × V)) |
10 | | dfss3 3873 |
. . . . . . . . . . . . 13
⊢ (𝐹 ⊆ (V × V) ↔
∀𝑥 ∈ 𝐹 𝑥 ∈ (V × V)) |
11 | 9, 10 | bitri 276 |
. . . . . . . . . . . 12
⊢ (Rel
𝐹 ↔ ∀𝑥 ∈ 𝐹 𝑥 ∈ (V × V)) |
12 | 11 | notbii 321 |
. . . . . . . . . . 11
⊢ (¬
Rel 𝐹 ↔ ¬
∀𝑥 ∈ 𝐹 𝑥 ∈ (V × V)) |
13 | | rexnal 3200 |
. . . . . . . . . . 11
⊢
(∃𝑥 ∈
𝐹 ¬ 𝑥 ∈ (V × V) ↔ ¬
∀𝑥 ∈ 𝐹 𝑥 ∈ (V × V)) |
14 | 12, 13 | bitr4i 279 |
. . . . . . . . . 10
⊢ (¬
Rel 𝐹 ↔ ∃𝑥 ∈ 𝐹 ¬ 𝑥 ∈ (V × V)) |
15 | | dmun 5657 |
. . . . . . . . . . . . . . . 16
⊢ dom
((𝐹 ∖ {𝑥}) ∪ {𝑥}) = (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}) |
16 | 15 | fveq2i 6533 |
. . . . . . . . . . . . . . 15
⊢
(♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘(dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥})) |
17 | | dmsnn0 5931 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (V × V) ↔ dom
{𝑥} ≠
∅) |
18 | 17 | biimpri 229 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (dom
{𝑥} ≠ ∅ →
𝑥 ∈ (V ×
V)) |
19 | 18 | necon1bi 3010 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑥 ∈ (V × V)
→ dom {𝑥} =
∅) |
20 | 19 | 3ad2ant3 1126 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → dom {𝑥} = ∅) |
21 | 20 | uneq2d 4055 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}) = (dom (𝐹 ∖ {𝑥}) ∪ ∅)) |
22 | | un0 4258 |
. . . . . . . . . . . . . . . . 17
⊢ (dom
(𝐹 ∖ {𝑥}) ∪ ∅) = dom (𝐹 ∖ {𝑥}) |
23 | 21, 22 | syl6eq 2845 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}) = dom (𝐹 ∖ {𝑥})) |
24 | 23 | fveq2d 6534 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) →
(♯‘(dom (𝐹
∖ {𝑥}) ∪ dom
{𝑥})) = (♯‘dom
(𝐹 ∖ {𝑥}))) |
25 | 16, 24 | syl5eq 2841 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) →
(♯‘dom ((𝐹
∖ {𝑥}) ∪ {𝑥})) = (♯‘dom (𝐹 ∖ {𝑥}))) |
26 | | diffi 8586 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 ∈ Fin → (𝐹 ∖ {𝑥}) ∈ Fin) |
27 | | dmfi 8638 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 ∖ {𝑥}) ∈ Fin → dom (𝐹 ∖ {𝑥}) ∈ Fin) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ Fin → dom (𝐹 ∖ {𝑥}) ∈ Fin) |
29 | | hashcl 13555 |
. . . . . . . . . . . . . . . . . 18
⊢ (dom
(𝐹 ∖ {𝑥}) ∈ Fin →
(♯‘dom (𝐹
∖ {𝑥})) ∈
ℕ0) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ Fin →
(♯‘dom (𝐹
∖ {𝑥})) ∈
ℕ0) |
31 | 30 | nn0red 11793 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin →
(♯‘dom (𝐹
∖ {𝑥})) ∈
ℝ) |
32 | | hashcl 13555 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∖ {𝑥}) ∈ Fin → (♯‘(𝐹 ∖ {𝑥})) ∈
ℕ0) |
33 | 26, 32 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ Fin →
(♯‘(𝐹 ∖
{𝑥})) ∈
ℕ0) |
34 | 33 | nn0red 11793 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin →
(♯‘(𝐹 ∖
{𝑥})) ∈
ℝ) |
35 | | peano2re 10649 |
. . . . . . . . . . . . . . . . 17
⊢
((♯‘(𝐹
∖ {𝑥})) ∈
ℝ → ((♯‘(𝐹 ∖ {𝑥})) + 1) ∈ ℝ) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin →
((♯‘(𝐹 ∖
{𝑥})) + 1) ∈
ℝ) |
37 | | fidomdm 8637 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∖ {𝑥}) ∈ Fin → dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥})) |
38 | 26, 37 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ Fin → dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥})) |
39 | | hashdom 13576 |
. . . . . . . . . . . . . . . . . 18
⊢ ((dom
(𝐹 ∖ {𝑥}) ∈ Fin ∧ (𝐹 ∖ {𝑥}) ∈ Fin) → ((♯‘dom
(𝐹 ∖ {𝑥})) ≤ (♯‘(𝐹 ∖ {𝑥})) ↔ dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥}))) |
40 | 28, 26, 39 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ Fin →
((♯‘dom (𝐹
∖ {𝑥})) ≤
(♯‘(𝐹 ∖
{𝑥})) ↔ dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥}))) |
41 | 38, 40 | mpbird 258 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin →
(♯‘dom (𝐹
∖ {𝑥})) ≤
(♯‘(𝐹 ∖
{𝑥}))) |
42 | 34 | ltp1d 11407 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin →
(♯‘(𝐹 ∖
{𝑥})) <
((♯‘(𝐹 ∖
{𝑥})) +
1)) |
43 | 31, 34, 36, 41, 42 | lelttrd 10634 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Fin →
(♯‘dom (𝐹
∖ {𝑥})) <
((♯‘(𝐹 ∖
{𝑥})) +
1)) |
44 | 43 | 3ad2ant1 1124 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) →
(♯‘dom (𝐹
∖ {𝑥})) <
((♯‘(𝐹 ∖
{𝑥})) +
1)) |
45 | 25, 44 | eqbrtrd 4978 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) →
(♯‘dom ((𝐹
∖ {𝑥}) ∪ {𝑥})) < ((♯‘(𝐹 ∖ {𝑥})) + 1)) |
46 | | snfi 8432 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑥} ∈ Fin |
47 | | incom 4094 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∖ {𝑥}) ∩ {𝑥}) = ({𝑥} ∩ (𝐹 ∖ {𝑥})) |
48 | | disjdif 4329 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝑥} ∩ (𝐹 ∖ {𝑥})) = ∅ |
49 | 47, 48 | eqtri 2817 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∖ {𝑥}) ∩ {𝑥}) = ∅ |
50 | | hashun 13579 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∖ {𝑥}) ∈ Fin ∧ {𝑥} ∈ Fin ∧ ((𝐹 ∖ {𝑥}) ∩ {𝑥}) = ∅) → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥}))) |
51 | 46, 49, 50 | mp3an23 1443 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∖ {𝑥}) ∈ Fin → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥}))) |
52 | 26, 51 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Fin →
(♯‘((𝐹 ∖
{𝑥}) ∪ {𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥}))) |
53 | | hashsng 13567 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ V →
(♯‘{𝑥}) =
1) |
54 | 53 | elv 3437 |
. . . . . . . . . . . . . . . 16
⊢
(♯‘{𝑥})
= 1 |
55 | 54 | oveq2i 7018 |
. . . . . . . . . . . . . . 15
⊢
((♯‘(𝐹
∖ {𝑥})) +
(♯‘{𝑥})) =
((♯‘(𝐹 ∖
{𝑥})) + 1) |
56 | 52, 55 | syl6req 2846 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Fin →
((♯‘(𝐹 ∖
{𝑥})) + 1) =
(♯‘((𝐹 ∖
{𝑥}) ∪ {𝑥}))) |
57 | 56 | 3ad2ant1 1124 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) →
((♯‘(𝐹 ∖
{𝑥})) + 1) =
(♯‘((𝐹 ∖
{𝑥}) ∪ {𝑥}))) |
58 | 45, 57 | breqtrd 4982 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) →
(♯‘dom ((𝐹
∖ {𝑥}) ∪ {𝑥})) < (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥}))) |
59 | | difsnid 4644 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝐹 → ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = 𝐹) |
60 | 59 | dmeqd 5652 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐹 → dom ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = dom 𝐹) |
61 | 60 | fveq2d 6534 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐹 → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘dom 𝐹)) |
62 | 61 | 3ad2ant2 1125 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) →
(♯‘dom ((𝐹
∖ {𝑥}) ∪ {𝑥})) = (♯‘dom 𝐹)) |
63 | 59 | fveq2d 6534 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐹 → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘𝐹)) |
64 | 63 | 3ad2ant2 1125 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) →
(♯‘((𝐹 ∖
{𝑥}) ∪ {𝑥})) = (♯‘𝐹)) |
65 | 58, 62, 64 | 3brtr3d 4987 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) →
(♯‘dom 𝐹) <
(♯‘𝐹)) |
66 | 65 | rexlimdv3a 3246 |
. . . . . . . . . 10
⊢ (𝐹 ∈ Fin → (∃𝑥 ∈ 𝐹 ¬ 𝑥 ∈ (V × V) →
(♯‘dom 𝐹) <
(♯‘𝐹))) |
67 | 14, 66 | syl5bi 243 |
. . . . . . . . 9
⊢ (𝐹 ∈ Fin → (¬ Rel
𝐹 → (♯‘dom
𝐹) <
(♯‘𝐹))) |
68 | 67 | imp 407 |
. . . . . . . 8
⊢ ((𝐹 ∈ Fin ∧ ¬ Rel
𝐹) →
(♯‘dom 𝐹) <
(♯‘𝐹)) |
69 | 8, 68 | gtned 10611 |
. . . . . . 7
⊢ ((𝐹 ∈ Fin ∧ ¬ Rel
𝐹) →
(♯‘𝐹) ≠
(♯‘dom 𝐹)) |
70 | 69 | ex 413 |
. . . . . 6
⊢ (𝐹 ∈ Fin → (¬ Rel
𝐹 →
(♯‘𝐹) ≠
(♯‘dom 𝐹))) |
71 | 70 | necon4bd 3002 |
. . . . 5
⊢ (𝐹 ∈ Fin →
((♯‘𝐹) =
(♯‘dom 𝐹)
→ Rel 𝐹)) |
72 | 71 | imp 407 |
. . . 4
⊢ ((𝐹 ∈ Fin ∧
(♯‘𝐹) =
(♯‘dom 𝐹))
→ Rel 𝐹) |
73 | | 2nalexn 1807 |
. . . . . . . 8
⊢ (¬
∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥∃𝑦 ¬ ∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧)) |
74 | | df-ne 2983 |
. . . . . . . . . . . . 13
⊢ (𝑦 ≠ 𝑧 ↔ ¬ 𝑦 = 𝑧) |
75 | 74 | anbi2i 622 |
. . . . . . . . . . . 12
⊢
(((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) ↔ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)) |
76 | | annim 404 |
. . . . . . . . . . . 12
⊢
(((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧) ↔ ¬ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧)) |
77 | 75, 76 | bitri 276 |
. . . . . . . . . . 11
⊢
(((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) ↔ ¬ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧)) |
78 | 77 | exbii 1827 |
. . . . . . . . . 10
⊢
(∃𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) ↔ ∃𝑧 ¬ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧)) |
79 | | exnal 1806 |
. . . . . . . . . 10
⊢
(∃𝑧 ¬
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧)) |
80 | 78, 79 | bitr2i 277 |
. . . . . . . . 9
⊢ (¬
∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) |
81 | 80 | 2exbii 1828 |
. . . . . . . 8
⊢
(∃𝑥∃𝑦 ¬ ∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥∃𝑦∃𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) |
82 | 73, 81 | bitri 276 |
. . . . . . 7
⊢ (¬
∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥∃𝑦∃𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) |
83 | 7 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘dom 𝐹) ∈
ℝ) |
84 | | 2re 11548 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ |
85 | | diffi 8586 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ Fin → (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin) |
86 | | dmfi 8638 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin → dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin) |
87 | 85, 86 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin → dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin) |
88 | | hashcl 13555 |
. . . . . . . . . . . . . . . 16
⊢ (dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin → (♯‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈
ℕ0) |
89 | 87, 88 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Fin →
(♯‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈
ℕ0) |
90 | 89 | nn0red 11793 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Fin →
(♯‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ) |
91 | 90 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ) |
92 | | readdcl 10455 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℝ ∧ (♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ) → (2 +
(♯‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ∈ ℝ) |
93 | 84, 91, 92 | sylancr 587 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ∈ ℝ) |
94 | | hashcl 13555 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Fin →
(♯‘𝐹) ∈
ℕ0) |
95 | 94 | nn0red 11793 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ Fin →
(♯‘𝐹) ∈
ℝ) |
96 | 95 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘𝐹) ∈ ℝ) |
97 | | 1re 10476 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ |
98 | | readdcl 10455 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℝ ∧ (♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ) → (1 +
(♯‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ∈ ℝ) |
99 | 97, 90, 98 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Fin → (1 +
(♯‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ∈ ℝ) |
100 | 99 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (1 + (♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ∈ ℝ) |
101 | 84, 90, 92 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Fin → (2 +
(♯‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ∈ ℝ) |
102 | 101 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ∈ ℝ) |
103 | | dmun 5657 |
. . . . . . . . . . . . . . . . . 18
⊢ dom
({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) = (dom {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) |
104 | | opex 5241 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
〈𝑥, 𝑦〉 ∈ V |
105 | | opex 5241 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
〈𝑥, 𝑧〉 ∈ V |
106 | 104, 105 | prss 4654 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ↔ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ⊆ 𝐹) |
107 | | undif 4338 |
. . . . . . . . . . . . . . . . . . . 20
⊢
({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ⊆ 𝐹 ↔ ({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) = 𝐹) |
108 | 106, 107 | sylbb 220 |
. . . . . . . . . . . . . . . . . . 19
⊢
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → ({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) = 𝐹) |
109 | 108 | dmeqd 5652 |
. . . . . . . . . . . . . . . . . 18
⊢
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → dom ({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) = dom 𝐹) |
110 | 103, 109 | syl5reqr 2844 |
. . . . . . . . . . . . . . . . 17
⊢
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → dom 𝐹 = (dom {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) |
111 | | vex 3435 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑦 ∈ V |
112 | | vex 3435 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑧 ∈ V |
113 | 111, 112 | dmprop 5941 |
. . . . . . . . . . . . . . . . . . 19
⊢ dom
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} = {𝑥, 𝑥} |
114 | | dfsn2 4479 |
. . . . . . . . . . . . . . . . . . 19
⊢ {𝑥} = {𝑥, 𝑥} |
115 | 113, 114 | eqtr4i 2820 |
. . . . . . . . . . . . . . . . . 18
⊢ dom
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} = {𝑥} |
116 | 115 | uneq1i 4051 |
. . . . . . . . . . . . . . . . 17
⊢ (dom
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) = ({𝑥} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) |
117 | 110, 116 | syl6eq 2845 |
. . . . . . . . . . . . . . . 16
⊢
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → dom 𝐹 = ({𝑥} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) |
118 | 117 | fveq2d 6534 |
. . . . . . . . . . . . . . 15
⊢
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → (♯‘dom 𝐹) = (♯‘({𝑥} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
119 | 118 | ad2antrl 724 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘dom 𝐹) = (♯‘({𝑥} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
120 | | hashun2 13580 |
. . . . . . . . . . . . . . . . 17
⊢ (({𝑥} ∈ Fin ∧ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin) →
(♯‘({𝑥} ∪
dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ ((♯‘{𝑥}) + (♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
121 | 46, 87, 120 | sylancr 587 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin →
(♯‘({𝑥} ∪
dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ ((♯‘{𝑥}) + (♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
122 | 54 | oveq1i 7017 |
. . . . . . . . . . . . . . . 16
⊢
((♯‘{𝑥})
+ (♯‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = (1 + (♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) |
123 | 121, 122 | syl6breq 4997 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Fin →
(♯‘({𝑥} ∪
dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ (1 + (♯‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
124 | 123 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘({𝑥} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ (1 + (♯‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
125 | 119, 124 | eqbrtrd 4978 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘dom 𝐹) ≤ (1 + (♯‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
126 | | 1lt2 11645 |
. . . . . . . . . . . . . . 15
⊢ 1 <
2 |
127 | | ltadd1 10944 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℝ ∧ 2 ∈ ℝ ∧ (♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ) → (1 < 2
↔ (1 + (♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) < (2 + (♯‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))))) |
128 | 97, 84, 90, 127 | mp3an12i 1455 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Fin → (1 < 2
↔ (1 + (♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) < (2 + (♯‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))))) |
129 | 126, 128 | mpbii 234 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Fin → (1 +
(♯‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) < (2 + (♯‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
130 | 129 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (1 + (♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) < (2 + (♯‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
131 | 83, 100, 102, 125, 130 | lelttrd 10634 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘dom 𝐹) < (2 + (♯‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
132 | | fidomdm 8637 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin → dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ≼ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) |
133 | 85, 132 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin → dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ≼ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) |
134 | | hashdom 13576 |
. . . . . . . . . . . . . . . . 17
⊢ ((dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin ∧ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin) →
((♯‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ≤ (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ↔ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ≼ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) |
135 | 87, 85, 134 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin →
((♯‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ≤ (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ↔ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ≼ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) |
136 | 133, 135 | mpbird 258 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Fin →
(♯‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ≤ (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) |
137 | | hashcl 13555 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin →
(♯‘(𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈
ℕ0) |
138 | 85, 137 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ Fin →
(♯‘(𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈
ℕ0) |
139 | 138 | nn0red 11793 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin →
(♯‘(𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ) |
140 | | leadd2 10946 |
. . . . . . . . . . . . . . . . 17
⊢
(((♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ ∧
(♯‘(𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ ∧ 2 ∈
ℝ) → ((♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ≤ (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ↔ (2 + (♯‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ (2 + (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))))) |
141 | 84, 140 | mp3an3 1440 |
. . . . . . . . . . . . . . . 16
⊢
(((♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ ∧
(♯‘(𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ) →
((♯‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ≤ (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ↔ (2 + (♯‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ (2 + (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))))) |
142 | 90, 139, 141 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Fin →
((♯‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ≤ (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ↔ (2 + (♯‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ (2 + (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))))) |
143 | 136, 142 | mpbid 233 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Fin → (2 +
(♯‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ (2 + (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
144 | 143 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ (2 + (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
145 | | prfi 8629 |
. . . . . . . . . . . . . . . . 17
⊢
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∈ Fin |
146 | | disjdif 4329 |
. . . . . . . . . . . . . . . . 17
⊢
({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∩ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) = ∅ |
147 | | hashun 13579 |
. . . . . . . . . . . . . . . . 17
⊢
(({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∈ Fin ∧ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin ∧ ({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∩ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) = ∅) →
(♯‘({〈𝑥,
𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = ((♯‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) + (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
148 | 145, 146,
147 | mp3an13 1442 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin →
(♯‘({〈𝑥,
𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = ((♯‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) + (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
149 | 85, 148 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Fin →
(♯‘({〈𝑥,
𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = ((♯‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) + (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
150 | 149 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = ((♯‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) + (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
151 | 108 | fveq2d 6534 |
. . . . . . . . . . . . . . 15
⊢
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → (♯‘({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = (♯‘𝐹)) |
152 | 151 | ad2antrl 724 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = (♯‘𝐹)) |
153 | | vex 3435 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑥 ∈ V |
154 | 153, 111 | opth 5253 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈𝑥, 𝑦〉 = 〈𝑥, 𝑧〉 ↔ (𝑥 = 𝑥 ∧ 𝑦 = 𝑧)) |
155 | 154 | simprbi 497 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑥, 𝑦〉 = 〈𝑥, 𝑧〉 → 𝑦 = 𝑧) |
156 | 155 | necon3i 3014 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ≠ 𝑧 → 〈𝑥, 𝑦〉 ≠ 〈𝑥, 𝑧〉) |
157 | | hashprg 13592 |
. . . . . . . . . . . . . . . . . 18
⊢
((〈𝑥, 𝑦〉 ∈ V ∧
〈𝑥, 𝑧〉 ∈ V) → (〈𝑥, 𝑦〉 ≠ 〈𝑥, 𝑧〉 ↔ (♯‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) = 2)) |
158 | 104, 105,
157 | mp2an 688 |
. . . . . . . . . . . . . . . . 17
⊢
(〈𝑥, 𝑦〉 ≠ 〈𝑥, 𝑧〉 ↔ (♯‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) = 2) |
159 | 156, 158 | sylib 219 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ≠ 𝑧 → (♯‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) = 2) |
160 | 159 | oveq1d 7022 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ≠ 𝑧 → ((♯‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) + (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = (2 + (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
161 | 160 | ad2antll 725 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → ((♯‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) + (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = (2 + (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) |
162 | 150, 152,
161 | 3eqtr3rd 2838 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = (♯‘𝐹)) |
163 | 144, 162 | breqtrd 4982 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ (♯‘𝐹)) |
164 | 83, 93, 96, 131, 163 | ltletrd 10636 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘dom 𝐹) < (♯‘𝐹)) |
165 | 83, 164 | gtned 10611 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘𝐹) ≠ (♯‘dom 𝐹)) |
166 | 165 | ex 413 |
. . . . . . . . 9
⊢ (𝐹 ∈ Fin →
(((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹))) |
167 | 166 | exlimdv 1909 |
. . . . . . . 8
⊢ (𝐹 ∈ Fin → (∃𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹))) |
168 | 167 | exlimdvv 1910 |
. . . . . . 7
⊢ (𝐹 ∈ Fin → (∃𝑥∃𝑦∃𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹))) |
169 | 82, 168 | syl5bi 243 |
. . . . . 6
⊢ (𝐹 ∈ Fin → (¬
∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹))) |
170 | 169 | necon4bd 3002 |
. . . . 5
⊢ (𝐹 ∈ Fin →
((♯‘𝐹) =
(♯‘dom 𝐹)
→ ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧))) |
171 | 170 | imp 407 |
. . . 4
⊢ ((𝐹 ∈ Fin ∧
(♯‘𝐹) =
(♯‘dom 𝐹))
→ ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧)) |
172 | | dffun4 6229 |
. . . 4
⊢ (Fun
𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧))) |
173 | 72, 171, 172 | sylanbrc 583 |
. . 3
⊢ ((𝐹 ∈ Fin ∧
(♯‘𝐹) =
(♯‘dom 𝐹))
→ Fun 𝐹) |
174 | 173 | ex 413 |
. 2
⊢ (𝐹 ∈ Fin →
((♯‘𝐹) =
(♯‘dom 𝐹)
→ Fun 𝐹)) |
175 | 3, 174 | impbid2 227 |
1
⊢ (𝐹 ∈ Fin → (Fun 𝐹 ↔ (♯‘𝐹) = (♯‘dom 𝐹))) |