Metamath Proof Explorer

Theorem hashge2el2dif

Description: A set with size at least 2 has at least 2 different elements. (Contributed by AV, 18-Mar-2019)

Ref Expression
Assertion hashge2el2dif ⊢ D ∈ V ∧ 2 ≤ D → ∃ x ∈ D ∃ y ∈ D x ≠ y

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ D = x → D = x
2 hashsng ⊢ x ∈ D → x = 1
3 1 2 sylan9eqr ⊢ x ∈ D ∧ D = x → D = 1
4 3 ralimiaa ⊢ ∀ x ∈ D D = x → ∀ x ∈ D D = 1
5 0re ⊢ 0 ∈ ℝ
6 1re ⊢ 1 ∈ ℝ
7 5 6 readdcli ⊢ 0 + 1 ∈ ℝ
8 7 a1i ⊢ D ∈ Fin ∧ D ∈ V ∧ 2 ≤ D → 0 + 1 ∈ ℝ
9 2re ⊢ 2 ∈ ℝ
10 9 a1i ⊢ D ∈ Fin ∧ D ∈ V ∧ 2 ≤ D → 2 ∈ ℝ
11 hashcl ⊢ D ∈ Fin → D ∈ ℕ 0
12 11 nn0red ⊢ D ∈ Fin → D ∈ ℝ
13 12 adantr ⊢ D ∈ Fin ∧ D ∈ V ∧ 2 ≤ D → D ∈ ℝ
14 8 10 13 3jca ⊢ D ∈ Fin ∧ D ∈ V ∧ 2 ≤ D → 0 + 1 ∈ ℝ ∧ 2 ∈ ℝ ∧ D ∈ ℝ
15 0p1e1 ⊢ 0 + 1 = 1
16 1lt2 ⊢ 1 < 2
17 15 16 eqbrtri ⊢ 0 + 1 < 2
18 17 jctl ⊢ 2 ≤ D → 0 + 1 < 2 ∧ 2 ≤ D
19 18 adantl ⊢ D ∈ V ∧ 2 ≤ D → 0 + 1 < 2 ∧ 2 ≤ D
20 19 adantl ⊢ D ∈ Fin ∧ D ∈ V ∧ 2 ≤ D → 0 + 1 < 2 ∧ 2 ≤ D
21 ltleletr ⊢ 0 + 1 ∈ ℝ ∧ 2 ∈ ℝ ∧ D ∈ ℝ → 0 + 1 < 2 ∧ 2 ≤ D → 0 + 1 ≤ D
22 14 20 21 sylc ⊢ D ∈ Fin ∧ D ∈ V ∧ 2 ≤ D → 0 + 1 ≤ D
23 11 nn0zd ⊢ D ∈ Fin → D ∈ ℤ
24 0z ⊢ 0 ∈ ℤ
25 23 24 jctil ⊢ D ∈ Fin → 0 ∈ ℤ ∧ D ∈ ℤ
26 25 adantr ⊢ D ∈ Fin ∧ D ∈ V ∧ 2 ≤ D → 0 ∈ ℤ ∧ D ∈ ℤ
27 zltp1le ⊢ 0 ∈ ℤ ∧ D ∈ ℤ → 0 < D ↔ 0 + 1 ≤ D
28 26 27 syl ⊢ D ∈ Fin ∧ D ∈ V ∧ 2 ≤ D → 0 < D ↔ 0 + 1 ≤ D
29 22 28 mpbird ⊢ D ∈ Fin ∧ D ∈ V ∧ 2 ≤ D → 0 < D
30 0ltpnf ⊢ 0 < +∞
31 simpl ⊢ D ∈ V ∧ 2 ≤ D → D ∈ V
32 31 anim2i ⊢ ¬ D ∈ Fin ∧ D ∈ V ∧ 2 ≤ D → ¬ D ∈ Fin ∧ D ∈ V
33 32 ancomd ⊢ ¬ D ∈ Fin ∧ D ∈ V ∧ 2 ≤ D → D ∈ V ∧ ¬ D ∈ Fin
34 hashinf ⊢ D ∈ V ∧ ¬ D ∈ Fin → D = +∞
35 33 34 syl ⊢ ¬ D ∈ Fin ∧ D ∈ V ∧ 2 ≤ D → D = +∞
36 30 35 breqtrrid ⊢ ¬ D ∈ Fin ∧ D ∈ V ∧ 2 ≤ D → 0 < D
37 29 36 pm2.61ian ⊢ D ∈ V ∧ 2 ≤ D → 0 < D
38 hashgt0n0 ⊢ D ∈ V ∧ 0 < D → D ≠ ∅
39 37 38 syldan ⊢ D ∈ V ∧ 2 ≤ D → D ≠ ∅
40 rspn0 ⊢ D ≠ ∅ → ∀ x ∈ D D = 1 → D = 1
41 39 40 syl ⊢ D ∈ V ∧ 2 ≤ D → ∀ x ∈ D D = 1 → D = 1
42 breq2 ⊢ D = 1 → 2 ≤ D ↔ 2 ≤ 1
43 6 9 ltnlei ⊢ 1 < 2 ↔ ¬ 2 ≤ 1
44 pm2.21 ⊢ ¬ 2 ≤ 1 → 2 ≤ 1 → ¬ ∀ x ∈ D D = x
45 43 44 sylbi ⊢ 1 < 2 → 2 ≤ 1 → ¬ ∀ x ∈ D D = x
46 16 45 ax-mp ⊢ 2 ≤ 1 → ¬ ∀ x ∈ D D = x
47 42 46 syl6bi ⊢ D = 1 → 2 ≤ D → ¬ ∀ x ∈ D D = x
48 47 com12 ⊢ 2 ≤ D → D = 1 → ¬ ∀ x ∈ D D = x
49 48 adantl ⊢ D ∈ V ∧ 2 ≤ D → D = 1 → ¬ ∀ x ∈ D D = x
50 41 49 syldc ⊢ ∀ x ∈ D D = 1 → D ∈ V ∧ 2 ≤ D → ¬ ∀ x ∈ D D = x
51 4 50 syl ⊢ ∀ x ∈ D D = x → D ∈ V ∧ 2 ≤ D → ¬ ∀ x ∈ D D = x
52 ax-1 ⊢ ¬ ∀ x ∈ D D = x → D ∈ V ∧ 2 ≤ D → ¬ ∀ x ∈ D D = x
53 51 52 pm2.61i ⊢ D ∈ V ∧ 2 ≤ D → ¬ ∀ x ∈ D D = x
54 eqsn ⊢ D ≠ ∅ → D = x ↔ ∀ y ∈ D y = x
55 39 54 syl ⊢ D ∈ V ∧ 2 ≤ D → D = x ↔ ∀ y ∈ D y = x
56 equcom ⊢ y = x ↔ x = y
57 56 a1i ⊢ D ∈ V ∧ 2 ≤ D → y = x ↔ x = y
58 57 ralbidv ⊢ D ∈ V ∧ 2 ≤ D → ∀ y ∈ D y = x ↔ ∀ y ∈ D x = y
59 55 58 bitrd ⊢ D ∈ V ∧ 2 ≤ D → D = x ↔ ∀ y ∈ D x = y
60 59 ralbidv ⊢ D ∈ V ∧ 2 ≤ D → ∀ x ∈ D D = x ↔ ∀ x ∈ D ∀ y ∈ D x = y
61 53 60 mtbid ⊢ D ∈ V ∧ 2 ≤ D → ¬ ∀ x ∈ D ∀ y ∈ D x = y
62 df-ne ⊢ x ≠ y ↔ ¬ x = y
63 62 rexbii ⊢ ∃ y ∈ D x ≠ y ↔ ∃ y ∈ D ¬ x = y
64 rexnal ⊢ ∃ y ∈ D ¬ x = y ↔ ¬ ∀ y ∈ D x = y
65 63 64 bitri ⊢ ∃ y ∈ D x ≠ y ↔ ¬ ∀ y ∈ D x = y
66 65 rexbii ⊢ ∃ x ∈ D ∃ y ∈ D x ≠ y ↔ ∃ x ∈ D ¬ ∀ y ∈ D x = y
67 rexnal ⊢ ∃ x ∈ D ¬ ∀ y ∈ D x = y ↔ ¬ ∀ x ∈ D ∀ y ∈ D x = y
68 66 67 bitri ⊢ ∃ x ∈ D ∃ y ∈ D x ≠ y ↔ ¬ ∀ x ∈ D ∀ y ∈ D x = y
69 61 68 sylibr ⊢ D ∈ V ∧ 2 ≤ D → ∃ x ∈ D ∃ y ∈ D x ≠ y