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 → 𝐴 ≺ ℕ )