This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrid ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) → ( ¬ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑎 ≠ 𝑏 → ¬ 1 < ( ♯ ‘ 𝑉 ) ) )
49 48 con4d ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) → ( 1 < ( ♯ ‘ 𝑉 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑎 ≠ 𝑏 ) )
50 49 impancom ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( 𝑉 ≠ ∅ → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑎 ≠ 𝑏 ) )
51 50 com12 ⊢ ( 𝑉 ≠ ∅ → ( ( 𝑉 ∈ 𝑊 ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑎 ≠ 𝑏 ) )
52 20 51 sylbi ⊢ ( ¬ ∅ = 𝑉 → ( ( 𝑉 ∈ 𝑊 ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑎 ≠ 𝑏 ) )
53 17 52 pm2.61i ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑎 ≠ 𝑏 )