Metamath Proof Explorer

Theorem hashgt12el2

Description: In a set with more than one element are two different elements. (Contributed by Alexander van der Vekens, 15-Nov-2017)

Ref Expression
Assertion hashgt12el2 ⊢ V ∈ W ∧ 1 < V ∧ A ∈ V → ∃ b ∈ V A ≠ b

Proof

Step Hyp Ref Expression
1 hash0 ⊢ ∅ = 0
2 fveq2 ⊢ ∅ = V → ∅ = V
3 1 2 eqtr3id ⊢ ∅ = V → 0 = V
4 breq2 ⊢ V = 0 → 1 < V ↔ 1 < 0
5 4 biimpd ⊢ V = 0 → 1 < V → 1 < 0
6 5 eqcoms ⊢ 0 = V → 1 < V → 1 < 0
7 0le1 ⊢ 0 ≤ 1
8 0re ⊢ 0 ∈ ℝ
9 1re ⊢ 1 ∈ ℝ
10 8 9 lenlti ⊢ 0 ≤ 1 ↔ ¬ 1 < 0
11 pm2.21 ⊢ ¬ 1 < 0 → 1 < 0 → ∃ b ∈ V A ≠ b
12 10 11 sylbi ⊢ 0 ≤ 1 → 1 < 0 → ∃ b ∈ V A ≠ b
13 7 12 ax-mp ⊢ 1 < 0 → ∃ b ∈ V A ≠ b
14 6 13 syl6com ⊢ 1 < V → 0 = V → ∃ b ∈ V A ≠ b
15 14 3ad2ant2 ⊢ V ∈ W ∧ 1 < V ∧ A ∈ V → 0 = V → ∃ b ∈ V A ≠ b
16 3 15 syl5com ⊢ ∅ = V → V ∈ W ∧ 1 < V ∧ A ∈ V → ∃ b ∈ V A ≠ b
17 df-ne ⊢ ∅ ≠ V ↔ ¬ ∅ = V
18 necom ⊢ ∅ ≠ V ↔ V ≠ ∅
19 17 18 bitr3i ⊢ ¬ ∅ = V ↔ V ≠ ∅
20 ralnex ⊢ ∀ b ∈ V ¬ A ≠ b ↔ ¬ ∃ b ∈ V A ≠ b
21 nne ⊢ ¬ A ≠ b ↔ A = b
22 eqcom ⊢ A = b ↔ b = A
23 21 22 bitri ⊢ ¬ A ≠ b ↔ b = A
24 23 ralbii ⊢ ∀ b ∈ V ¬ A ≠ b ↔ ∀ b ∈ V b = A
25 20 24 bitr3i ⊢ ¬ ∃ b ∈ V A ≠ b ↔ ∀ b ∈ V b = A
26 eqsn ⊢ V ≠ ∅ → V = A ↔ ∀ b ∈ V b = A
27 26 bicomd ⊢ V ≠ ∅ → ∀ b ∈ V b = A ↔ V = A
28 27 adantl ⊢ V ∈ W ∧ V ≠ ∅ → ∀ b ∈ V b = A ↔ V = A
29 28 adantr ⊢ V ∈ W ∧ V ≠ ∅ ∧ A ∈ V → ∀ b ∈ V b = A ↔ V = A
30 hashsnle1 ⊢ A ≤ 1
31 fveq2 ⊢ V = A → V = A
32 31 breq1d ⊢ V = A → V ≤ 1 ↔ A ≤ 1
33 32 adantl ⊢ V ∈ W ∧ V ≠ ∅ ∧ A ∈ V ∧ V = A → V ≤ 1 ↔ A ≤ 1
34 30 33 mpbiri ⊢ V ∈ W ∧ V ≠ ∅ ∧ A ∈ V ∧ V = A → V ≤ 1
35 34 ex ⊢ V ∈ W ∧ V ≠ ∅ ∧ A ∈ V → V = A → V ≤ 1
36 29 35 sylbid ⊢ V ∈ W ∧ V ≠ ∅ ∧ A ∈ V → ∀ b ∈ V b = A → V ≤ 1
37 hashxrcl ⊢ V ∈ W → V ∈ ℝ *
38 37 adantr ⊢ V ∈ W ∧ V ≠ ∅ → V ∈ ℝ *
39 38 adantr ⊢ V ∈ W ∧ V ≠ ∅ ∧ A ∈ V → V ∈ ℝ *
40 1xr ⊢ 1 ∈ ℝ *
41 xrlenlt ⊢ V ∈ ℝ * ∧ 1 ∈ ℝ * → V ≤ 1 ↔ ¬ 1 < V
42 39 40 41 sylancl ⊢ V ∈ W ∧ V ≠ ∅ ∧ A ∈ V → V ≤ 1 ↔ ¬ 1 < V
43 36 42 sylibd ⊢ V ∈ W ∧ V ≠ ∅ ∧ A ∈ V → ∀ b ∈ V b = A → ¬ 1 < V
44 25 43 biimtrid ⊢ V ∈ W ∧ V ≠ ∅ ∧ A ∈ V → ¬ ∃ b ∈ V A ≠ b → ¬ 1 < V
45 44 con4d ⊢ V ∈ W ∧ V ≠ ∅ ∧ A ∈ V → 1 < V → ∃ b ∈ V A ≠ b
46 45 exp31 ⊢ V ∈ W → V ≠ ∅ → A ∈ V → 1 < V → ∃ b ∈ V A ≠ b
47 46 com24 ⊢ V ∈ W → 1 < V → A ∈ V → V ≠ ∅ → ∃ b ∈ V A ≠ b
48 47 3imp ⊢ V ∈ W ∧ 1 < V ∧ A ∈ V → V ≠ ∅ → ∃ b ∈ V A ≠ b
49 48 com12 ⊢ V ≠ ∅ → V ∈ W ∧ 1 < V ∧ A ∈ V → ∃ b ∈ V A ≠ b
50 19 49 sylbi ⊢ ¬ ∅ = V → V ∈ W ∧ 1 < V ∧ A ∈ V → ∃ b ∈ V A ≠ b
51 16 50 pm2.61i ⊢ V ∈ W ∧ 1 < V ∧ A ∈ V → ∃ b ∈ V A ≠ b