This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hashge2el2difr

Description: A set with at least 2 different elements has size at least 2. (Contributed by AV, 14-Oct-2020)

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

Proof

Step Hyp Ref Expression
1 hashv01gt1 
 |-  ( D e. V -> ( ( # ` D ) = 0 \/ ( # ` D ) = 1 \/ 1 < ( # ` D ) ) )
2 hasheq0 
 |-  ( D e. V -> ( ( # ` D ) = 0 <-> D = (/) ) )
3 rexeq 
 |-  ( D = (/) -> ( E. x e. D E. y e. D x =/= y <-> E. x e. (/) E. y e. D x =/= y ) )
4 rex0 
 |-  -. E. x e. (/) E. y e. D x =/= y
5 pm2.21 
 |-  ( -. E. x e. (/) E. y e. D x =/= y -> ( E. x e. (/) E. y e. D x =/= y -> 2 <_ ( # ` D ) ) )
6 4 5 mp1i 
 |-  ( D = (/) -> ( E. x e. (/) E. y e. D x =/= y -> 2 <_ ( # ` D ) ) )
7 3 6 sylbid 
 |-  ( D = (/) -> ( E. x e. D E. y e. D x =/= y -> 2 <_ ( # ` D ) ) )
8 2 7 biimtrdi 
 |-  ( D e. V -> ( ( # ` D ) = 0 -> ( E. x e. D E. y e. D x =/= y -> 2 <_ ( # ` D ) ) ) )
9 8 com12 
 |-  ( ( # ` D ) = 0 -> ( D e. V -> ( E. x e. D E. y e. D x =/= y -> 2 <_ ( # ` D ) ) ) )
10 hash1snb 
 |-  ( D e. V -> ( ( # ` D ) = 1 <-> E. z D = { z } ) )
11 rexeq 
 |-  ( D = { z } -> ( E. y e. D x =/= y <-> E. y e. { z } x =/= y ) )
12 11 rexeqbi1dv 
 |-  ( D = { z } -> ( E. x e. D E. y e. D x =/= y <-> E. x e. { z } E. y e. { z } x =/= y ) )
13 vex 
 |-  z e. _V
14 neeq1 
 |-  ( x = z -> ( x =/= y <-> z =/= y ) )
15 14 rexbidv 
 |-  ( x = z -> ( E. y e. { z } x =/= y <-> E. y e. { z } z =/= y ) )
16 13 15 rexsn 
 |-  ( E. x e. { z } E. y e. { z } x =/= y <-> E. y e. { z } z =/= y )
17 neeq2 
 |-  ( y = z -> ( z =/= y <-> z =/= z ) )
18 13 17 rexsn 
 |-  ( E. y e. { z } z =/= y <-> z =/= z )
19 16 18 bitri 
 |-  ( E. x e. { z } E. y e. { z } x =/= y <-> z =/= z )
20 12 19 bitrdi 
 |-  ( D = { z } -> ( E. x e. D E. y e. D x =/= y <-> z =/= z ) )
21 equid 
 |-  z = z
22 eqneqall 
 |-  ( z = z -> ( z =/= z -> 2 <_ ( # ` D ) ) )
23 21 22 mp1i 
 |-  ( D = { z } -> ( z =/= z -> 2 <_ ( # ` D ) ) )
24 20 23 sylbid 
 |-  ( D = { z } -> ( E. x e. D E. y e. D x =/= y -> 2 <_ ( # ` D ) ) )
25 24 exlimiv 
 |-  ( E. z D = { z } -> ( E. x e. D E. y e. D x =/= y -> 2 <_ ( # ` D ) ) )
26 10 25 biimtrdi 
 |-  ( D e. V -> ( ( # ` D ) = 1 -> ( E. x e. D E. y e. D x =/= y -> 2 <_ ( # ` D ) ) ) )
27 26 com12 
 |-  ( ( # ` D ) = 1 -> ( D e. V -> ( E. x e. D E. y e. D x =/= y -> 2 <_ ( # ` D ) ) ) )
28 hashnn0pnf 
 |-  ( D e. V -> ( ( # ` D ) e. NN0 \/ ( # ` D ) = +oo ) )
29 1z 
 |-  1 e. ZZ
30 nn0z 
 |-  ( ( # ` D ) e. NN0 -> ( # ` D ) e. ZZ )
31 zltp1le 
 |-  ( ( 1 e. ZZ /\ ( # ` D ) e. ZZ ) -> ( 1 < ( # ` D ) <-> ( 1 + 1 ) <_ ( # ` D ) ) )
32 31 biimpd 
 |-  ( ( 1 e. ZZ /\ ( # ` D ) e. ZZ ) -> ( 1 < ( # ` D ) -> ( 1 + 1 ) <_ ( # ` D ) ) )
33 29 30 32 sylancr 
 |-  ( ( # ` D ) e. NN0 -> ( 1 < ( # ` D ) -> ( 1 + 1 ) <_ ( # ` D ) ) )
34 df-2 
 |-  2 = ( 1 + 1 )
35 34 breq1i 
 |-  ( 2 <_ ( # ` D ) <-> ( 1 + 1 ) <_ ( # ` D ) )
36 33 35 imbitrrdi 
 |-  ( ( # ` D ) e. NN0 -> ( 1 < ( # ` D ) -> 2 <_ ( # ` D ) ) )
37 2re 
 |-  2 e. RR
38 37 rexri 
 |-  2 e. RR*
39 pnfge 
 |-  ( 2 e. RR* -> 2 <_ +oo )
40 38 39 mp1i 
 |-  ( ( # ` D ) = +oo -> 2 <_ +oo )
41 breq2 
 |-  ( ( # ` D ) = +oo -> ( 2 <_ ( # ` D ) <-> 2 <_ +oo ) )
42 40 41 mpbird 
 |-  ( ( # ` D ) = +oo -> 2 <_ ( # ` D ) )
43 42 a1d 
 |-  ( ( # ` D ) = +oo -> ( 1 < ( # ` D ) -> 2 <_ ( # ` D ) ) )
44 36 43 jaoi 
 |-  ( ( ( # ` D ) e. NN0 \/ ( # ` D ) = +oo ) -> ( 1 < ( # ` D ) -> 2 <_ ( # ` D ) ) )
45 28 44 syl 
 |-  ( D e. V -> ( 1 < ( # ` D ) -> 2 <_ ( # ` D ) ) )
46 45 impcom 
 |-  ( ( 1 < ( # ` D ) /\ D e. V ) -> 2 <_ ( # ` D ) )
47 46 a1d 
 |-  ( ( 1 < ( # ` D ) /\ D e. V ) -> ( E. x e. D E. y e. D x =/= y -> 2 <_ ( # ` D ) ) )
48 47 ex 
 |-  ( 1 < ( # ` D ) -> ( D e. V -> ( E. x e. D E. y e. D x =/= y -> 2 <_ ( # ` D ) ) ) )
49 9 27 48 3jaoi 
 |-  ( ( ( # ` D ) = 0 \/ ( # ` D ) = 1 \/ 1 < ( # ` D ) ) -> ( D e. V -> ( E. x e. D E. y e. D x =/= y -> 2 <_ ( # ` D ) ) ) )
50 1 49 mpcom 
 |-  ( D e. V -> ( E. x e. D E. y e. D x =/= y -> 2 <_ ( # ` D ) ) )
51 50 imp 
 |-  ( ( D e. V /\ E. x e. D E. y e. D x =/= y ) -> 2 <_ ( # ` D ) )