Theorem rp-isfinite5

Description: A set is said to be finite if it can be put in one-to-one correspondence with all the natural numbers between 1 and some n e. NN0 . (Contributed by RP, 3-Mar-2020)

	Ref	Expression
Assertion	rp-isfinite5	|- ( A e. Fin <-> E. n e. NN0 ( 1 ... n ) ~~ A )

Proof

Step	Hyp	Ref	Expression
1		fvex	|- ( # ` A ) e. _V
2		hashcl	|- ( A e. Fin -> ( # ` A ) e. NN0 )
3		isfinite4	|- ( A e. Fin <-> ( 1 ... ( # ` A ) ) ~~ A )
4	3	biimpi	|- ( A e. Fin -> ( 1 ... ( # ` A ) ) ~~ A )
5	2 4	jca	|- ( A e. Fin -> ( ( # ` A ) e. NN0 /\ ( 1 ... ( # ` A ) ) ~~ A ) )
6		eleq1	|- ( n = ( # ` A ) -> ( n e. NN0 <-> ( # ` A ) e. NN0 ) )
7		oveq2	|- ( n = ( # ` A ) -> ( 1 ... n ) = ( 1 ... ( # ` A ) ) )
8	7	breq1d	|- ( n = ( # ` A ) -> ( ( 1 ... n ) ~~ A <-> ( 1 ... ( # ` A ) ) ~~ A ) )
9	6 8	anbi12d	|- ( n = ( # ` A ) -> ( ( n e. NN0 /\ ( 1 ... n ) ~~ A ) <-> ( ( # ` A ) e. NN0 /\ ( 1 ... ( # ` A ) ) ~~ A ) ) )
10	9	spcegv	|- ( ( # ` A ) e. _V -> ( ( ( # ` A ) e. NN0 /\ ( 1 ... ( # ` A ) ) ~~ A ) -> E. n ( n e. NN0 /\ ( 1 ... n ) ~~ A ) ) )
11	1 5 10	mpsyl	|- ( A e. Fin -> E. n ( n e. NN0 /\ ( 1 ... n ) ~~ A ) )
12		df-rex	|- ( E. n e. NN0 ( 1 ... n ) ~~ A <-> E. n ( n e. NN0 /\ ( 1 ... n ) ~~ A ) )
13	11 12	sylibr	|- ( A e. Fin -> E. n e. NN0 ( 1 ... n ) ~~ A )
14		hasheni	|- ( ( 1 ... n ) ~~ A -> ( # ` ( 1 ... n ) ) = ( # ` A ) )
15	14	eqcomd	|- ( ( 1 ... n ) ~~ A -> ( # ` A ) = ( # ` ( 1 ... n ) ) )
16		hashfz1	|- ( n e. NN0 -> ( # ` ( 1 ... n ) ) = n )
17		ovex	|- ( 1 ... ( # ` A ) ) e. _V
18		eqtr	|- ( ( ( # ` A ) = ( # ` ( 1 ... n ) ) /\ ( # ` ( 1 ... n ) ) = n ) -> ( # ` A ) = n )
19		oveq2	|- ( ( # ` A ) = n -> ( 1 ... ( # ` A ) ) = ( 1 ... n ) )
20		eqeng	|- ( ( 1 ... ( # ` A ) ) e. _V -> ( ( 1 ... ( # ` A ) ) = ( 1 ... n ) -> ( 1 ... ( # ` A ) ) ~~ ( 1 ... n ) ) )
21	19 20	syl5	|- ( ( 1 ... ( # ` A ) ) e. _V -> ( ( # ` A ) = n -> ( 1 ... ( # ` A ) ) ~~ ( 1 ... n ) ) )
22	17 18 21	mpsyl	|- ( ( ( # ` A ) = ( # ` ( 1 ... n ) ) /\ ( # ` ( 1 ... n ) ) = n ) -> ( 1 ... ( # ` A ) ) ~~ ( 1 ... n ) )
23	15 16 22	syl2anr	|- ( ( n e. NN0 /\ ( 1 ... n ) ~~ A ) -> ( 1 ... ( # ` A ) ) ~~ ( 1 ... n ) )
24		entr	|- ( ( ( 1 ... ( # ` A ) ) ~~ ( 1 ... n ) /\ ( 1 ... n ) ~~ A ) -> ( 1 ... ( # ` A ) ) ~~ A )
25	23 24	sylancom	|- ( ( n e. NN0 /\ ( 1 ... n ) ~~ A ) -> ( 1 ... ( # ` A ) ) ~~ A )
26	25 3	sylibr	|- ( ( n e. NN0 /\ ( 1 ... n ) ~~ A ) -> A e. Fin )
27	26	rexlimiva	|- ( E. n e. NN0 ( 1 ... n ) ~~ A -> A e. Fin )
28	13 27	impbii	|- ( A e. Fin <-> E. n e. NN0 ( 1 ... n ) ~~ A )