Metamath Proof Explorer

Theorem hashge2el2difr

Description: A set with at least 2 different elements has size at least 2. (Contributed by AV, 14-Oct-2020)

Ref Expression
Assertion hashge2el2difr ( ( 𝐷 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 ) → 2 ≤ ( ♯ ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 hashv01gt1 ⊢ ( 𝐷 ∈ 𝑉 → ( ( ♯ ‘ 𝐷 ) = 0 ∨ ( ♯ ‘ 𝐷 ) = 1 ∨ 1 < ( ♯ ‘ 𝐷 ) ) )
2 hasheq0 ⊢ ( 𝐷 ∈ 𝑉 → ( ( ♯ ‘ 𝐷 ) = 0 ↔ 𝐷 = ∅ ) )
3 rexeq ⊢ ( 𝐷 = ∅ → ( ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 ↔ ∃ 𝑥 ∈ ∅ ∃ 𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 ) )
4 rex0 ⊢ ¬ ∃ 𝑥 ∈ ∅ ∃ 𝑦 ∈ 𝐷 𝑥 ≠ 𝑦
5 pm2.21 ⊢ ( ¬ ∃ 𝑥 ∈ ∅ ∃ 𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 → ( ∃ 𝑥 ∈ ∅ ∃ 𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 → 2 ≤ ( ♯ ‘ 𝐷 ) ) )
6 4 5 mp1i ⊢ ( 𝐷 = ∅ → ( ∃ 𝑥 ∈ ∅ ∃ 𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 → 2 ≤ ( ♯ ‘ 𝐷 ) ) )
7 3 6 sylbid ⊢ ( 𝐷 = ∅ → ( ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 → 2 ≤ ( ♯ ‘ 𝐷 ) ) )
8 2 7 syl6bi ⊢ ( 𝐷 ∈ 𝑉 → ( ( ♯ ‘ 𝐷 ) = 0 → ( ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 → 2 ≤ ( ♯ ‘ 𝐷 ) ) ) )
9 8 com12 ⊢ ( ( ♯ ‘ 𝐷 ) = 0 → ( 𝐷 ∈ 𝑉 → ( ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 → 2 ≤ ( ♯ ‘ 𝐷 ) ) ) )
10 hash1snb ⊢ ( 𝐷 ∈ 𝑉 → ( ( ♯ ‘ 𝐷 ) = 1 ↔ ∃ 𝑧 𝐷 = { 𝑧 } ) )
11 rexeq ⊢ ( 𝐷 = { 𝑧 } → ( ∃ 𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 ↔ ∃ 𝑦 ∈ { 𝑧 } 𝑥 ≠ 𝑦 ) )
12 11 rexeqbi1dv ⊢ ( 𝐷 = { 𝑧 } → ( ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 ↔ ∃ 𝑥 ∈ { 𝑧 } ∃ 𝑦 ∈ { 𝑧 } 𝑥 ≠ 𝑦 ) )
13 vex ⊢ 𝑧 ∈ V
14 neeq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ≠ 𝑦 ↔ 𝑧 ≠ 𝑦 ) )
15 14 rexbidv ⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑦 ∈ { 𝑧 } 𝑥 ≠ 𝑦 ↔ ∃ 𝑦 ∈ { 𝑧 } 𝑧 ≠ 𝑦 ) )
16 13 15 rexsn ⊢ ( ∃ 𝑥 ∈ { 𝑧 } ∃ 𝑦 ∈ { 𝑧 } 𝑥 ≠ 𝑦 ↔ ∃ 𝑦 ∈ { 𝑧 } 𝑧 ≠ 𝑦 )
17 neeq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑧 ≠ 𝑦 ↔ 𝑧 ≠ 𝑧 ) )
18 13 17 rexsn ⊢ ( ∃ 𝑦 ∈ { 𝑧 } 𝑧 ≠ 𝑦 ↔ 𝑧 ≠ 𝑧 )
19 16 18 bitri ⊢ ( ∃ 𝑥 ∈ { 𝑧 } ∃ 𝑦 ∈ { 𝑧 } 𝑥 ≠ 𝑦 ↔ 𝑧 ≠ 𝑧 )
20 12 19 bitrdi ⊢ ( 𝐷 = { 𝑧 } → ( ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 ↔ 𝑧 ≠ 𝑧 ) )
21 equid ⊢ 𝑧 = 𝑧
22 eqneqall ⊢ ( 𝑧 = 𝑧 → ( 𝑧 ≠ 𝑧 → 2 ≤ ( ♯ ‘ 𝐷 ) ) )
23 21 22 mp1i ⊢ ( 𝐷 = { 𝑧 } → ( 𝑧 ≠ 𝑧 → 2 ≤ ( ♯ ‘ 𝐷 ) ) )
24 20 23 sylbid ⊢ ( 𝐷 = { 𝑧 } → ( ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 → 2 ≤ ( ♯ ‘ 𝐷 ) ) )
25 24 exlimiv ⊢ ( ∃ 𝑧 𝐷 = { 𝑧 } → ( ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 → 2 ≤ ( ♯ ‘ 𝐷 ) ) )
26 10 25 syl6bi ⊢ ( 𝐷 ∈ 𝑉 → ( ( ♯ ‘ 𝐷 ) = 1 → ( ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 → 2 ≤ ( ♯ ‘ 𝐷 ) ) ) )
27 26 com12 ⊢ ( ( ♯ ‘ 𝐷 ) = 1 → ( 𝐷 ∈ 𝑉 → ( ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 → 2 ≤ ( ♯ ‘ 𝐷 ) ) ) )
28 hashnn0pnf ⊢ ( 𝐷 ∈ 𝑉 → ( ( ♯ ‘ 𝐷 ) ∈ ℕ0 ∨ ( ♯ ‘ 𝐷 ) = +∞ ) )
29 1z ⊢ 1 ∈ ℤ
30 nn0z ⊢ ( ( ♯ ‘ 𝐷 ) ∈ ℕ0 → ( ♯ ‘ 𝐷 ) ∈ ℤ )
31 zltp1le ⊢ ( ( 1 ∈ ℤ ∧ ( ♯ ‘ 𝐷 ) ∈ ℤ ) → ( 1 < ( ♯ ‘ 𝐷 ) ↔ ( 1 + 1 ) ≤ ( ♯ ‘ 𝐷 ) ) )
32 31 biimpd ⊢ ( ( 1 ∈ ℤ ∧ ( ♯ ‘ 𝐷 ) ∈ ℤ ) → ( 1 < ( ♯ ‘ 𝐷 ) → ( 1 + 1 ) ≤ ( ♯ ‘ 𝐷 ) ) )
33 29 30 32 sylancr ⊢ ( ( ♯ ‘ 𝐷 ) ∈ ℕ0 → ( 1 < ( ♯ ‘ 𝐷 ) → ( 1 + 1 ) ≤ ( ♯ ‘ 𝐷 ) ) )
34 df-2 ⊢ 2 = ( 1 + 1 )
35 34 breq1i ⊢ ( 2 ≤ ( ♯ ‘ 𝐷 ) ↔ ( 1 + 1 ) ≤ ( ♯ ‘ 𝐷 ) )
36 33 35 syl6ibr ⊢ ( ( ♯ ‘ 𝐷 ) ∈ ℕ0 → ( 1 < ( ♯ ‘ 𝐷 ) → 2 ≤ ( ♯ ‘ 𝐷 ) ) )
37 2re ⊢ 2 ∈ ℝ
38 37 rexri ⊢ 2 ∈ ℝ*
39 pnfge ⊢ ( 2 ∈ ℝ* → 2 ≤ +∞ )
40 38 39 mp1i ⊢ ( ( ♯ ‘ 𝐷 ) = +∞ → 2 ≤ +∞ )
41 breq2 ⊢ ( ( ♯ ‘ 𝐷 ) = +∞ → ( 2 ≤ ( ♯ ‘ 𝐷 ) ↔ 2 ≤ +∞ ) )
42 40 41 mpbird ⊢ ( ( ♯ ‘ 𝐷 ) = +∞ → 2 ≤ ( ♯ ‘ 𝐷 ) )
43 42 a1d ⊢ ( ( ♯ ‘ 𝐷 ) = +∞ → ( 1 < ( ♯ ‘ 𝐷 ) → 2 ≤ ( ♯ ‘ 𝐷 ) ) )
44 36 43 jaoi ⊢ ( ( ( ♯ ‘ 𝐷 ) ∈ ℕ0 ∨ ( ♯ ‘ 𝐷 ) = +∞ ) → ( 1 < ( ♯ ‘ 𝐷 ) → 2 ≤ ( ♯ ‘ 𝐷 ) ) )
45 28 44 syl ⊢ ( 𝐷 ∈ 𝑉 → ( 1 < ( ♯ ‘ 𝐷 ) → 2 ≤ ( ♯ ‘ 𝐷 ) ) )
46 45 impcom ⊢ ( ( 1 < ( ♯ ‘ 𝐷 ) ∧ 𝐷 ∈ 𝑉 ) → 2 ≤ ( ♯ ‘ 𝐷 ) )
47 46 a1d ⊢ ( ( 1 < ( ♯ ‘ 𝐷 ) ∧ 𝐷 ∈ 𝑉 ) → ( ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 → 2 ≤ ( ♯ ‘ 𝐷 ) ) )
48 47 ex ⊢ ( 1 < ( ♯ ‘ 𝐷 ) → ( 𝐷 ∈ 𝑉 → ( ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 → 2 ≤ ( ♯ ‘ 𝐷 ) ) ) )
49 9 27 48 3jaoi ⊢ ( ( ( ♯ ‘ 𝐷 ) = 0 ∨ ( ♯ ‘ 𝐷 ) = 1 ∨ 1 < ( ♯ ‘ 𝐷 ) ) → ( 𝐷 ∈ 𝑉 → ( ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 → 2 ≤ ( ♯ ‘ 𝐷 ) ) ) )
50 1 49 mpcom ⊢ ( 𝐷 ∈ 𝑉 → ( ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 → 2 ≤ ( ♯ ‘ 𝐷 ) ) )
51 50 imp ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 ) → 2 ≤ ( ♯ ‘ 𝐷 ) )