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

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