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