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	⊢ ( 𝐴 ∈ Fin ↔ ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		hashcl	⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
2		hashfz1	⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) = ( ♯ ‘ 𝐴 ) )
3	1 2	syl	⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) = ( ♯ ‘ 𝐴 ) )
4		fzfi	⊢ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∈ Fin
5		hashen	⊢ ( ( ( 1 ... ( ♯ ‘ 𝐴 ) ) ∈ Fin ∧ 𝐴 ∈ Fin ) → ( ( ♯ ‘ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) = ( ♯ ‘ 𝐴 ) ↔ ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ 𝐴 ) )
6	4 5	mpan	⊢ ( 𝐴 ∈ Fin → ( ( ♯ ‘ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) = ( ♯ ‘ 𝐴 ) ↔ ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ 𝐴 ) )
7	3 6	mpbid	⊢ ( 𝐴 ∈ Fin → ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ 𝐴 )
8		ensym	⊢ ( ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ 𝐴 → 𝐴 ≈ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
9		enfi	⊢ ( 𝐴 ≈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( 𝐴 ∈ Fin ↔ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∈ Fin ) )
10	9	biimprcd	⊢ ( ( 1 ... ( ♯ ‘ 𝐴 ) ) ∈ Fin → ( 𝐴 ≈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → 𝐴 ∈ Fin ) )
11	4 8 10	mpsyl	⊢ ( ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ 𝐴 → 𝐴 ∈ Fin )
12	7 11	impbii	⊢ ( 𝐴 ∈ Fin ↔ ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ 𝐴 )