Metamath Proof Explorer


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 ) )