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

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