Metamath Proof Explorer

Theorem ficardom

Description: The cardinal number of a finite set is a finite ordinal. (Contributed by Paul Chapman, 11-Apr-2009) (Revised by Mario Carneiro, 4-Feb-2013)

		Ref	Expression
	Assertion	ficardom	$⊢ A \in Fin \to card (A) \in ω$

Proof

Step	Hyp	Ref	Expression
1		isfi	$⊢ A \in Fin \leftrightarrow \exists x \in ω A \approx x$
2	1	biimpi	$⊢ A \in Fin \to \exists x \in ω A \approx x$
3		finnum	$⊢ A \in Fin \to A \in dom card$
4		cardid2	$⊢ A \in dom card \to card (A) \approx A$
5	3 4	syl	$⊢ A \in Fin \to card (A) \approx A$
6		entr	$⊢ (card (A) \approx A \land A \approx x) \to card (A) \approx x$
7	5 6	sylan	$⊢ (A \in Fin \land A \approx x) \to card (A) \approx x$
8		cardon	$⊢ card (A) \in On$
9		onomeneq	$⊢ (card (A) \in On \land x \in ω) \to (card (A) \approx x \leftrightarrow card (A) = x)$
10	8 9	mpan	$⊢ x \in ω \to (card (A) \approx x \leftrightarrow card (A) = x)$
11	7 10	imbitrid	$⊢ x \in ω \to ((A \in Fin \land A \approx x) \to card (A) = x)$
12		eleq1a	$⊢ x \in ω \to (card (A) = x \to card (A) \in ω)$
13	11 12	syld	$⊢ x \in ω \to ((A \in Fin \land A \approx x) \to card (A) \in ω)$
14	13	expcomd	$⊢ x \in ω \to (A \approx x \to (A \in Fin \to card (A) \in ω))$
15	14	rexlimiv	$⊢ \exists x \in ω A \approx x \to (A \in Fin \to card (A) \in ω)$
16	2 15	mpcom	$⊢ A \in Fin \to card (A) \in ω$