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 ( ( 𝑉𝑊 ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ∃ 𝑎𝑉𝑏𝑉 𝑎𝑏 )

Proof

Step Hyp Ref Expression
1 hash0 ( ♯ ‘ ∅ ) = 0
2 fveq2 ( ∅ = 𝑉 → ( ♯ ‘ ∅ ) = ( ♯ ‘ 𝑉 ) )
3 1 2 eqtr3id ( ∅ = 𝑉 → 0 = ( ♯ ‘ 𝑉 ) )
4 breq2 ( ( ♯ ‘ 𝑉 ) = 0 → ( 1 < ( ♯ ‘ 𝑉 ) ↔ 1 < 0 ) )
5 4 biimpd ( ( ♯ ‘ 𝑉 ) = 0 → ( 1 < ( ♯ ‘ 𝑉 ) → 1 < 0 ) )
6 5 eqcoms ( 0 = ( ♯ ‘ 𝑉 ) → ( 1 < ( ♯ ‘ 𝑉 ) → 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 → ∃ 𝑎𝑉𝑏𝑉 𝑎𝑏 ) )
12 10 11 sylbi ( 0 ≤ 1 → ( 1 < 0 → ∃ 𝑎𝑉𝑏𝑉 𝑎𝑏 ) )
13 7 12 ax-mp ( 1 < 0 → ∃ 𝑎𝑉𝑏𝑉 𝑎𝑏 )
14 6 13 syl6com ( 1 < ( ♯ ‘ 𝑉 ) → ( 0 = ( ♯ ‘ 𝑉 ) → ∃ 𝑎𝑉𝑏𝑉 𝑎𝑏 ) )
15 14 adantl ( ( 𝑉𝑊 ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( 0 = ( ♯ ‘ 𝑉 ) → ∃ 𝑎𝑉𝑏𝑉 𝑎𝑏 ) )
16 15 com12 ( 0 = ( ♯ ‘ 𝑉 ) → ( ( 𝑉𝑊 ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ∃ 𝑎𝑉𝑏𝑉 𝑎𝑏 ) )
17 3 16 syl ( ∅ = 𝑉 → ( ( 𝑉𝑊 ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ∃ 𝑎𝑉𝑏𝑉 𝑎𝑏 ) )
18 df-ne ( ∅ ≠ 𝑉 ↔ ¬ ∅ = 𝑉 )
19 necom ( ∅ ≠ 𝑉𝑉 ≠ ∅ )
20 18 19 bitr3i ( ¬ ∅ = 𝑉𝑉 ≠ ∅ )
21 ralnex ( ∀ 𝑎𝑉 ¬ ∃ 𝑏𝑉 𝑎𝑏 ↔ ¬ ∃ 𝑎𝑉𝑏𝑉 𝑎𝑏 )
22 ralnex ( ∀ 𝑏𝑉 ¬ 𝑎𝑏 ↔ ¬ ∃ 𝑏𝑉 𝑎𝑏 )
23 nne ( ¬ 𝑎𝑏𝑎 = 𝑏 )
24 equcom ( 𝑎 = 𝑏𝑏 = 𝑎 )
25 23 24 bitri ( ¬ 𝑎𝑏𝑏 = 𝑎 )
26 25 ralbii ( ∀ 𝑏𝑉 ¬ 𝑎𝑏 ↔ ∀ 𝑏𝑉 𝑏 = 𝑎 )
27 22 26 bitr3i ( ¬ ∃ 𝑏𝑉 𝑎𝑏 ↔ ∀ 𝑏𝑉 𝑏 = 𝑎 )
28 27 ralbii ( ∀ 𝑎𝑉 ¬ ∃ 𝑏𝑉 𝑎𝑏 ↔ ∀ 𝑎𝑉𝑏𝑉 𝑏 = 𝑎 )
29 21 28 bitr3i ( ¬ ∃ 𝑎𝑉𝑏𝑉 𝑎𝑏 ↔ ∀ 𝑎𝑉𝑏𝑉 𝑏 = 𝑎 )
30 eqsn ( 𝑉 ≠ ∅ → ( 𝑉 = { 𝑎 } ↔ ∀ 𝑏𝑉 𝑏 = 𝑎 ) )
31 30 adantl ( ( 𝑉𝑊𝑉 ≠ ∅ ) → ( 𝑉 = { 𝑎 } ↔ ∀ 𝑏𝑉 𝑏 = 𝑎 ) )
32 31 bicomd ( ( 𝑉𝑊𝑉 ≠ ∅ ) → ( ∀ 𝑏𝑉 𝑏 = 𝑎𝑉 = { 𝑎 } ) )
33 32 ralbidv ( ( 𝑉𝑊𝑉 ≠ ∅ ) → ( ∀ 𝑎𝑉𝑏𝑉 𝑏 = 𝑎 ↔ ∀ 𝑎𝑉 𝑉 = { 𝑎 } ) )
34 fveq2 ( 𝑉 = { 𝑎 } → ( ♯ ‘ 𝑉 ) = ( ♯ ‘ { 𝑎 } ) )
35 hashsnle1 ( ♯ ‘ { 𝑎 } ) ≤ 1
36 34 35 eqbrtrdi ( 𝑉 = { 𝑎 } → ( ♯ ‘ 𝑉 ) ≤ 1 )
37 36 a1i ( ( 𝑉𝑊𝑎𝑉 ) → ( 𝑉 = { 𝑎 } → ( ♯ ‘ 𝑉 ) ≤ 1 ) )
38 37 reximdva0 ( ( 𝑉𝑊𝑉 ≠ ∅ ) → ∃ 𝑎𝑉 ( 𝑉 = { 𝑎 } → ( ♯ ‘ 𝑉 ) ≤ 1 ) )
39 r19.36v ( ∃ 𝑎𝑉 ( 𝑉 = { 𝑎 } → ( ♯ ‘ 𝑉 ) ≤ 1 ) → ( ∀ 𝑎𝑉 𝑉 = { 𝑎 } → ( ♯ ‘ 𝑉 ) ≤ 1 ) )
40 38 39 syl ( ( 𝑉𝑊𝑉 ≠ ∅ ) → ( ∀ 𝑎𝑉 𝑉 = { 𝑎 } → ( ♯ ‘ 𝑉 ) ≤ 1 ) )
41 33 40 sylbid ( ( 𝑉𝑊𝑉 ≠ ∅ ) → ( ∀ 𝑎𝑉𝑏𝑉 𝑏 = 𝑎 → ( ♯ ‘ 𝑉 ) ≤ 1 ) )
42 hashxrcl ( 𝑉𝑊 → ( ♯ ‘ 𝑉 ) ∈ ℝ* )
43 42 adantr ( ( 𝑉𝑊𝑉 ≠ ∅ ) → ( ♯ ‘ 𝑉 ) ∈ ℝ* )
44 1xr 1 ∈ ℝ*
45 xrlenlt ( ( ( ♯ ‘ 𝑉 ) ∈ ℝ* ∧ 1 ∈ ℝ* ) → ( ( ♯ ‘ 𝑉 ) ≤ 1 ↔ ¬ 1 < ( ♯ ‘ 𝑉 ) ) )
46 43 44 45 sylancl ( ( 𝑉𝑊𝑉 ≠ ∅ ) → ( ( ♯ ‘ 𝑉 ) ≤ 1 ↔ ¬ 1 < ( ♯ ‘ 𝑉 ) ) )
47 41 46 sylibd ( ( 𝑉𝑊𝑉 ≠ ∅ ) → ( ∀ 𝑎𝑉𝑏𝑉 𝑏 = 𝑎 → ¬ 1 < ( ♯ ‘ 𝑉 ) ) )
48 29 47 syl5bi ( ( 𝑉𝑊𝑉 ≠ ∅ ) → ( ¬ ∃ 𝑎𝑉𝑏𝑉 𝑎𝑏 → ¬ 1 < ( ♯ ‘ 𝑉 ) ) )
49 48 con4d ( ( 𝑉𝑊𝑉 ≠ ∅ ) → ( 1 < ( ♯ ‘ 𝑉 ) → ∃ 𝑎𝑉𝑏𝑉 𝑎𝑏 ) )
50 49 impancom ( ( 𝑉𝑊 ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( 𝑉 ≠ ∅ → ∃ 𝑎𝑉𝑏𝑉 𝑎𝑏 ) )
51 50 com12 ( 𝑉 ≠ ∅ → ( ( 𝑉𝑊 ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ∃ 𝑎𝑉𝑏𝑉 𝑎𝑏 ) )
52 20 51 sylbi ( ¬ ∅ = 𝑉 → ( ( 𝑉𝑊 ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ∃ 𝑎𝑉𝑏𝑉 𝑎𝑏 ) )
53 17 52 pm2.61i ( ( 𝑉𝑊 ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ∃ 𝑎𝑉𝑏𝑉 𝑎𝑏 )