Metamath Proof Explorer


Theorem cardsucinf

Description: The cardinality of the successor of an infinite ordinal. (Contributed by Mario Carneiro, 11-Jan-2013)

Ref Expression
Assertion cardsucinf ( ( 𝐴 ∈ On ∧ ω ⊆ 𝐴 ) → ( card ‘ suc 𝐴 ) = ( card ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 infensuc ( ( 𝐴 ∈ On ∧ ω ⊆ 𝐴 ) → 𝐴 ≈ suc 𝐴 )
2 carden2b ( 𝐴 ≈ suc 𝐴 → ( card ‘ 𝐴 ) = ( card ‘ suc 𝐴 ) )
3 1 2 syl ( ( 𝐴 ∈ On ∧ ω ⊆ 𝐴 ) → ( card ‘ 𝐴 ) = ( card ‘ suc 𝐴 ) )
4 3 eqcomd ( ( 𝐴 ∈ On ∧ ω ⊆ 𝐴 ) → ( card ‘ suc 𝐴 ) = ( card ‘ 𝐴 ) )