This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fisdomnn

Description: A finite set is dominated by the set of natural numbers. (Contributed by SN, 6-Jul-2025)

Ref Expression
Assertion fisdomnn ( 𝐴 ∈ Fin → 𝐴 ≺ ℕ )

Proof

Step Hyp Ref Expression
1 canth2g ⊢ ( 𝐴 ∈ Fin → 𝐴 ≺ 𝒫 𝐴 )
2 pwfi ⊢ ( 𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin )
3 fzfi ⊢ ( 1 ... ( ♯ ‘ 𝒫 𝐴 ) ) ∈ Fin
4 nnex ⊢ ℕ ∈ V
5 fz1ssnn ⊢ ( 1 ... ( ♯ ‘ 𝒫 𝐴 ) ) ⊆ ℕ
6 ssdomfi2 ⊢ ( ( ( 1 ... ( ♯ ‘ 𝒫 𝐴 ) ) ∈ Fin ∧ ℕ ∈ V ∧ ( 1 ... ( ♯ ‘ 𝒫 𝐴 ) ) ⊆ ℕ ) → ( 1 ... ( ♯ ‘ 𝒫 𝐴 ) ) ≼ ℕ )
7 3 4 5 6 mp3an ⊢ ( 1 ... ( ♯ ‘ 𝒫 𝐴 ) ) ≼ ℕ
8 isfinite4 ⊢ ( 𝒫 𝐴 ∈ Fin ↔ ( 1 ... ( ♯ ‘ 𝒫 𝐴 ) ) ≈ 𝒫 𝐴 )
9 domen1 ⊢ ( ( 1 ... ( ♯ ‘ 𝒫 𝐴 ) ) ≈ 𝒫 𝐴 → ( ( 1 ... ( ♯ ‘ 𝒫 𝐴 ) ) ≼ ℕ ↔ 𝒫 𝐴 ≼ ℕ ) )
10 8 9 sylbi ⊢ ( 𝒫 𝐴 ∈ Fin → ( ( 1 ... ( ♯ ‘ 𝒫 𝐴 ) ) ≼ ℕ ↔ 𝒫 𝐴 ≼ ℕ ) )
11 7 10 mpbii ⊢ ( 𝒫 𝐴 ∈ Fin → 𝒫 𝐴 ≼ ℕ )
12 2 11 sylbi ⊢ ( 𝐴 ∈ Fin → 𝒫 𝐴 ≼ ℕ )
13 sdomdomtrfi ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≺ 𝒫 𝐴 ∧ 𝒫 𝐴 ≼ ℕ ) → 𝐴 ≺ ℕ )
14 1 12 13 mpd3an23 ⊢ ( 𝐴 ∈ Fin → 𝐴 ≺ ℕ )