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 
|- ( ( V e. W /\ 1 < ( # ` V ) /\ 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. b e. V A =/= b ) )
12 10 11 sylbi 
 |-  ( 0 <_ 1 -> ( 1 < 0 -> E. b e. V A =/= b ) )
13 7 12 ax-mp 
 |-  ( 1 < 0 -> E. b e. V A =/= b )
14 6 13 syl6com 
 |-  ( 1 < ( # ` V ) -> ( 0 = ( # ` V ) -> E. b e. V A =/= b ) )
15 14 3ad2ant2 
 |-  ( ( V e. W /\ 1 < ( # ` V ) /\ A e. V ) -> ( 0 = ( # ` V ) -> E. b e. V A =/= b ) )
16 3 15 syl5com 
 |-  ( (/) = V -> ( ( V e. W /\ 1 < ( # ` V ) /\ A e. V ) -> E. b e. V A =/= b ) )
17 df-ne 
 |-  ( (/) =/= V <-> -. (/) = V )
18 necom 
 |-  ( (/) =/= V <-> V =/= (/) )
19 17 18 bitr3i 
 |-  ( -. (/) = V <-> V =/= (/) )
20 ralnex 
 |-  ( A. b e. V -. A =/= b <-> -. E. b e. V A =/= b )
21 nne 
 |-  ( -. A =/= b <-> A = b )
22 eqcom 
 |-  ( A = b <-> b = A )
23 21 22 bitri 
 |-  ( -. A =/= b <-> b = A )
24 23 ralbii 
 |-  ( A. b e. V -. A =/= b <-> A. b e. V b = A )
25 20 24 bitr3i 
 |-  ( -. E. b e. V A =/= b <-> A. b e. V b = A )
26 eqsn 
 |-  ( V =/= (/) -> ( V = { A } <-> A. b e. V b = A ) )
27 26 bicomd 
 |-  ( V =/= (/) -> ( A. b e. V b = A <-> V = { A } ) )
28 27 adantl 
 |-  ( ( V e. W /\ V =/= (/) ) -> ( A. b e. V b = A <-> V = { A } ) )
29 28 adantr 
 |-  ( ( ( V e. W /\ V =/= (/) ) /\ A e. V ) -> ( A. b e. V b = A <-> V = { A } ) )
30 hashsnle1 
 |-  ( # ` { A } ) <_ 1
31 fveq2 
 |-  ( V = { A } -> ( # ` V ) = ( # ` { A } ) )
32 31 breq1d 
 |-  ( V = { A } -> ( ( # ` V ) <_ 1 <-> ( # ` { A } ) <_ 1 ) )
33 32 adantl 
 |-  ( ( ( ( V e. W /\ V =/= (/) ) /\ A e. V ) /\ V = { A } ) -> ( ( # ` V ) <_ 1 <-> ( # ` { A } ) <_ 1 ) )
34 30 33 mpbiri 
 |-  ( ( ( ( V e. W /\ V =/= (/) ) /\ A e. V ) /\ V = { A } ) -> ( # ` V ) <_ 1 )
35 34 ex 
 |-  ( ( ( V e. W /\ V =/= (/) ) /\ A e. V ) -> ( V = { A } -> ( # ` V ) <_ 1 ) )
36 29 35 sylbid 
 |-  ( ( ( V e. W /\ V =/= (/) ) /\ A e. V ) -> ( A. b e. V b = A -> ( # ` V ) <_ 1 ) )
37 hashxrcl 
 |-  ( V e. W -> ( # ` V ) e. RR* )
38 37 adantr 
 |-  ( ( V e. W /\ V =/= (/) ) -> ( # ` V ) e. RR* )
39 38 adantr 
 |-  ( ( ( V e. W /\ V =/= (/) ) /\ A e. V ) -> ( # ` V ) e. RR* )
40 1xr 
 |-  1 e. RR*
41 xrlenlt 
 |-  ( ( ( # ` V ) e. RR* /\ 1 e. RR* ) -> ( ( # ` V ) <_ 1 <-> -. 1 < ( # ` V ) ) )
42 39 40 41 sylancl 
 |-  ( ( ( V e. W /\ V =/= (/) ) /\ A e. V ) -> ( ( # ` V ) <_ 1 <-> -. 1 < ( # ` V ) ) )
43 36 42 sylibd 
 |-  ( ( ( V e. W /\ V =/= (/) ) /\ A e. V ) -> ( A. b e. V b = A -> -. 1 < ( # ` V ) ) )
44 25 43 biimtrid 
 |-  ( ( ( V e. W /\ V =/= (/) ) /\ A e. V ) -> ( -. E. b e. V A =/= b -> -. 1 < ( # ` V ) ) )
45 44 con4d 
 |-  ( ( ( V e. W /\ V =/= (/) ) /\ A e. V ) -> ( 1 < ( # ` V ) -> E. b e. V A =/= b ) )
46 45 exp31 
 |-  ( V e. W -> ( V =/= (/) -> ( A e. V -> ( 1 < ( # ` V ) -> E. b e. V A =/= b ) ) ) )
47 46 com24 
 |-  ( V e. W -> ( 1 < ( # ` V ) -> ( A e. V -> ( V =/= (/) -> E. b e. V A =/= b ) ) ) )
48 47 3imp 
 |-  ( ( V e. W /\ 1 < ( # ` V ) /\ A e. V ) -> ( V =/= (/) -> E. b e. V A =/= b ) )
49 48 com12 
 |-  ( V =/= (/) -> ( ( V e. W /\ 1 < ( # ` V ) /\ A e. V ) -> E. b e. V A =/= b ) )
50 19 49 sylbi 
 |-  ( -. (/) = V -> ( ( V e. W /\ 1 < ( # ` V ) /\ A e. V ) -> E. b e. V A =/= b ) )
51 16 50 pm2.61i 
 |-  ( ( V e. W /\ 1 < ( # ` V ) /\ A e. V ) -> E. b e. V A =/= b )