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
|- ( ( A e. On /\ _om C_ A ) -> ( card ` suc A ) = ( card ` A ) )

Proof

Step Hyp Ref Expression
1 infensuc
 |-  ( ( A e. On /\ _om C_ A ) -> A ~~ suc A )
2 carden2b
 |-  ( A ~~ suc A -> ( card ` A ) = ( card ` suc A ) )
3 1 2 syl
 |-  ( ( A e. On /\ _om C_ A ) -> ( card ` A ) = ( card ` suc A ) )
4 3 eqcomd
 |-  ( ( A e. On /\ _om C_ A ) -> ( card ` suc A ) = ( card ` A ) )