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

Metamath Proof Explorer

Theorem hasheq0

Description: Two ways of saying a set is empty. (Contributed by Paul Chapman, 26-Oct-2012) (Revised by Mario Carneiro, 27-Jul-2014)

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

Proof

Step Hyp Ref Expression
1 pnfnre 
 |-  +oo e/ RR
2 1 neli 
 |-  -. +oo e. RR
3 hashinf 
 |-  ( ( A e. V /\ -. A e. Fin ) -> ( # ` A ) = +oo )
4 3 eleq1d 
 |-  ( ( A e. V /\ -. A e. Fin ) -> ( ( # ` A ) e. RR <-> +oo e. RR ) )
5 2 4 mtbiri 
 |-  ( ( A e. V /\ -. A e. Fin ) -> -. ( # ` A ) e. RR )
6 id 
 |-  ( ( # ` A ) = 0 -> ( # ` A ) = 0 )
7 0re 
 |-  0 e. RR
8 6 7 eqeltrdi 
 |-  ( ( # ` A ) = 0 -> ( # ` A ) e. RR )
9 5 8 nsyl 
 |-  ( ( A e. V /\ -. A e. Fin ) -> -. ( # ` A ) = 0 )
10 id 
 |-  ( A = (/) -> A = (/) )
11 0fi 
 |-  (/) e. Fin
12 10 11 eqeltrdi 
 |-  ( A = (/) -> A e. Fin )
13 12 con3i 
 |-  ( -. A e. Fin -> -. A = (/) )
14 13 adantl 
 |-  ( ( A e. V /\ -. A e. Fin ) -> -. A = (/) )
15 9 14 2falsed 
 |-  ( ( A e. V /\ -. A e. Fin ) -> ( ( # ` A ) = 0 <-> A = (/) ) )
16 15 ex 
 |-  ( A e. V -> ( -. A e. Fin -> ( ( # ` A ) = 0 <-> A = (/) ) ) )
17 hashen 
 |-  ( ( A e. Fin /\ (/) e. Fin ) -> ( ( # ` A ) = ( # ` (/) ) <-> A ~~ (/) ) )
18 11 17 mpan2 
 |-  ( A e. Fin -> ( ( # ` A ) = ( # ` (/) ) <-> A ~~ (/) ) )
19 fz10 
 |-  ( 1 ... 0 ) = (/)
20 19 fveq2i 
 |-  ( # ` ( 1 ... 0 ) ) = ( # ` (/) )
21 0nn0 
 |-  0 e. NN0
22 hashfz1 
 |-  ( 0 e. NN0 -> ( # ` ( 1 ... 0 ) ) = 0 )
23 21 22 ax-mp 
 |-  ( # ` ( 1 ... 0 ) ) = 0
24 20 23 eqtr3i 
 |-  ( # ` (/) ) = 0
25 24 eqeq2i 
 |-  ( ( # ` A ) = ( # ` (/) ) <-> ( # ` A ) = 0 )
26 en0 
 |-  ( A ~~ (/) <-> A = (/) )
27 18 25 26 3bitr3g 
 |-  ( A e. Fin -> ( ( # ` A ) = 0 <-> A = (/) ) )
28 16 27 pm2.61d2 
 |-  ( A e. V -> ( ( # ` A ) = 0 <-> A = (/) ) )