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∈Va≠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∈Va≠b
12 10 11 sylbi ⊢0≤1→1<0→∃a∈V∃b∈Va≠b
13 7 12 ax-mp ⊢1<0→∃a∈V∃b∈Va≠b
14 6 13 syl6com ⊢1<V→0=V→∃a∈V∃b∈Va≠b
15 14 adantl ⊢V∈W∧1<V→0=V→∃a∈V∃b∈Va≠b
16 15 com12 ⊢0=V→V∈W∧1<V→∃a∈V∃b∈Va≠b
17 3 16 syl ⊢∅=V→V∈W∧1<V→∃a∈V∃b∈Va≠b
18 df-ne ⊢∅≠V↔¬∅=V
19 necom ⊢∅≠V↔V≠∅
20 18 19 bitr3i ⊢¬∅=V↔V≠∅
21 ralnex ⊢∀a∈V¬∃b∈Va≠b↔¬∃a∈V∃b∈Va≠b
22 ralnex ⊢∀b∈V¬a≠b↔¬∃b∈Va≠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∈Vb=a
27 22 26 bitr3i ⊢¬∃b∈Va≠b↔∀b∈Vb=a
28 27 ralbii ⊢∀a∈V¬∃b∈Va≠b↔∀a∈V∀b∈Vb=a
29 21 28 bitr3i ⊢¬∃a∈V∃b∈Va≠b↔∀a∈V∀b∈Vb=a
30 eqsn ⊢V≠∅→V=a↔∀b∈Vb=a
31 30 adantl ⊢V∈W∧V≠∅→V=a↔∀b∈Vb=a
32 31 bicomd ⊢V∈W∧V≠∅→∀b∈Vb=a↔V=a
33 32 ralbidv ⊢V∈W∧V≠∅→∀a∈V∀b∈Vb=a↔∀a∈VV=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∈VV=a→V≤1
39 r19.36v ⊢∃a∈VV=a→V≤1→∀a∈VV=a→V≤1
40 38 39 syl ⊢V∈W∧V≠∅→∀a∈VV=a→V≤1
41 33 40 sylbid ⊢V∈W∧V≠∅→∀a∈V∀b∈Vb=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∈Vb=a→¬1<V
48 29 47 biimtrid ⊢V∈W∧V≠∅→¬∃a∈V∃b∈Va≠b→¬1<V
49 48 con4d ⊢V∈W∧V≠∅→1<V→∃a∈V∃b∈Va≠b
50 49 impancom ⊢V∈W∧1<V→V≠∅→∃a∈V∃b∈Va≠b
51 50 com12 ⊢V≠∅→V∈W∧1<V→∃a∈V∃b∈Va≠b
52 20 51 sylbi ⊢¬∅=V→V∈W∧1<V→∃a∈V∃b∈Va≠b
53 17 52 pm2.61i ⊢V∈W∧1<V→∃a∈V∃b∈Va≠b