Theorem hashneq0

Description: Two ways of saying a set is not empty. (Contributed by Alexander van der Vekens, 23-Sep-2018)

	Ref	Expression
Assertion	hashneq0	|- ( A e. V -> ( 0 < ( # ` A ) <-> A =/= (/) ) )

Proof

Step	Hyp	Ref	Expression
1		hashnn0pnf	|- ( A e. V -> ( ( # ` A ) e. NN0 \/ ( # ` A ) = +oo ) )
2		nn0re	|- ( ( # ` A ) e. NN0 -> ( # ` A ) e. RR )
3		nn0ge0	|- ( ( # ` A ) e. NN0 -> 0 <_ ( # ` A ) )
4		ne0gt0	|- ( ( ( # ` A ) e. RR /\ 0 <_ ( # ` A ) ) -> ( ( # ` A ) =/= 0 <-> 0 < ( # ` A ) ) )
5	2 3 4	syl2anc	|- ( ( # ` A ) e. NN0 -> ( ( # ` A ) =/= 0 <-> 0 < ( # ` A ) ) )
6	5	bicomd	|- ( ( # ` A ) e. NN0 -> ( 0 < ( # ` A ) <-> ( # ` A ) =/= 0 ) )
7		breq2	|- ( ( # ` A ) = +oo -> ( 0 < ( # ` A ) <-> 0 < +oo ) )
8		0ltpnf	|- 0 < +oo
9		0re	|- 0 e. RR
10		renepnf	|- ( 0 e. RR -> 0 =/= +oo )
11	9 10	ax-mp	|- 0 =/= +oo
12	11	necomi	|- +oo =/= 0
13	8 12	2th	|- ( 0 < +oo <-> +oo =/= 0 )
14		neeq1	|- ( ( # ` A ) = +oo -> ( ( # ` A ) =/= 0 <-> +oo =/= 0 ) )
15	13 14	bitr4id	|- ( ( # ` A ) = +oo -> ( 0 < +oo <-> ( # ` A ) =/= 0 ) )
16	7 15	bitrd	|- ( ( # ` A ) = +oo -> ( 0 < ( # ` A ) <-> ( # ` A ) =/= 0 ) )
17	6 16	jaoi	|- ( ( ( # ` A ) e. NN0 \/ ( # ` A ) = +oo ) -> ( 0 < ( # ` A ) <-> ( # ` A ) =/= 0 ) )
18	1 17	syl	|- ( A e. V -> ( 0 < ( # ` A ) <-> ( # ` A ) =/= 0 ) )
19		hasheq0	|- ( A e. V -> ( ( # ` A ) = 0 <-> A = (/) ) )
20	19	necon3bid	|- ( A e. V -> ( ( # ` A ) =/= 0 <-> A =/= (/) ) )
21	18 20	bitrd	|- ( A e. V -> ( 0 < ( # ` A ) <-> A =/= (/) ) )