Metamath Proof Explorer

Theorem hashge2el2dif

Description: A set with size at least 2 has at least 2 different elements. (Contributed by AV, 18-Mar-2019)

Ref Expression
Assertion hashge2el2dif 
|- ( ( D e. V /\ 2 <_ ( # ` D ) ) -> E. x e. D E. y e. D x =/= y )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( D = { x } -> ( # ` D ) = ( # ` { x } ) )
2 hashsng 
 |-  ( x e. D -> ( # ` { x } ) = 1 )
3 1 2 sylan9eqr 
 |-  ( ( x e. D /\ D = { x } ) -> ( # ` D ) = 1 )
4 3 ralimiaa 
 |-  ( A. x e. D D = { x } -> A. x e. D ( # ` D ) = 1 )
5 0re 
 |-  0 e. RR
6 1re 
 |-  1 e. RR
7 5 6 readdcli 
 |-  ( 0 + 1 ) e. RR
8 7 a1i 
 |-  ( ( D e. Fin /\ ( D e. V /\ 2 <_ ( # ` D ) ) ) -> ( 0 + 1 ) e. RR )
9 2re 
 |-  2 e. RR
10 9 a1i 
 |-  ( ( D e. Fin /\ ( D e. V /\ 2 <_ ( # ` D ) ) ) -> 2 e. RR )
11 hashcl 
 |-  ( D e. Fin -> ( # ` D ) e. NN0 )
12 11 nn0red 
 |-  ( D e. Fin -> ( # ` D ) e. RR )
13 12 adantr 
 |-  ( ( D e. Fin /\ ( D e. V /\ 2 <_ ( # ` D ) ) ) -> ( # ` D ) e. RR )
14 8 10 13 3jca 
 |-  ( ( D e. Fin /\ ( D e. V /\ 2 <_ ( # ` D ) ) ) -> ( ( 0 + 1 ) e. RR /\ 2 e. RR /\ ( # ` D ) e. RR ) )
15 0p1e1 
 |-  ( 0 + 1 ) = 1
16 1lt2 
 |-  1 < 2
17 15 16 eqbrtri 
 |-  ( 0 + 1 ) < 2
18 17 jctl 
 |-  ( 2 <_ ( # ` D ) -> ( ( 0 + 1 ) < 2 /\ 2 <_ ( # ` D ) ) )
19 18 adantl 
 |-  ( ( D e. V /\ 2 <_ ( # ` D ) ) -> ( ( 0 + 1 ) < 2 /\ 2 <_ ( # ` D ) ) )
20 19 adantl 
 |-  ( ( D e. Fin /\ ( D e. V /\ 2 <_ ( # ` D ) ) ) -> ( ( 0 + 1 ) < 2 /\ 2 <_ ( # ` D ) ) )
21 ltleletr 
 |-  ( ( ( 0 + 1 ) e. RR /\ 2 e. RR /\ ( # ` D ) e. RR ) -> ( ( ( 0 + 1 ) < 2 /\ 2 <_ ( # ` D ) ) -> ( 0 + 1 ) <_ ( # ` D ) ) )
22 14 20 21 sylc 
 |-  ( ( D e. Fin /\ ( D e. V /\ 2 <_ ( # ` D ) ) ) -> ( 0 + 1 ) <_ ( # ` D ) )
23 11 nn0zd 
 |-  ( D e. Fin -> ( # ` D ) e. ZZ )
24 0z 
 |-  0 e. ZZ
25 23 24 jctil 
 |-  ( D e. Fin -> ( 0 e. ZZ /\ ( # ` D ) e. ZZ ) )
26 25 adantr 
 |-  ( ( D e. Fin /\ ( D e. V /\ 2 <_ ( # ` D ) ) ) -> ( 0 e. ZZ /\ ( # ` D ) e. ZZ ) )
27 zltp1le 
 |-  ( ( 0 e. ZZ /\ ( # ` D ) e. ZZ ) -> ( 0 < ( # ` D ) <-> ( 0 + 1 ) <_ ( # ` D ) ) )
28 26 27 syl 
 |-  ( ( D e. Fin /\ ( D e. V /\ 2 <_ ( # ` D ) ) ) -> ( 0 < ( # ` D ) <-> ( 0 + 1 ) <_ ( # ` D ) ) )
29 22 28 mpbird 
 |-  ( ( D e. Fin /\ ( D e. V /\ 2 <_ ( # ` D ) ) ) -> 0 < ( # ` D ) )
30 0ltpnf 
 |-  0 < +oo
31 simpl 
 |-  ( ( D e. V /\ 2 <_ ( # ` D ) ) -> D e. V )
32 31 anim2i 
 |-  ( ( -. D e. Fin /\ ( D e. V /\ 2 <_ ( # ` D ) ) ) -> ( -. D e. Fin /\ D e. V ) )
33 32 ancomd 
 |-  ( ( -. D e. Fin /\ ( D e. V /\ 2 <_ ( # ` D ) ) ) -> ( D e. V /\ -. D e. Fin ) )
34 hashinf 
 |-  ( ( D e. V /\ -. D e. Fin ) -> ( # ` D ) = +oo )
35 33 34 syl 
 |-  ( ( -. D e. Fin /\ ( D e. V /\ 2 <_ ( # ` D ) ) ) -> ( # ` D ) = +oo )
36 30 35 breqtrrid 
 |-  ( ( -. D e. Fin /\ ( D e. V /\ 2 <_ ( # ` D ) ) ) -> 0 < ( # ` D ) )
37 29 36 pm2.61ian 
 |-  ( ( D e. V /\ 2 <_ ( # ` D ) ) -> 0 < ( # ` D ) )
38 hashgt0n0 
 |-  ( ( D e. V /\ 0 < ( # ` D ) ) -> D =/= (/) )
39 37 38 syldan 
 |-  ( ( D e. V /\ 2 <_ ( # ` D ) ) -> D =/= (/) )
40 rspn0 
 |-  ( D =/= (/) -> ( A. x e. D ( # ` D ) = 1 -> ( # ` D ) = 1 ) )
41 39 40 syl 
 |-  ( ( D e. V /\ 2 <_ ( # ` D ) ) -> ( A. x e. D ( # ` D ) = 1 -> ( # ` D ) = 1 ) )
42 breq2 
 |-  ( ( # ` D ) = 1 -> ( 2 <_ ( # ` D ) <-> 2 <_ 1 ) )
43 6 9 ltnlei 
 |-  ( 1 < 2 <-> -. 2 <_ 1 )
44 pm2.21 
 |-  ( -. 2 <_ 1 -> ( 2 <_ 1 -> -. A. x e. D D = { x } ) )
45 43 44 sylbi 
 |-  ( 1 < 2 -> ( 2 <_ 1 -> -. A. x e. D D = { x } ) )
46 16 45 ax-mp 
 |-  ( 2 <_ 1 -> -. A. x e. D D = { x } )
47 42 46 syl6bi 
 |-  ( ( # ` D ) = 1 -> ( 2 <_ ( # ` D ) -> -. A. x e. D D = { x } ) )
48 47 com12 
 |-  ( 2 <_ ( # ` D ) -> ( ( # ` D ) = 1 -> -. A. x e. D D = { x } ) )
49 48 adantl 
 |-  ( ( D e. V /\ 2 <_ ( # ` D ) ) -> ( ( # ` D ) = 1 -> -. A. x e. D D = { x } ) )
50 41 49 syldc 
 |-  ( A. x e. D ( # ` D ) = 1 -> ( ( D e. V /\ 2 <_ ( # ` D ) ) -> -. A. x e. D D = { x } ) )
51 4 50 syl 
 |-  ( A. x e. D D = { x } -> ( ( D e. V /\ 2 <_ ( # ` D ) ) -> -. A. x e. D D = { x } ) )
52 ax-1 
 |-  ( -. A. x e. D D = { x } -> ( ( D e. V /\ 2 <_ ( # ` D ) ) -> -. A. x e. D D = { x } ) )
53 51 52 pm2.61i 
 |-  ( ( D e. V /\ 2 <_ ( # ` D ) ) -> -. A. x e. D D = { x } )
54 eqsn 
 |-  ( D =/= (/) -> ( D = { x } <-> A. y e. D y = x ) )
55 39 54 syl 
 |-  ( ( D e. V /\ 2 <_ ( # ` D ) ) -> ( D = { x } <-> A. y e. D y = x ) )
56 equcom 
 |-  ( y = x <-> x = y )
57 56 a1i 
 |-  ( ( D e. V /\ 2 <_ ( # ` D ) ) -> ( y = x <-> x = y ) )
58 57 ralbidv 
 |-  ( ( D e. V /\ 2 <_ ( # ` D ) ) -> ( A. y e. D y = x <-> A. y e. D x = y ) )
59 55 58 bitrd 
 |-  ( ( D e. V /\ 2 <_ ( # ` D ) ) -> ( D = { x } <-> A. y e. D x = y ) )
60 59 ralbidv 
 |-  ( ( D e. V /\ 2 <_ ( # ` D ) ) -> ( A. x e. D D = { x } <-> A. x e. D A. y e. D x = y ) )
61 53 60 mtbid 
 |-  ( ( D e. V /\ 2 <_ ( # ` D ) ) -> -. A. x e. D A. y e. D x = y )
62 df-ne 
 |-  ( x =/= y <-> -. x = y )
63 62 rexbii 
 |-  ( E. y e. D x =/= y <-> E. y e. D -. x = y )
64 rexnal 
 |-  ( E. y e. D -. x = y <-> -. A. y e. D x = y )
65 63 64 bitri 
 |-  ( E. y e. D x =/= y <-> -. A. y e. D x = y )
66 65 rexbii 
 |-  ( E. x e. D E. y e. D x =/= y <-> E. x e. D -. A. y e. D x = y )
67 rexnal 
 |-  ( E. x e. D -. A. y e. D x = y <-> -. A. x e. D A. y e. D x = y )
68 66 67 bitri 
 |-  ( E. x e. D E. y e. D x =/= y <-> -. A. x e. D A. y e. D x = y )
69 61 68 sylibr 
 |-  ( ( D e. V /\ 2 <_ ( # ` D ) ) -> E. x e. D E. y e. D x =/= y )