| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | funfn 6596 | . . 3
⊢ (Fun
𝐹 ↔ 𝐹 Fn dom 𝐹) | 
| 2 |  | hashfn 14414 | . . 3
⊢ (𝐹 Fn dom 𝐹 → (♯‘𝐹) = (♯‘dom 𝐹)) | 
| 3 | 1, 2 | sylbi 217 | . 2
⊢ (Fun
𝐹 →
(♯‘𝐹) =
(♯‘dom 𝐹)) | 
| 4 |  | dmfi 9375 | . . . . . . . . . . 11
⊢ (𝐹 ∈ Fin → dom 𝐹 ∈ Fin) | 
| 5 |  | hashcl 14395 | . . . . . . . . . . 11
⊢ (dom
𝐹 ∈ Fin →
(♯‘dom 𝐹)
∈ ℕ0) | 
| 6 | 4, 5 | syl 17 | . . . . . . . . . 10
⊢ (𝐹 ∈ Fin →
(♯‘dom 𝐹)
∈ ℕ0) | 
| 7 | 6 | nn0red 12588 | . . . . . . . . 9
⊢ (𝐹 ∈ Fin →
(♯‘dom 𝐹)
∈ ℝ) | 
| 8 | 7 | adantr 480 | . . . . . . . 8
⊢ ((𝐹 ∈ Fin ∧ ¬ Rel
𝐹) →
(♯‘dom 𝐹)
∈ ℝ) | 
| 9 |  | df-rel 5692 | . . . . . . . . . . . . 13
⊢ (Rel
𝐹 ↔ 𝐹 ⊆ (V × V)) | 
| 10 |  | dfss3 3972 | . . . . . . . . . . . . 13
⊢ (𝐹 ⊆ (V × V) ↔
∀𝑥 ∈ 𝐹 𝑥 ∈ (V × V)) | 
| 11 | 9, 10 | bitri 275 | . . . . . . . . . . . 12
⊢ (Rel
𝐹 ↔ ∀𝑥 ∈ 𝐹 𝑥 ∈ (V × V)) | 
| 12 | 11 | notbii 320 | . . . . . . . . . . 11
⊢ (¬
Rel 𝐹 ↔ ¬
∀𝑥 ∈ 𝐹 𝑥 ∈ (V × V)) | 
| 13 |  | rexnal 3100 | . . . . . . . . . . 11
⊢
(∃𝑥 ∈
𝐹 ¬ 𝑥 ∈ (V × V) ↔ ¬
∀𝑥 ∈ 𝐹 𝑥 ∈ (V × V)) | 
| 14 | 12, 13 | bitr4i 278 | . . . . . . . . . 10
⊢ (¬
Rel 𝐹 ↔ ∃𝑥 ∈ 𝐹 ¬ 𝑥 ∈ (V × V)) | 
| 15 |  | dmun 5921 | . . . . . . . . . . . . . . . 16
⊢ dom
((𝐹 ∖ {𝑥}) ∪ {𝑥}) = (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}) | 
| 16 | 15 | fveq2i 6909 | . . . . . . . . . . . . . . 15
⊢
(♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘(dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥})) | 
| 17 |  | dmsnn0 6227 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (V × V) ↔ dom
{𝑥} ≠
∅) | 
| 18 | 17 | biimpri 228 | . . . . . . . . . . . . . . . . . . . 20
⊢ (dom
{𝑥} ≠ ∅ →
𝑥 ∈ (V ×
V)) | 
| 19 | 18 | necon1bi 2969 | . . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑥 ∈ (V × V)
→ dom {𝑥} =
∅) | 
| 20 | 19 | 3ad2ant3 1136 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → dom {𝑥} = ∅) | 
| 21 | 20 | uneq2d 4168 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}) = (dom (𝐹 ∖ {𝑥}) ∪ ∅)) | 
| 22 |  | un0 4394 | . . . . . . . . . . . . . . . . 17
⊢ (dom
(𝐹 ∖ {𝑥}) ∪ ∅) = dom (𝐹 ∖ {𝑥}) | 
| 23 | 21, 22 | eqtrdi 2793 | . . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) → (dom (𝐹 ∖ {𝑥}) ∪ dom {𝑥}) = dom (𝐹 ∖ {𝑥})) | 
| 24 | 23 | fveq2d 6910 | . . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) →
(♯‘(dom (𝐹
∖ {𝑥}) ∪ dom
{𝑥})) = (♯‘dom
(𝐹 ∖ {𝑥}))) | 
| 25 | 16, 24 | eqtrid 2789 | . . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) →
(♯‘dom ((𝐹
∖ {𝑥}) ∪ {𝑥})) = (♯‘dom (𝐹 ∖ {𝑥}))) | 
| 26 |  | diffi 9215 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 ∈ Fin → (𝐹 ∖ {𝑥}) ∈ Fin) | 
| 27 |  | dmfi 9375 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 ∖ {𝑥}) ∈ Fin → dom (𝐹 ∖ {𝑥}) ∈ Fin) | 
| 28 | 26, 27 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ Fin → dom (𝐹 ∖ {𝑥}) ∈ Fin) | 
| 29 |  | hashcl 14395 | . . . . . . . . . . . . . . . . . 18
⊢ (dom
(𝐹 ∖ {𝑥}) ∈ Fin →
(♯‘dom (𝐹
∖ {𝑥})) ∈
ℕ0) | 
| 30 | 28, 29 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ Fin →
(♯‘dom (𝐹
∖ {𝑥})) ∈
ℕ0) | 
| 31 | 30 | nn0red 12588 | . . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin →
(♯‘dom (𝐹
∖ {𝑥})) ∈
ℝ) | 
| 32 |  | hashcl 14395 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∖ {𝑥}) ∈ Fin → (♯‘(𝐹 ∖ {𝑥})) ∈
ℕ0) | 
| 33 | 26, 32 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ Fin →
(♯‘(𝐹 ∖
{𝑥})) ∈
ℕ0) | 
| 34 | 33 | nn0red 12588 | . . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin →
(♯‘(𝐹 ∖
{𝑥})) ∈
ℝ) | 
| 35 |  | peano2re 11434 | . . . . . . . . . . . . . . . . 17
⊢
((♯‘(𝐹
∖ {𝑥})) ∈
ℝ → ((♯‘(𝐹 ∖ {𝑥})) + 1) ∈ ℝ) | 
| 36 | 34, 35 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin →
((♯‘(𝐹 ∖
{𝑥})) + 1) ∈
ℝ) | 
| 37 |  | fidomdm 9374 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∖ {𝑥}) ∈ Fin → dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥})) | 
| 38 | 26, 37 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ Fin → dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥})) | 
| 39 |  | hashdom 14418 | . . . . . . . . . . . . . . . . . 18
⊢ ((dom
(𝐹 ∖ {𝑥}) ∈ Fin ∧ (𝐹 ∖ {𝑥}) ∈ Fin) → ((♯‘dom
(𝐹 ∖ {𝑥})) ≤ (♯‘(𝐹 ∖ {𝑥})) ↔ dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥}))) | 
| 40 | 28, 26, 39 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ Fin →
((♯‘dom (𝐹
∖ {𝑥})) ≤
(♯‘(𝐹 ∖
{𝑥})) ↔ dom (𝐹 ∖ {𝑥}) ≼ (𝐹 ∖ {𝑥}))) | 
| 41 | 38, 40 | mpbird 257 | . . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin →
(♯‘dom (𝐹
∖ {𝑥})) ≤
(♯‘(𝐹 ∖
{𝑥}))) | 
| 42 | 34 | ltp1d 12198 | . . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin →
(♯‘(𝐹 ∖
{𝑥})) <
((♯‘(𝐹 ∖
{𝑥})) +
1)) | 
| 43 | 31, 34, 36, 41, 42 | lelttrd 11419 | . . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Fin →
(♯‘dom (𝐹
∖ {𝑥})) <
((♯‘(𝐹 ∖
{𝑥})) +
1)) | 
| 44 | 43 | 3ad2ant1 1134 | . . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) →
(♯‘dom (𝐹
∖ {𝑥})) <
((♯‘(𝐹 ∖
{𝑥})) +
1)) | 
| 45 | 25, 44 | eqbrtrd 5165 | . . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) →
(♯‘dom ((𝐹
∖ {𝑥}) ∪ {𝑥})) < ((♯‘(𝐹 ∖ {𝑥})) + 1)) | 
| 46 |  | snfi 9083 | . . . . . . . . . . . . . . . . 17
⊢ {𝑥} ∈ Fin | 
| 47 |  | disjdifr 4473 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∖ {𝑥}) ∩ {𝑥}) = ∅ | 
| 48 |  | hashun 14421 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∖ {𝑥}) ∈ Fin ∧ {𝑥} ∈ Fin ∧ ((𝐹 ∖ {𝑥}) ∩ {𝑥}) = ∅) → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥}))) | 
| 49 | 46, 47, 48 | mp3an23 1455 | . . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∖ {𝑥}) ∈ Fin → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥}))) | 
| 50 | 26, 49 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Fin →
(♯‘((𝐹 ∖
{𝑥}) ∪ {𝑥})) = ((♯‘(𝐹 ∖ {𝑥})) + (♯‘{𝑥}))) | 
| 51 |  | hashsng 14408 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ V →
(♯‘{𝑥}) =
1) | 
| 52 | 51 | elv 3485 | . . . . . . . . . . . . . . . 16
⊢
(♯‘{𝑥})
= 1 | 
| 53 | 52 | oveq2i 7442 | . . . . . . . . . . . . . . 15
⊢
((♯‘(𝐹
∖ {𝑥})) +
(♯‘{𝑥})) =
((♯‘(𝐹 ∖
{𝑥})) + 1) | 
| 54 | 50, 53 | eqtr2di 2794 | . . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Fin →
((♯‘(𝐹 ∖
{𝑥})) + 1) =
(♯‘((𝐹 ∖
{𝑥}) ∪ {𝑥}))) | 
| 55 | 54 | 3ad2ant1 1134 | . . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) →
((♯‘(𝐹 ∖
{𝑥})) + 1) =
(♯‘((𝐹 ∖
{𝑥}) ∪ {𝑥}))) | 
| 56 | 45, 55 | breqtrd 5169 | . . . . . . . . . . . 12
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) →
(♯‘dom ((𝐹
∖ {𝑥}) ∪ {𝑥})) < (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥}))) | 
| 57 |  | difsnid 4810 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝐹 → ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = 𝐹) | 
| 58 | 57 | dmeqd 5916 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐹 → dom ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = dom 𝐹) | 
| 59 | 58 | fveq2d 6910 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐹 → (♯‘dom ((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘dom 𝐹)) | 
| 60 | 59 | 3ad2ant2 1135 | . . . . . . . . . . . 12
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) →
(♯‘dom ((𝐹
∖ {𝑥}) ∪ {𝑥})) = (♯‘dom 𝐹)) | 
| 61 | 57 | fveq2d 6910 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐹 → (♯‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = (♯‘𝐹)) | 
| 62 | 61 | 3ad2ant2 1135 | . . . . . . . . . . . 12
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) →
(♯‘((𝐹 ∖
{𝑥}) ∪ {𝑥})) = (♯‘𝐹)) | 
| 63 | 56, 60, 62 | 3brtr3d 5174 | . . . . . . . . . . 11
⊢ ((𝐹 ∈ Fin ∧ 𝑥 ∈ 𝐹 ∧ ¬ 𝑥 ∈ (V × V)) →
(♯‘dom 𝐹) <
(♯‘𝐹)) | 
| 64 | 63 | rexlimdv3a 3159 | . . . . . . . . . 10
⊢ (𝐹 ∈ Fin → (∃𝑥 ∈ 𝐹 ¬ 𝑥 ∈ (V × V) →
(♯‘dom 𝐹) <
(♯‘𝐹))) | 
| 65 | 14, 64 | biimtrid 242 | . . . . . . . . 9
⊢ (𝐹 ∈ Fin → (¬ Rel
𝐹 → (♯‘dom
𝐹) <
(♯‘𝐹))) | 
| 66 | 65 | imp 406 | . . . . . . . 8
⊢ ((𝐹 ∈ Fin ∧ ¬ Rel
𝐹) →
(♯‘dom 𝐹) <
(♯‘𝐹)) | 
| 67 | 8, 66 | gtned 11396 | . . . . . . 7
⊢ ((𝐹 ∈ Fin ∧ ¬ Rel
𝐹) →
(♯‘𝐹) ≠
(♯‘dom 𝐹)) | 
| 68 | 67 | ex 412 | . . . . . 6
⊢ (𝐹 ∈ Fin → (¬ Rel
𝐹 →
(♯‘𝐹) ≠
(♯‘dom 𝐹))) | 
| 69 | 68 | necon4bd 2960 | . . . . 5
⊢ (𝐹 ∈ Fin →
((♯‘𝐹) =
(♯‘dom 𝐹)
→ Rel 𝐹)) | 
| 70 | 69 | imp 406 | . . . 4
⊢ ((𝐹 ∈ Fin ∧
(♯‘𝐹) =
(♯‘dom 𝐹))
→ Rel 𝐹) | 
| 71 |  | 2nalexn 1828 | . . . . . . . 8
⊢ (¬
∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥∃𝑦 ¬ ∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧)) | 
| 72 |  | df-ne 2941 | . . . . . . . . . . . . 13
⊢ (𝑦 ≠ 𝑧 ↔ ¬ 𝑦 = 𝑧) | 
| 73 | 72 | anbi2i 623 | . . . . . . . . . . . 12
⊢
(((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) ↔ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧)) | 
| 74 |  | annim 403 | . . . . . . . . . . . 12
⊢
(((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ ¬ 𝑦 = 𝑧) ↔ ¬ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧)) | 
| 75 | 73, 74 | bitri 275 | . . . . . . . . . . 11
⊢
(((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) ↔ ¬ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧)) | 
| 76 | 75 | exbii 1848 | . . . . . . . . . 10
⊢
(∃𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) ↔ ∃𝑧 ¬ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧)) | 
| 77 |  | exnal 1827 | . . . . . . . . . 10
⊢
(∃𝑧 ¬
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧) ↔ ¬ ∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧)) | 
| 78 | 76, 77 | bitr2i 276 | . . . . . . . . 9
⊢ (¬
∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) | 
| 79 | 78 | 2exbii 1849 | . . . . . . . 8
⊢
(∃𝑥∃𝑦 ¬ ∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥∃𝑦∃𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) | 
| 80 | 71, 79 | bitri 275 | . . . . . . 7
⊢ (¬
∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧) ↔ ∃𝑥∃𝑦∃𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) | 
| 81 | 7 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘dom 𝐹) ∈
ℝ) | 
| 82 |  | 2re 12340 | . . . . . . . . . . . . 13
⊢ 2 ∈
ℝ | 
| 83 |  | diffi 9215 | . . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ Fin → (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin) | 
| 84 |  | dmfi 9375 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin → dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin) | 
| 85 | 83, 84 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin → dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin) | 
| 86 |  | hashcl 14395 | . . . . . . . . . . . . . . . 16
⊢ (dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin → (♯‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈
ℕ0) | 
| 87 | 85, 86 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Fin →
(♯‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈
ℕ0) | 
| 88 | 87 | nn0red 12588 | . . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Fin →
(♯‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ) | 
| 89 | 88 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ) | 
| 90 |  | readdcl 11238 | . . . . . . . . . . . . 13
⊢ ((2
∈ ℝ ∧ (♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ) → (2 +
(♯‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ∈ ℝ) | 
| 91 | 82, 89, 90 | sylancr 587 | . . . . . . . . . . . 12
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ∈ ℝ) | 
| 92 |  | hashcl 14395 | . . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Fin →
(♯‘𝐹) ∈
ℕ0) | 
| 93 | 92 | nn0red 12588 | . . . . . . . . . . . . 13
⊢ (𝐹 ∈ Fin →
(♯‘𝐹) ∈
ℝ) | 
| 94 | 93 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘𝐹) ∈ ℝ) | 
| 95 |  | 1re 11261 | . . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ | 
| 96 |  | readdcl 11238 | . . . . . . . . . . . . . . 15
⊢ ((1
∈ ℝ ∧ (♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ) → (1 +
(♯‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ∈ ℝ) | 
| 97 | 95, 88, 96 | sylancr 587 | . . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Fin → (1 +
(♯‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ∈ ℝ) | 
| 98 | 97 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (1 + (♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ∈ ℝ) | 
| 99 | 82, 88, 90 | sylancr 587 | . . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Fin → (2 +
(♯‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ∈ ℝ) | 
| 100 | 99 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ∈ ℝ) | 
| 101 |  | opex 5469 | . . . . . . . . . . . . . . . . . . . . 21
⊢
〈𝑥, 𝑦〉 ∈ V | 
| 102 |  | opex 5469 | . . . . . . . . . . . . . . . . . . . . 21
⊢
〈𝑥, 𝑧〉 ∈ V | 
| 103 | 101, 102 | prss 4820 | . . . . . . . . . . . . . . . . . . . 20
⊢
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ↔ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ⊆ 𝐹) | 
| 104 |  | undif 4482 | . . . . . . . . . . . . . . . . . . . 20
⊢
({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ⊆ 𝐹 ↔ ({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) = 𝐹) | 
| 105 | 103, 104 | sylbb 219 | . . . . . . . . . . . . . . . . . . 19
⊢
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → ({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) = 𝐹) | 
| 106 | 105 | dmeqd 5916 | . . . . . . . . . . . . . . . . . 18
⊢
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → dom ({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) = dom 𝐹) | 
| 107 |  | dmun 5921 | . . . . . . . . . . . . . . . . . 18
⊢ dom
({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) = (dom {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) | 
| 108 | 106, 107 | eqtr3di 2792 | . . . . . . . . . . . . . . . . 17
⊢
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → dom 𝐹 = (dom {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) | 
| 109 |  | vex 3484 | . . . . . . . . . . . . . . . . . . . 20
⊢ 𝑦 ∈ V | 
| 110 |  | vex 3484 | . . . . . . . . . . . . . . . . . . . 20
⊢ 𝑧 ∈ V | 
| 111 | 109, 110 | dmprop 6237 | . . . . . . . . . . . . . . . . . . 19
⊢ dom
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} = {𝑥, 𝑥} | 
| 112 |  | dfsn2 4639 | . . . . . . . . . . . . . . . . . . 19
⊢ {𝑥} = {𝑥, 𝑥} | 
| 113 | 111, 112 | eqtr4i 2768 | . . . . . . . . . . . . . . . . . 18
⊢ dom
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} = {𝑥} | 
| 114 | 113 | uneq1i 4164 | . . . . . . . . . . . . . . . . 17
⊢ (dom
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) = ({𝑥} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) | 
| 115 | 108, 114 | eqtrdi 2793 | . . . . . . . . . . . . . . . 16
⊢
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → dom 𝐹 = ({𝑥} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) | 
| 116 | 115 | fveq2d 6910 | . . . . . . . . . . . . . . 15
⊢
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → (♯‘dom 𝐹) = (♯‘({𝑥} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) | 
| 117 | 116 | ad2antrl 728 | . . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘dom 𝐹) = (♯‘({𝑥} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) | 
| 118 |  | hashun2 14422 | . . . . . . . . . . . . . . . . 17
⊢ (({𝑥} ∈ Fin ∧ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin) →
(♯‘({𝑥} ∪
dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ ((♯‘{𝑥}) + (♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) | 
| 119 | 46, 85, 118 | sylancr 587 | . . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin →
(♯‘({𝑥} ∪
dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ ((♯‘{𝑥}) + (♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) | 
| 120 | 52 | oveq1i 7441 | . . . . . . . . . . . . . . . 16
⊢
((♯‘{𝑥})
+ (♯‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = (1 + (♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) | 
| 121 | 119, 120 | breqtrdi 5184 | . . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Fin →
(♯‘({𝑥} ∪
dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ (1 + (♯‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) | 
| 122 | 121 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘({𝑥} ∪ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ (1 + (♯‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) | 
| 123 | 117, 122 | eqbrtrd 5165 | . . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘dom 𝐹) ≤ (1 + (♯‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) | 
| 124 |  | 1lt2 12437 | . . . . . . . . . . . . . . 15
⊢ 1 <
2 | 
| 125 |  | ltadd1 11730 | . . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℝ ∧ 2 ∈ ℝ ∧ (♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ) → (1 < 2
↔ (1 + (♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) < (2 + (♯‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))))) | 
| 126 | 95, 82, 88, 125 | mp3an12i 1467 | . . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Fin → (1 < 2
↔ (1 + (♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) < (2 + (♯‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))))) | 
| 127 | 124, 126 | mpbii 233 | . . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Fin → (1 +
(♯‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) < (2 + (♯‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) | 
| 128 | 127 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (1 + (♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) < (2 + (♯‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) | 
| 129 | 81, 98, 100, 123, 128 | lelttrd 11419 | . . . . . . . . . . . 12
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘dom 𝐹) < (2 + (♯‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) | 
| 130 |  | fidomdm 9374 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin → dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ≼ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) | 
| 131 | 83, 130 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin → dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ≼ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) | 
| 132 |  | hashdom 14418 | . . . . . . . . . . . . . . . . 17
⊢ ((dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin ∧ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin) →
((♯‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ≤ (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ↔ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ≼ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) | 
| 133 | 85, 83, 132 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin →
((♯‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ≤ (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ↔ dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ≼ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) | 
| 134 | 131, 133 | mpbird 257 | . . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Fin →
(♯‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ≤ (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) | 
| 135 |  | hashcl 14395 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin →
(♯‘(𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈
ℕ0) | 
| 136 | 83, 135 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ Fin →
(♯‘(𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈
ℕ0) | 
| 137 | 136 | nn0red 12588 | . . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ Fin →
(♯‘(𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ) | 
| 138 |  | leadd2 11732 | . . . . . . . . . . . . . . . . 17
⊢
(((♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ ∧
(♯‘(𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ ∧ 2 ∈
ℝ) → ((♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ≤ (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ↔ (2 + (♯‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ (2 + (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))))) | 
| 139 | 82, 138 | mp3an3 1452 | . . . . . . . . . . . . . . . 16
⊢
(((♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ ∧
(♯‘(𝐹 ∖
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ∈ ℝ) →
((♯‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ≤ (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ↔ (2 + (♯‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ (2 + (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))))) | 
| 140 | 88, 137, 139 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Fin →
((♯‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ≤ (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) ↔ (2 + (♯‘dom
(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ (2 + (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))))) | 
| 141 | 134, 140 | mpbid 232 | . . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Fin → (2 +
(♯‘dom (𝐹
∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ (2 + (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) | 
| 142 | 141 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ (2 + (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) | 
| 143 |  | prfi 9363 | . . . . . . . . . . . . . . . . 17
⊢
{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∈ Fin | 
| 144 |  | disjdif 4472 | . . . . . . . . . . . . . . . . 17
⊢
({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∩ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) = ∅ | 
| 145 |  | hashun 14421 | . . . . . . . . . . . . . . . . 17
⊢
(({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∈ Fin ∧ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin ∧ ({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∩ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})) = ∅) →
(♯‘({〈𝑥,
𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = ((♯‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) + (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) | 
| 146 | 143, 144,
145 | mp3an13 1454 | . . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) ∈ Fin →
(♯‘({〈𝑥,
𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = ((♯‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) + (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) | 
| 147 | 83, 146 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Fin →
(♯‘({〈𝑥,
𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = ((♯‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) + (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) | 
| 148 | 147 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = ((♯‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) + (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) | 
| 149 | 105 | fveq2d 6910 | . . . . . . . . . . . . . . 15
⊢
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → (♯‘({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = (♯‘𝐹)) | 
| 150 | 149 | ad2antrl 728 | . . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘({〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉} ∪ (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = (♯‘𝐹)) | 
| 151 |  | vex 3484 | . . . . . . . . . . . . . . . . . . . 20
⊢ 𝑥 ∈ V | 
| 152 | 151, 109 | opth 5481 | . . . . . . . . . . . . . . . . . . 19
⊢
(〈𝑥, 𝑦〉 = 〈𝑥, 𝑧〉 ↔ (𝑥 = 𝑥 ∧ 𝑦 = 𝑧)) | 
| 153 | 152 | simprbi 496 | . . . . . . . . . . . . . . . . . 18
⊢
(〈𝑥, 𝑦〉 = 〈𝑥, 𝑧〉 → 𝑦 = 𝑧) | 
| 154 | 153 | necon3i 2973 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 ≠ 𝑧 → 〈𝑥, 𝑦〉 ≠ 〈𝑥, 𝑧〉) | 
| 155 |  | hashprg 14434 | . . . . . . . . . . . . . . . . . 18
⊢
((〈𝑥, 𝑦〉 ∈ V ∧
〈𝑥, 𝑧〉 ∈ V) → (〈𝑥, 𝑦〉 ≠ 〈𝑥, 𝑧〉 ↔ (♯‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) = 2)) | 
| 156 | 101, 102,
155 | mp2an 692 | . . . . . . . . . . . . . . . . 17
⊢
(〈𝑥, 𝑦〉 ≠ 〈𝑥, 𝑧〉 ↔ (♯‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) = 2) | 
| 157 | 154, 156 | sylib 218 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 ≠ 𝑧 → (♯‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) = 2) | 
| 158 | 157 | oveq1d 7446 | . . . . . . . . . . . . . . 15
⊢ (𝑦 ≠ 𝑧 → ((♯‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) + (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = (2 + (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) | 
| 159 | 158 | ad2antll 729 | . . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → ((♯‘{〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}) + (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = (2 + (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉})))) | 
| 160 | 148, 150,
159 | 3eqtr3rd 2786 | . . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (♯‘(𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) = (♯‘𝐹)) | 
| 161 | 142, 160 | breqtrd 5169 | . . . . . . . . . . . 12
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (2 + (♯‘dom (𝐹 ∖ {〈𝑥, 𝑦〉, 〈𝑥, 𝑧〉}))) ≤ (♯‘𝐹)) | 
| 162 | 81, 91, 94, 129, 161 | ltletrd 11421 | . . . . . . . . . . 11
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘dom 𝐹) < (♯‘𝐹)) | 
| 163 | 81, 162 | gtned 11396 | . . . . . . . . . 10
⊢ ((𝐹 ∈ Fin ∧ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧)) → (♯‘𝐹) ≠ (♯‘dom 𝐹)) | 
| 164 | 163 | ex 412 | . . . . . . . . 9
⊢ (𝐹 ∈ Fin →
(((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹))) | 
| 165 | 164 | exlimdv 1933 | . . . . . . . 8
⊢ (𝐹 ∈ Fin → (∃𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹))) | 
| 166 | 165 | exlimdvv 1934 | . . . . . . 7
⊢ (𝐹 ∈ Fin → (∃𝑥∃𝑦∃𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∧ 𝑦 ≠ 𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹))) | 
| 167 | 80, 166 | biimtrid 242 | . . . . . 6
⊢ (𝐹 ∈ Fin → (¬
∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧) → (♯‘𝐹) ≠ (♯‘dom 𝐹))) | 
| 168 | 167 | necon4bd 2960 | . . . . 5
⊢ (𝐹 ∈ Fin →
((♯‘𝐹) =
(♯‘dom 𝐹)
→ ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧))) | 
| 169 | 168 | imp 406 | . . . 4
⊢ ((𝐹 ∈ Fin ∧
(♯‘𝐹) =
(♯‘dom 𝐹))
→ ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧)) | 
| 170 |  | dffun4 6577 | . . . 4
⊢ (Fun
𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧))) | 
| 171 | 70, 169, 170 | sylanbrc 583 | . . 3
⊢ ((𝐹 ∈ Fin ∧
(♯‘𝐹) =
(♯‘dom 𝐹))
→ Fun 𝐹) | 
| 172 | 171 | ex 412 | . 2
⊢ (𝐹 ∈ Fin →
((♯‘𝐹) =
(♯‘dom 𝐹)
→ Fun 𝐹)) | 
| 173 | 3, 172 | impbid2 226 | 1
⊢ (𝐹 ∈ Fin → (Fun 𝐹 ↔ (♯‘𝐹) = (♯‘dom 𝐹))) |