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	⊢ ( 𝐴 ∈ Fin → ( card ‘ 𝐴 ) ∈ ω )

Proof

Step	Hyp	Ref	Expression
1		isfi	⊢ ( 𝐴 ∈ Fin ↔ ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 )
2	1	biimpi	⊢ ( 𝐴 ∈ Fin → ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 )
3		finnum	⊢ ( 𝐴 ∈ Fin → 𝐴 ∈ dom card )
4		cardid2	⊢ ( 𝐴 ∈ dom card → ( card ‘ 𝐴 ) ≈ 𝐴 )
5	3 4	syl	⊢ ( 𝐴 ∈ Fin → ( card ‘ 𝐴 ) ≈ 𝐴 )
6		entr	⊢ ( ( ( card ‘ 𝐴 ) ≈ 𝐴 ∧ 𝐴 ≈ 𝑥 ) → ( card ‘ 𝐴 ) ≈ 𝑥 )
7	5 6	sylan	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝑥 ) → ( card ‘ 𝐴 ) ≈ 𝑥 )
8		cardon	⊢ ( card ‘ 𝐴 ) ∈ On
9		onomeneq	⊢ ( ( ( card ‘ 𝐴 ) ∈ On ∧ 𝑥 ∈ ω ) → ( ( card ‘ 𝐴 ) ≈ 𝑥 ↔ ( card ‘ 𝐴 ) = 𝑥 ) )
10	8 9	mpan	⊢ ( 𝑥 ∈ ω → ( ( card ‘ 𝐴 ) ≈ 𝑥 ↔ ( card ‘ 𝐴 ) = 𝑥 ) )
11	7 10	imbitrid	⊢ ( 𝑥 ∈ ω → ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝑥 ) → ( card ‘ 𝐴 ) = 𝑥 ) )
12		eleq1a	⊢ ( 𝑥 ∈ ω → ( ( card ‘ 𝐴 ) = 𝑥 → ( card ‘ 𝐴 ) ∈ ω ) )
13	11 12	syld	⊢ ( 𝑥 ∈ ω → ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝑥 ) → ( card ‘ 𝐴 ) ∈ ω ) )
14	13	expcomd	⊢ ( 𝑥 ∈ ω → ( 𝐴 ≈ 𝑥 → ( 𝐴 ∈ Fin → ( card ‘ 𝐴 ) ∈ ω ) ) )
15	14	rexlimiv	⊢ ( ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 → ( 𝐴 ∈ Fin → ( card ‘ 𝐴 ) ∈ ω ) )
16	2 15	mpcom	⊢ ( 𝐴 ∈ Fin → ( card ‘ 𝐴 ) ∈ ω )