| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | hashv01gt1 14385 | . . 3
⊢ (𝐷 ∈ 𝑉 → ((♯‘𝐷) = 0 ∨ (♯‘𝐷) = 1 ∨ 1 < (♯‘𝐷))) | 
| 2 |  | hasheq0 14403 | . . . . . 6
⊢ (𝐷 ∈ 𝑉 → ((♯‘𝐷) = 0 ↔ 𝐷 = ∅)) | 
| 3 |  | rexeq 3321 | . . . . . . 7
⊢ (𝐷 = ∅ → (∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 ↔ ∃𝑥 ∈ ∅ ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦)) | 
| 4 |  | rex0 4359 | . . . . . . . 8
⊢  ¬
∃𝑥 ∈ ∅
∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 | 
| 5 |  | pm2.21 123 | . . . . . . . 8
⊢ (¬
∃𝑥 ∈ ∅
∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 → (∃𝑥 ∈ ∅ ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 → 2 ≤ (♯‘𝐷))) | 
| 6 | 4, 5 | mp1i 13 | . . . . . . 7
⊢ (𝐷 = ∅ → (∃𝑥 ∈ ∅ ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 → 2 ≤ (♯‘𝐷))) | 
| 7 | 3, 6 | sylbid 240 | . . . . . 6
⊢ (𝐷 = ∅ → (∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 → 2 ≤ (♯‘𝐷))) | 
| 8 | 2, 7 | biimtrdi 253 | . . . . 5
⊢ (𝐷 ∈ 𝑉 → ((♯‘𝐷) = 0 → (∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 → 2 ≤ (♯‘𝐷)))) | 
| 9 | 8 | com12 32 | . . . 4
⊢
((♯‘𝐷) =
0 → (𝐷 ∈ 𝑉 → (∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 → 2 ≤ (♯‘𝐷)))) | 
| 10 |  | hash1snb 14459 | . . . . . 6
⊢ (𝐷 ∈ 𝑉 → ((♯‘𝐷) = 1 ↔ ∃𝑧 𝐷 = {𝑧})) | 
| 11 |  | rexeq 3321 | . . . . . . . . . 10
⊢ (𝐷 = {𝑧} → (∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 ↔ ∃𝑦 ∈ {𝑧}𝑥 ≠ 𝑦)) | 
| 12 | 11 | rexeqbi1dv 3338 | . . . . . . . . 9
⊢ (𝐷 = {𝑧} → (∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 ↔ ∃𝑥 ∈ {𝑧}∃𝑦 ∈ {𝑧}𝑥 ≠ 𝑦)) | 
| 13 |  | vex 3483 | . . . . . . . . . . 11
⊢ 𝑧 ∈ V | 
| 14 |  | neeq1 3002 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝑥 ≠ 𝑦 ↔ 𝑧 ≠ 𝑦)) | 
| 15 | 14 | rexbidv 3178 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (∃𝑦 ∈ {𝑧}𝑥 ≠ 𝑦 ↔ ∃𝑦 ∈ {𝑧}𝑧 ≠ 𝑦)) | 
| 16 | 13, 15 | rexsn 4681 | . . . . . . . . . 10
⊢
(∃𝑥 ∈
{𝑧}∃𝑦 ∈ {𝑧}𝑥 ≠ 𝑦 ↔ ∃𝑦 ∈ {𝑧}𝑧 ≠ 𝑦) | 
| 17 |  | neeq2 3003 | . . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → (𝑧 ≠ 𝑦 ↔ 𝑧 ≠ 𝑧)) | 
| 18 | 13, 17 | rexsn 4681 | . . . . . . . . . 10
⊢
(∃𝑦 ∈
{𝑧}𝑧 ≠ 𝑦 ↔ 𝑧 ≠ 𝑧) | 
| 19 | 16, 18 | bitri 275 | . . . . . . . . 9
⊢
(∃𝑥 ∈
{𝑧}∃𝑦 ∈ {𝑧}𝑥 ≠ 𝑦 ↔ 𝑧 ≠ 𝑧) | 
| 20 | 12, 19 | bitrdi 287 | . . . . . . . 8
⊢ (𝐷 = {𝑧} → (∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 ↔ 𝑧 ≠ 𝑧)) | 
| 21 |  | equid 2010 | . . . . . . . . 9
⊢ 𝑧 = 𝑧 | 
| 22 |  | eqneqall 2950 | . . . . . . . . 9
⊢ (𝑧 = 𝑧 → (𝑧 ≠ 𝑧 → 2 ≤ (♯‘𝐷))) | 
| 23 | 21, 22 | mp1i 13 | . . . . . . . 8
⊢ (𝐷 = {𝑧} → (𝑧 ≠ 𝑧 → 2 ≤ (♯‘𝐷))) | 
| 24 | 20, 23 | sylbid 240 | . . . . . . 7
⊢ (𝐷 = {𝑧} → (∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 → 2 ≤ (♯‘𝐷))) | 
| 25 | 24 | exlimiv 1929 | . . . . . 6
⊢
(∃𝑧 𝐷 = {𝑧} → (∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 → 2 ≤ (♯‘𝐷))) | 
| 26 | 10, 25 | biimtrdi 253 | . . . . 5
⊢ (𝐷 ∈ 𝑉 → ((♯‘𝐷) = 1 → (∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 → 2 ≤ (♯‘𝐷)))) | 
| 27 | 26 | com12 32 | . . . 4
⊢
((♯‘𝐷) =
1 → (𝐷 ∈ 𝑉 → (∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 → 2 ≤ (♯‘𝐷)))) | 
| 28 |  | hashnn0pnf 14382 | . . . . . . . 8
⊢ (𝐷 ∈ 𝑉 → ((♯‘𝐷) ∈ ℕ0 ∨
(♯‘𝐷) =
+∞)) | 
| 29 |  | 1z 12649 | . . . . . . . . . . 11
⊢ 1 ∈
ℤ | 
| 30 |  | nn0z 12640 | . . . . . . . . . . 11
⊢
((♯‘𝐷)
∈ ℕ0 → (♯‘𝐷) ∈ ℤ) | 
| 31 |  | zltp1le 12669 | . . . . . . . . . . . 12
⊢ ((1
∈ ℤ ∧ (♯‘𝐷) ∈ ℤ) → (1 <
(♯‘𝐷) ↔ (1
+ 1) ≤ (♯‘𝐷))) | 
| 32 | 31 | biimpd 229 | . . . . . . . . . . 11
⊢ ((1
∈ ℤ ∧ (♯‘𝐷) ∈ ℤ) → (1 <
(♯‘𝐷) → (1
+ 1) ≤ (♯‘𝐷))) | 
| 33 | 29, 30, 32 | sylancr 587 | . . . . . . . . . 10
⊢
((♯‘𝐷)
∈ ℕ0 → (1 < (♯‘𝐷) → (1 + 1) ≤ (♯‘𝐷))) | 
| 34 |  | df-2 12330 | . . . . . . . . . . 11
⊢ 2 = (1 +
1) | 
| 35 | 34 | breq1i 5149 | . . . . . . . . . 10
⊢ (2 ≤
(♯‘𝐷) ↔ (1
+ 1) ≤ (♯‘𝐷)) | 
| 36 | 33, 35 | imbitrrdi 252 | . . . . . . . . 9
⊢
((♯‘𝐷)
∈ ℕ0 → (1 < (♯‘𝐷) → 2 ≤ (♯‘𝐷))) | 
| 37 |  | 2re 12341 | . . . . . . . . . . . . 13
⊢ 2 ∈
ℝ | 
| 38 | 37 | rexri 11320 | . . . . . . . . . . . 12
⊢ 2 ∈
ℝ* | 
| 39 |  | pnfge 13173 | . . . . . . . . . . . 12
⊢ (2 ∈
ℝ* → 2 ≤ +∞) | 
| 40 | 38, 39 | mp1i 13 | . . . . . . . . . . 11
⊢
((♯‘𝐷) =
+∞ → 2 ≤ +∞) | 
| 41 |  | breq2 5146 | . . . . . . . . . . 11
⊢
((♯‘𝐷) =
+∞ → (2 ≤ (♯‘𝐷) ↔ 2 ≤ +∞)) | 
| 42 | 40, 41 | mpbird 257 | . . . . . . . . . 10
⊢
((♯‘𝐷) =
+∞ → 2 ≤ (♯‘𝐷)) | 
| 43 | 42 | a1d 25 | . . . . . . . . 9
⊢
((♯‘𝐷) =
+∞ → (1 < (♯‘𝐷) → 2 ≤ (♯‘𝐷))) | 
| 44 | 36, 43 | jaoi 857 | . . . . . . . 8
⊢
(((♯‘𝐷)
∈ ℕ0 ∨ (♯‘𝐷) = +∞) → (1 <
(♯‘𝐷) → 2
≤ (♯‘𝐷))) | 
| 45 | 28, 44 | syl 17 | . . . . . . 7
⊢ (𝐷 ∈ 𝑉 → (1 < (♯‘𝐷) → 2 ≤
(♯‘𝐷))) | 
| 46 | 45 | impcom 407 | . . . . . 6
⊢ ((1 <
(♯‘𝐷) ∧
𝐷 ∈ 𝑉) → 2 ≤ (♯‘𝐷)) | 
| 47 | 46 | a1d 25 | . . . . 5
⊢ ((1 <
(♯‘𝐷) ∧
𝐷 ∈ 𝑉) → (∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 → 2 ≤ (♯‘𝐷))) | 
| 48 | 47 | ex 412 | . . . 4
⊢ (1 <
(♯‘𝐷) →
(𝐷 ∈ 𝑉 → (∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 → 2 ≤ (♯‘𝐷)))) | 
| 49 | 9, 27, 48 | 3jaoi 1429 | . . 3
⊢
(((♯‘𝐷)
= 0 ∨ (♯‘𝐷)
= 1 ∨ 1 < (♯‘𝐷)) → (𝐷 ∈ 𝑉 → (∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 → 2 ≤ (♯‘𝐷)))) | 
| 50 | 1, 49 | mpcom 38 | . 2
⊢ (𝐷 ∈ 𝑉 → (∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 → 2 ≤ (♯‘𝐷))) | 
| 51 | 50 | imp 406 | 1
⊢ ((𝐷 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦) → 2 ≤ (♯‘𝐷)) |