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 ( ( 𝐷 ∈ 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝐷 ) ) → ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 𝑥 ≠ 𝑦 )

Proof

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