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 ) )