Metamath Proof Explorer


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 =/= (/) ) )