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

Metamath Proof Explorer

Theorem hashgt0elex

Description: If the size of a set is greater than zero, then the set must contain at least one element. (Contributed by Alexander van der Vekens, 6-Jan-2018)

Ref Expression
Assertion hashgt0elex 
|- ( ( V e. W /\ 0 < ( # ` V ) ) -> E. x x e. V )

Proof

Step Hyp Ref Expression
1 alnex 
 |-  ( A. x -. x e. V <-> -. E. x x e. V )
2 eq0 
 |-  ( V = (/) <-> A. x -. x e. V )
3 2 biimpri 
 |-  ( A. x -. x e. V -> V = (/) )
4 3 a1d 
 |-  ( A. x -. x e. V -> ( V e. W -> V = (/) ) )
5 1 4 sylbir 
 |-  ( -. E. x x e. V -> ( V e. W -> V = (/) ) )
6 5 impcom 
 |-  ( ( V e. W /\ -. E. x x e. V ) -> V = (/) )
7 hashle00 
 |-  ( V e. W -> ( ( # ` V ) <_ 0 <-> V = (/) ) )
8 7 adantr 
 |-  ( ( V e. W /\ -. E. x x e. V ) -> ( ( # ` V ) <_ 0 <-> V = (/) ) )
9 6 8 mpbird 
 |-  ( ( V e. W /\ -. E. x x e. V ) -> ( # ` V ) <_ 0 )
10 hashxrcl 
 |-  ( V e. W -> ( # ` V ) e. RR* )
11 0xr 
 |-  0 e. RR*
12 xrlenlt 
 |-  ( ( ( # ` V ) e. RR* /\ 0 e. RR* ) -> ( ( # ` V ) <_ 0 <-> -. 0 < ( # ` V ) ) )
13 10 11 12 sylancl 
 |-  ( V e. W -> ( ( # ` V ) <_ 0 <-> -. 0 < ( # ` V ) ) )
14 13 bicomd 
 |-  ( V e. W -> ( -. 0 < ( # ` V ) <-> ( # ` V ) <_ 0 ) )
15 14 adantr 
 |-  ( ( V e. W /\ -. E. x x e. V ) -> ( -. 0 < ( # ` V ) <-> ( # ` V ) <_ 0 ) )
16 9 15 mpbird 
 |-  ( ( V e. W /\ -. E. x x e. V ) -> -. 0 < ( # ` V ) )
17 16 ex 
 |-  ( V e. W -> ( -. E. x x e. V -> -. 0 < ( # ` V ) ) )
18 17 con4d 
 |-  ( V e. W -> ( 0 < ( # ` V ) -> E. x x e. V ) )
19 18 imp 
 |-  ( ( V e. W /\ 0 < ( # ` V ) ) -> E. x x e. V )