Theorem hashge1

Description: The cardinality of a nonempty set is greater than or equal to one. (Contributed by Thierry Arnoux, 20-Jun-2017)

	Ref	Expression
Assertion	hashge1	|- ( ( A e. V /\ A =/= (/) ) -> 1 <_ ( # ` A ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( ( A e. V /\ A =/= (/) ) /\ A e. Fin ) -> A e. Fin )
2		simplr	|- ( ( ( A e. V /\ A =/= (/) ) /\ A e. Fin ) -> A =/= (/) )
3		hashnncl	|- ( A e. Fin -> ( ( # ` A ) e. NN <-> A =/= (/) ) )
4	3	biimpar	|- ( ( A e. Fin /\ A =/= (/) ) -> ( # ` A ) e. NN )
5	1 2 4	syl2anc	|- ( ( ( A e. V /\ A =/= (/) ) /\ A e. Fin ) -> ( # ` A ) e. NN )
6	5	nnge1d	|- ( ( ( A e. V /\ A =/= (/) ) /\ A e. Fin ) -> 1 <_ ( # ` A ) )
7		1xr	|- 1 e. RR*
8		pnfge	|- ( 1 e. RR* -> 1 <_ +oo )
9	7 8	ax-mp	|- 1 <_ +oo
10		hashinf	|- ( ( A e. V /\ -. A e. Fin ) -> ( # ` A ) = +oo )
11	10	adantlr	|- ( ( ( A e. V /\ A =/= (/) ) /\ -. A e. Fin ) -> ( # ` A ) = +oo )
12	9 11	breqtrrid	|- ( ( ( A e. V /\ A =/= (/) ) /\ -. A e. Fin ) -> 1 <_ ( # ` A ) )
13	6 12	pm2.61dan	|- ( ( A e. V /\ A =/= (/) ) -> 1 <_ ( # ` A ) )