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 )