fisdomnn

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

		Ref	Expression
	Assertion	fisdomnn	$⊢ A \in Fin \to A ≺ ℕ$

Step	Hyp	Ref	Expression
1		canth2g	$⊢ A \in Fin \to A ≺ 𝒫 A$
2		pwfi	$⊢ A \in Fin \leftrightarrow 𝒫 A \in Fin$
3		fzfi	$⊢ (1 \dots \|𝒫 A\|) \in Fin$
4		nnex	$⊢ ℕ \in V$
5		fz1ssnn	$⊢ (1 \dots \|𝒫 A\|) \subseteq ℕ$
6		ssdomfi2	$⊢ ((1 \dots \|𝒫 A\|) \in Fin \land ℕ \in V \land (1 \dots \|𝒫 A\|) \subseteq ℕ) \to (1 \dots \|𝒫 A\|) ≼ ℕ$
7	3 4 5 6	mp3an	$⊢ (1 \dots \|𝒫 A\|) ≼ ℕ$
8		isfinite4	$⊢ 𝒫 A \in Fin \leftrightarrow (1 \dots \|𝒫 A\|) \approx 𝒫 A$
9		domen1	$⊢ (1 \dots \|𝒫 A\|) \approx 𝒫 A \to ((1 \dots \|𝒫 A\|) ≼ ℕ \leftrightarrow 𝒫 A ≼ ℕ)$
10	8 9	sylbi	$⊢ 𝒫 A \in Fin \to ((1 \dots \|𝒫 A\|) ≼ ℕ \leftrightarrow 𝒫 A ≼ ℕ)$
11	7 10	mpbii	$⊢ 𝒫 A \in Fin \to 𝒫 A ≼ ℕ$
12	2 11	sylbi	$⊢ A \in Fin \to 𝒫 A ≼ ℕ$
13		sdomdomtrfi	$⊢ (A \in Fin \land A ≺ 𝒫 A \land 𝒫 A ≼ ℕ) \to A ≺ ℕ$
14	1 12 13	mpd3an23	$⊢ A \in Fin \to A ≺ ℕ$

Metamath Proof Explorer