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 ∈ Fin → card ⁡ A ∈ ω

Proof

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