Theorem hasheq0

Description: Two ways of saying a finite 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		0fin	|- (/) 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 = (/) ) )