Metamath Proof Explorer


Theorem isfinite4

Description: A finite set is equinumerous to the range of integers from one up to the hash value of the set. In other words, counting objects with natural numbers works if and only if it is a finite collection. (Contributed by Richard Penner, 26-Feb-2020)

Ref Expression
Assertion isfinite4
|- ( A e. Fin <-> ( 1 ... ( # ` A ) ) ~~ A )

Proof

Step Hyp Ref Expression
1 hashcl
 |-  ( A e. Fin -> ( # ` A ) e. NN0 )
2 hashfz1
 |-  ( ( # ` A ) e. NN0 -> ( # ` ( 1 ... ( # ` A ) ) ) = ( # ` A ) )
3 1 2 syl
 |-  ( A e. Fin -> ( # ` ( 1 ... ( # ` A ) ) ) = ( # ` A ) )
4 fzfi
 |-  ( 1 ... ( # ` A ) ) e. Fin
5 hashen
 |-  ( ( ( 1 ... ( # ` A ) ) e. Fin /\ A e. Fin ) -> ( ( # ` ( 1 ... ( # ` A ) ) ) = ( # ` A ) <-> ( 1 ... ( # ` A ) ) ~~ A ) )
6 4 5 mpan
 |-  ( A e. Fin -> ( ( # ` ( 1 ... ( # ` A ) ) ) = ( # ` A ) <-> ( 1 ... ( # ` A ) ) ~~ A ) )
7 3 6 mpbid
 |-  ( A e. Fin -> ( 1 ... ( # ` A ) ) ~~ A )
8 ensym
 |-  ( ( 1 ... ( # ` A ) ) ~~ A -> A ~~ ( 1 ... ( # ` A ) ) )
9 enfi
 |-  ( A ~~ ( 1 ... ( # ` A ) ) -> ( A e. Fin <-> ( 1 ... ( # ` A ) ) e. Fin ) )
10 9 biimprcd
 |-  ( ( 1 ... ( # ` A ) ) e. Fin -> ( A ~~ ( 1 ... ( # ` A ) ) -> A e. Fin ) )
11 4 8 10 mpsyl
 |-  ( ( 1 ... ( # ` A ) ) ~~ A -> A e. Fin )
12 7 11 impbii
 |-  ( A e. Fin <-> ( 1 ... ( # ` A ) ) ~~ A )