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 ( 𝐴 ∈ 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 syl5ib ( 𝑥 ∈ ω → ( ( 𝐴 ∈ 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 ‘ 𝐴 ) ∈ ω )