Metamath Proof Explorer

Theorem hashgt12el

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 hashgt12el ⊢ 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 → ∃ a ∈ V ∃ b ∈ V a ≠ b
12 10 11 sylbi ⊢ 0 ≤ 1 → 1 < 0 → ∃ a ∈ V ∃ b ∈ V a ≠ b
13 7 12 ax-mp ⊢ 1 < 0 → ∃ a ∈ V ∃ b ∈ V a ≠ b
14 6 13 syl6com ⊢ 1 < V → 0 = V → ∃ a ∈ V ∃ b ∈ V a ≠ b
15 14 adantl ⊢ V ∈ W ∧ 1 < V → 0 = V → ∃ a ∈ V ∃ b ∈ V a ≠ b
16 15 com12 ⊢ 0 = V → V ∈ W ∧ 1 < V → ∃ a ∈ V ∃ b ∈ V a ≠ b
17 3 16 syl ⊢ ∅ = V → V ∈ W ∧ 1 < V → ∃ a ∈ V ∃ b ∈ V a ≠ b
18 df-ne ⊢ ∅ ≠ V ↔ ¬ ∅ = V
19 necom ⊢ ∅ ≠ V ↔ V ≠ ∅
20 18 19 bitr3i ⊢ ¬ ∅ = V ↔ V ≠ ∅
21 ralnex ⊢ ∀ a ∈ V ¬ ∃ b ∈ V a ≠ b ↔ ¬ ∃ a ∈ V ∃ b ∈ V a ≠ b
22 ralnex ⊢ ∀ b ∈ V ¬ a ≠ b ↔ ¬ ∃ b ∈ V a ≠ b
23 nne ⊢ ¬ a ≠ b ↔ a = b
24 equcom ⊢ a = b ↔ b = a
25 23 24 bitri ⊢ ¬ a ≠ b ↔ b = a
26 25 ralbii ⊢ ∀ b ∈ V ¬ a ≠ b ↔ ∀ b ∈ V b = a
27 22 26 bitr3i ⊢ ¬ ∃ b ∈ V a ≠ b ↔ ∀ b ∈ V b = a
28 27 ralbii ⊢ ∀ a ∈ V ¬ ∃ b ∈ V a ≠ b ↔ ∀ a ∈ V ∀ b ∈ V b = a
29 21 28 bitr3i ⊢ ¬ ∃ a ∈ V ∃ b ∈ V a ≠ b ↔ ∀ a ∈ V ∀ b ∈ V b = a
30 eqsn ⊢ V ≠ ∅ → V = a ↔ ∀ b ∈ V b = a
31 30 adantl ⊢ V ∈ W ∧ V ≠ ∅ → V = a ↔ ∀ b ∈ V b = a
32 31 bicomd ⊢ V ∈ W ∧ V ≠ ∅ → ∀ b ∈ V b = a ↔ V = a
33 32 ralbidv ⊢ V ∈ W ∧ V ≠ ∅ → ∀ a ∈ V ∀ b ∈ V b = a ↔ ∀ a ∈ V V = a
34 fveq2 ⊢ V = a → V = a
35 hashsnle1 ⊢ a ≤ 1
36 34 35 eqbrtrdi ⊢ V = a → V ≤ 1
37 36 a1i ⊢ V ∈ W ∧ a ∈ V → V = a → V ≤ 1
38 37 reximdva0 ⊢ V ∈ W ∧ V ≠ ∅ → ∃ a ∈ V V = a → V ≤ 1
39 r19.36v ⊢ ∃ a ∈ V V = a → V ≤ 1 → ∀ a ∈ V V = a → V ≤ 1
40 38 39 syl ⊢ V ∈ W ∧ V ≠ ∅ → ∀ a ∈ V V = a → V ≤ 1
41 33 40 sylbid ⊢ V ∈ W ∧ V ≠ ∅ → ∀ a ∈ V ∀ b ∈ V b = a → V ≤ 1
42 hashxrcl ⊢ V ∈ W → V ∈ ℝ *
43 42 adantr ⊢ V ∈ W ∧ V ≠ ∅ → V ∈ ℝ *
44 1xr ⊢ 1 ∈ ℝ *
45 xrlenlt ⊢ V ∈ ℝ * ∧ 1 ∈ ℝ * → V ≤ 1 ↔ ¬ 1 < V
46 43 44 45 sylancl ⊢ V ∈ W ∧ V ≠ ∅ → V ≤ 1 ↔ ¬ 1 < V
47 41 46 sylibd ⊢ V ∈ W ∧ V ≠ ∅ → ∀ a ∈ V ∀ b ∈ V b = a → ¬ 1 < V
48 29 47 syl5bi ⊢ V ∈ W ∧ V ≠ ∅ → ¬ ∃ a ∈ V ∃ b ∈ V a ≠ b → ¬ 1 < V
49 48 con4d ⊢ V ∈ W ∧ V ≠ ∅ → 1 < V → ∃ a ∈ V ∃ b ∈ V a ≠ b
50 49 impancom ⊢ V ∈ W ∧ 1 < V → V ≠ ∅ → ∃ a ∈ V ∃ b ∈ V a ≠ b
51 50 com12 ⊢ V ≠ ∅ → V ∈ W ∧ 1 < V → ∃ a ∈ V ∃ b ∈ V a ≠ b
52 20 51 sylbi ⊢ ¬ ∅ = V → V ∈ W ∧ 1 < V → ∃ a ∈ V ∃ b ∈ V a ≠ b
53 17 52 pm2.61i ⊢ V ∈ W ∧ 1 < V → ∃ a ∈ V ∃ b ∈ V a ≠ b