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 ‘ 𝐴 ) = 𝐵 ) |