This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ‘ 𝐴 ) ∈ ω )