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

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 ( ( 𝑉 ∈ 𝑊 ∧ 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 3ad2ant2 ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 1 < ( ♯ ‘ 𝑉 ) ∧ 𝐴 ∈ 𝑉 ) → ( 0 = ( ♯ ‘ 𝑉 ) → ∃ 𝑏 ∈ 𝑉 𝐴 ≠ 𝑏 ) )
16 3 15 syl5com ⊢ ( ∅ = 𝑉 → ( ( 𝑉 ∈ 𝑊 ∧ 1 < ( ♯ ‘ 𝑉 ) ∧ 𝐴 ∈ 𝑉 ) → ∃ 𝑏 ∈ 𝑉 𝐴 ≠ 𝑏 ) )
17 df-ne ⊢ ( ∅ ≠ 𝑉 ↔ ¬ ∅ = 𝑉 )
18 necom ⊢ ( ∅ ≠ 𝑉 ↔ 𝑉 ≠ ∅ )
19 17 18 bitr3i ⊢ ( ¬ ∅ = 𝑉 ↔ 𝑉 ≠ ∅ )
20 ralnex ⊢ ( ∀ 𝑏 ∈ 𝑉 ¬ 𝐴 ≠ 𝑏 ↔ ¬ ∃ 𝑏 ∈ 𝑉 𝐴 ≠ 𝑏 )
21 nne ⊢ ( ¬ 𝐴 ≠ 𝑏 ↔ 𝐴 = 𝑏 )
22 eqcom ⊢ ( 𝐴 = 𝑏 ↔ 𝑏 = 𝐴 )
23 21 22 bitri ⊢ ( ¬ 𝐴 ≠ 𝑏 ↔ 𝑏 = 𝐴 )
24 23 ralbii ⊢ ( ∀ 𝑏 ∈ 𝑉 ¬ 𝐴 ≠ 𝑏 ↔ ∀ 𝑏 ∈ 𝑉 𝑏 = 𝐴 )
25 20 24 bitr3i ⊢ ( ¬ ∃ 𝑏 ∈ 𝑉 𝐴 ≠ 𝑏 ↔ ∀ 𝑏 ∈ 𝑉 𝑏 = 𝐴 )
26 eqsn ⊢ ( 𝑉 ≠ ∅ → ( 𝑉 = { 𝐴 } ↔ ∀ 𝑏 ∈ 𝑉 𝑏 = 𝐴 ) )
27 26 bicomd ⊢ ( 𝑉 ≠ ∅ → ( ∀ 𝑏 ∈ 𝑉 𝑏 = 𝐴 ↔ 𝑉 = { 𝐴 } ) )
28 27 adantl ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) → ( ∀ 𝑏 ∈ 𝑉 𝑏 = 𝐴 ↔ 𝑉 = { 𝐴 } ) )
29 28 adantr ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) ∧ 𝐴 ∈ 𝑉 ) → ( ∀ 𝑏 ∈ 𝑉 𝑏 = 𝐴 ↔ 𝑉 = { 𝐴 } ) )
30 hashsnle1 ⊢ ( ♯ ‘ { 𝐴 } ) ≤ 1
31 fveq2 ⊢ ( 𝑉 = { 𝐴 } → ( ♯ ‘ 𝑉 ) = ( ♯ ‘ { 𝐴 } ) )
32 31 breq1d ⊢ ( 𝑉 = { 𝐴 } → ( ( ♯ ‘ 𝑉 ) ≤ 1 ↔ ( ♯ ‘ { 𝐴 } ) ≤ 1 ) )
33 32 adantl ⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑉 = { 𝐴 } ) → ( ( ♯ ‘ 𝑉 ) ≤ 1 ↔ ( ♯ ‘ { 𝐴 } ) ≤ 1 ) )
34 30 33 mpbiri ⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑉 = { 𝐴 } ) → ( ♯ ‘ 𝑉 ) ≤ 1 )
35 34 ex ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) ∧ 𝐴 ∈ 𝑉 ) → ( 𝑉 = { 𝐴 } → ( ♯ ‘ 𝑉 ) ≤ 1 ) )
36 29 35 sylbid ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) ∧ 𝐴 ∈ 𝑉 ) → ( ∀ 𝑏 ∈ 𝑉 𝑏 = 𝐴 → ( ♯ ‘ 𝑉 ) ≤ 1 ) )
37 hashxrcl ⊢ ( 𝑉 ∈ 𝑊 → ( ♯ ‘ 𝑉 ) ∈ ℝ* )
38 37 adantr ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) → ( ♯ ‘ 𝑉 ) ∈ ℝ* )
39 38 adantr ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) ∧ 𝐴 ∈ 𝑉 ) → ( ♯ ‘ 𝑉 ) ∈ ℝ* )
40 1xr ⊢ 1 ∈ ℝ*
41 xrlenlt ⊢ ( ( ( ♯ ‘ 𝑉 ) ∈ ℝ* ∧ 1 ∈ ℝ* ) → ( ( ♯ ‘ 𝑉 ) ≤ 1 ↔ ¬ 1 < ( ♯ ‘ 𝑉 ) ) )
42 39 40 41 sylancl ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) ∧ 𝐴 ∈ 𝑉 ) → ( ( ♯ ‘ 𝑉 ) ≤ 1 ↔ ¬ 1 < ( ♯ ‘ 𝑉 ) ) )
43 36 42 sylibd ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) ∧ 𝐴 ∈ 𝑉 ) → ( ∀ 𝑏 ∈ 𝑉 𝑏 = 𝐴 → ¬ 1 < ( ♯ ‘ 𝑉 ) ) )
44 25 43 biimtrid ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) ∧ 𝐴 ∈ 𝑉 ) → ( ¬ ∃ 𝑏 ∈ 𝑉 𝐴 ≠ 𝑏 → ¬ 1 < ( ♯ ‘ 𝑉 ) ) )
45 44 con4d ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) ∧ 𝐴 ∈ 𝑉 ) → ( 1 < ( ♯ ‘ 𝑉 ) → ∃ 𝑏 ∈ 𝑉 𝐴 ≠ 𝑏 ) )
46 45 exp31 ⊢ ( 𝑉 ∈ 𝑊 → ( 𝑉 ≠ ∅ → ( 𝐴 ∈ 𝑉 → ( 1 < ( ♯ ‘ 𝑉 ) → ∃ 𝑏 ∈ 𝑉 𝐴 ≠ 𝑏 ) ) ) )
47 46 com24 ⊢ ( 𝑉 ∈ 𝑊 → ( 1 < ( ♯ ‘ 𝑉 ) → ( 𝐴 ∈ 𝑉 → ( 𝑉 ≠ ∅ → ∃ 𝑏 ∈ 𝑉 𝐴 ≠ 𝑏 ) ) ) )
48 47 3imp ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 1 < ( ♯ ‘ 𝑉 ) ∧ 𝐴 ∈ 𝑉 ) → ( 𝑉 ≠ ∅ → ∃ 𝑏 ∈ 𝑉 𝐴 ≠ 𝑏 ) )
49 48 com12 ⊢ ( 𝑉 ≠ ∅ → ( ( 𝑉 ∈ 𝑊 ∧ 1 < ( ♯ ‘ 𝑉 ) ∧ 𝐴 ∈ 𝑉 ) → ∃ 𝑏 ∈ 𝑉 𝐴 ≠ 𝑏 ) )
50 19 49 sylbi ⊢ ( ¬ ∅ = 𝑉 → ( ( 𝑉 ∈ 𝑊 ∧ 1 < ( ♯ ‘ 𝑉 ) ∧ 𝐴 ∈ 𝑉 ) → ∃ 𝑏 ∈ 𝑉 𝐴 ≠ 𝑏 ) )
51 16 50 pm2.61i ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 1 < ( ♯ ‘ 𝑉 ) ∧ 𝐴 ∈ 𝑉 ) → ∃ 𝑏 ∈ 𝑉 𝐴 ≠ 𝑏 )