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 )