This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: If A is equinumerous to a natural number, then that number is its
cardinal. (Contributed by Mario Carneiro, 11-Jan-2013)
|
|
Ref |
Expression |
|
Assertion |
cardennn |
⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ ω ) → ( card ‘ 𝐴 ) = 𝐵 ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
carden2b |
⊢ ( 𝐴 ≈ 𝐵 → ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) ) |
| 2 |
|
cardnn |
⊢ ( 𝐵 ∈ ω → ( card ‘ 𝐵 ) = 𝐵 ) |
| 3 |
1 2
|
sylan9eq |
⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ ω ) → ( card ‘ 𝐴 ) = 𝐵 ) |