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 ⊢ D ∈ V ∧ ∃ x ∈ D ∃ y ∈ D x ≠ y → 2 ≤ D

Proof

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