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 e. W /\ 1 < ( # ` V ) ) -> E. a e. V E. b e. 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 e. RR
9 1re
 |-  1 e. RR
10 8 9 lenlti
 |-  ( 0 <_ 1 <-> -. 1 < 0 )
11 pm2.21
 |-  ( -. 1 < 0 -> ( 1 < 0 -> E. a e. V E. b e. V a =/= b ) )
12 10 11 sylbi
 |-  ( 0 <_ 1 -> ( 1 < 0 -> E. a e. V E. b e. V a =/= b ) )
13 7 12 ax-mp
 |-  ( 1 < 0 -> E. a e. V E. b e. V a =/= b )
14 6 13 syl6com
 |-  ( 1 < ( # ` V ) -> ( 0 = ( # ` V ) -> E. a e. V E. b e. V a =/= b ) )
15 14 adantl
 |-  ( ( V e. W /\ 1 < ( # ` V ) ) -> ( 0 = ( # ` V ) -> E. a e. V E. b e. V a =/= b ) )
16 15 com12
 |-  ( 0 = ( # ` V ) -> ( ( V e. W /\ 1 < ( # ` V ) ) -> E. a e. V E. b e. V a =/= b ) )
17 3 16 syl
 |-  ( (/) = V -> ( ( V e. W /\ 1 < ( # ` V ) ) -> E. a e. V E. b e. V a =/= b ) )
18 df-ne
 |-  ( (/) =/= V <-> -. (/) = V )
19 necom
 |-  ( (/) =/= V <-> V =/= (/) )
20 18 19 bitr3i
 |-  ( -. (/) = V <-> V =/= (/) )
21 ralnex
 |-  ( A. a e. V -. E. b e. V a =/= b <-> -. E. a e. V E. b e. V a =/= b )
22 ralnex
 |-  ( A. b e. V -. a =/= b <-> -. E. b e. 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
 |-  ( A. b e. V -. a =/= b <-> A. b e. V b = a )
27 22 26 bitr3i
 |-  ( -. E. b e. V a =/= b <-> A. b e. V b = a )
28 27 ralbii
 |-  ( A. a e. V -. E. b e. V a =/= b <-> A. a e. V A. b e. V b = a )
29 21 28 bitr3i
 |-  ( -. E. a e. V E. b e. V a =/= b <-> A. a e. V A. b e. V b = a )
30 eqsn
 |-  ( V =/= (/) -> ( V = { a } <-> A. b e. V b = a ) )
31 30 adantl
 |-  ( ( V e. W /\ V =/= (/) ) -> ( V = { a } <-> A. b e. V b = a ) )
32 31 bicomd
 |-  ( ( V e. W /\ V =/= (/) ) -> ( A. b e. V b = a <-> V = { a } ) )
33 32 ralbidv
 |-  ( ( V e. W /\ V =/= (/) ) -> ( A. a e. V A. b e. V b = a <-> A. a e. 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 e. W /\ a e. V ) -> ( V = { a } -> ( # ` V ) <_ 1 ) )
38 37 reximdva0
 |-  ( ( V e. W /\ V =/= (/) ) -> E. a e. V ( V = { a } -> ( # ` V ) <_ 1 ) )
39 r19.36v
 |-  ( E. a e. V ( V = { a } -> ( # ` V ) <_ 1 ) -> ( A. a e. V V = { a } -> ( # ` V ) <_ 1 ) )
40 38 39 syl
 |-  ( ( V e. W /\ V =/= (/) ) -> ( A. a e. V V = { a } -> ( # ` V ) <_ 1 ) )
41 33 40 sylbid
 |-  ( ( V e. W /\ V =/= (/) ) -> ( A. a e. V A. b e. V b = a -> ( # ` V ) <_ 1 ) )
42 hashxrcl
 |-  ( V e. W -> ( # ` V ) e. RR* )
43 42 adantr
 |-  ( ( V e. W /\ V =/= (/) ) -> ( # ` V ) e. RR* )
44 1xr
 |-  1 e. RR*
45 xrlenlt
 |-  ( ( ( # ` V ) e. RR* /\ 1 e. RR* ) -> ( ( # ` V ) <_ 1 <-> -. 1 < ( # ` V ) ) )
46 43 44 45 sylancl
 |-  ( ( V e. W /\ V =/= (/) ) -> ( ( # ` V ) <_ 1 <-> -. 1 < ( # ` V ) ) )
47 41 46 sylibd
 |-  ( ( V e. W /\ V =/= (/) ) -> ( A. a e. V A. b e. V b = a -> -. 1 < ( # ` V ) ) )
48 29 47 syl5bi
 |-  ( ( V e. W /\ V =/= (/) ) -> ( -. E. a e. V E. b e. V a =/= b -> -. 1 < ( # ` V ) ) )
49 48 con4d
 |-  ( ( V e. W /\ V =/= (/) ) -> ( 1 < ( # ` V ) -> E. a e. V E. b e. V a =/= b ) )
50 49 impancom
 |-  ( ( V e. W /\ 1 < ( # ` V ) ) -> ( V =/= (/) -> E. a e. V E. b e. V a =/= b ) )
51 50 com12
 |-  ( V =/= (/) -> ( ( V e. W /\ 1 < ( # ` V ) ) -> E. a e. V E. b e. V a =/= b ) )
52 20 51 sylbi
 |-  ( -. (/) = V -> ( ( V e. W /\ 1 < ( # ` V ) ) -> E. a e. V E. b e. V a =/= b ) )
53 17 52 pm2.61i
 |-  ( ( V e. W /\ 1 < ( # ` V ) ) -> E. a e. V E. b e. V a =/= b )