Metamath Proof Explorer

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 ( 𝐴 ∈ Fin ↔ ∃ 𝑛 ∈ ℕ0 ( 1 ... 𝑛 ) ≈ 𝐴 )

Proof

Step Hyp Ref Expression
1 hashcl ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
2 isfinite4 ⊢ ( 𝐴 ∈ Fin ↔ ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ 𝐴 )
3 2 biimpi ⊢ ( 𝐴 ∈ Fin → ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ 𝐴 )
4 1 3 jca ⊢ ( 𝐴 ∈ Fin → ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ 𝐴 ) )
5 eleq1 ⊢ ( 𝑛 = ( ♯ ‘ 𝐴 ) → ( 𝑛 ∈ ℕ0 ↔ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) )
6 oveq2 ⊢ ( 𝑛 = ( ♯ ‘ 𝐴 ) → ( 1 ... 𝑛 ) = ( 1 ... ( ♯ ‘ 𝐴 ) ) )
7 6 breq1d ⊢ ( 𝑛 = ( ♯ ‘ 𝐴 ) → ( ( 1 ... 𝑛 ) ≈ 𝐴 ↔ ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ 𝐴 ) )
8 5 7 anbi12d ⊢ ( 𝑛 = ( ♯ ‘ 𝐴 ) → ( ( 𝑛 ∈ ℕ0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) ↔ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ 𝐴 ) ) )
9 1 4 8 spcedv ⊢ ( 𝐴 ∈ Fin → ∃ 𝑛 ( 𝑛 ∈ ℕ0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) )
10 df-rex ⊢ ( ∃ 𝑛 ∈ ℕ0 ( 1 ... 𝑛 ) ≈ 𝐴 ↔ ∃ 𝑛 ( 𝑛 ∈ ℕ0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) )
11 9 10 sylibr ⊢ ( 𝐴 ∈ Fin → ∃ 𝑛 ∈ ℕ0 ( 1 ... 𝑛 ) ≈ 𝐴 )
12 hasheni ⊢ ( ( 1 ... 𝑛 ) ≈ 𝐴 → ( ♯ ‘ ( 1 ... 𝑛 ) ) = ( ♯ ‘ 𝐴 ) )
13 12 eqcomd ⊢ ( ( 1 ... 𝑛 ) ≈ 𝐴 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ ( 1 ... 𝑛 ) ) )
14 hashfz1 ⊢ ( 𝑛 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑛 ) ) = 𝑛 )
15 ovex ⊢ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∈ V
16 eqtr ⊢ ( ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ ( 1 ... 𝑛 ) ) ∧ ( ♯ ‘ ( 1 ... 𝑛 ) ) = 𝑛 ) → ( ♯ ‘ 𝐴 ) = 𝑛 )
17 oveq2 ⊢ ( ( ♯ ‘ 𝐴 ) = 𝑛 → ( 1 ... ( ♯ ‘ 𝐴 ) ) = ( 1 ... 𝑛 ) )
18 eqeng ⊢ ( ( 1 ... ( ♯ ‘ 𝐴 ) ) ∈ V → ( ( 1 ... ( ♯ ‘ 𝐴 ) ) = ( 1 ... 𝑛 ) → ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ ( 1 ... 𝑛 ) ) )
19 17 18 syl5 ⊢ ( ( 1 ... ( ♯ ‘ 𝐴 ) ) ∈ V → ( ( ♯ ‘ 𝐴 ) = 𝑛 → ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ ( 1 ... 𝑛 ) ) )
20 15 16 19 mpsyl ⊢ ( ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ ( 1 ... 𝑛 ) ) ∧ ( ♯ ‘ ( 1 ... 𝑛 ) ) = 𝑛 ) → ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ ( 1 ... 𝑛 ) )
21 13 14 20 syl2anr ⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) → ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ ( 1 ... 𝑛 ) )
22 entr ⊢ ( ( ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ ( 1 ... 𝑛 ) ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) → ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ 𝐴 )
23 21 22 sylancom ⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) → ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ 𝐴 )
24 23 2 sylibr ⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( 1 ... 𝑛 ) ≈ 𝐴 ) → 𝐴 ∈ Fin )
25 24 rexlimiva ⊢ ( ∃ 𝑛 ∈ ℕ0 ( 1 ... 𝑛 ) ≈ 𝐴 → 𝐴 ∈ Fin )
26 11 25 impbii ⊢ ( 𝐴 ∈ Fin ↔ ∃ 𝑛 ∈ ℕ0 ( 1 ... 𝑛 ) ≈ 𝐴 )