Metamath Proof Explorer

Theorem carden2

Description: Two numerable sets are equinumerous iff their cardinal numbers are equal. Unlike carden , the Axiom of Choice is not required. (Contributed by Mario Carneiro, 22-Sep-2013)

Ref Expression
Assertion carden2 
|- ( ( A e. dom card /\ B e. dom card ) -> ( ( card ` A ) = ( card ` B ) <-> A ~~ B ) )

Proof

Step Hyp Ref Expression
1 carddom2 
 |-  ( ( A e. dom card /\ B e. dom card ) -> ( ( card ` A ) C_ ( card ` B ) <-> A ~<_ B ) )
2 carddom2 
 |-  ( ( B e. dom card /\ A e. dom card ) -> ( ( card ` B ) C_ ( card ` A ) <-> B ~<_ A ) )
3 2 ancoms 
 |-  ( ( A e. dom card /\ B e. dom card ) -> ( ( card ` B ) C_ ( card ` A ) <-> B ~<_ A ) )
4 1 3 anbi12d 
 |-  ( ( A e. dom card /\ B e. dom card ) -> ( ( ( card ` A ) C_ ( card ` B ) /\ ( card ` B ) C_ ( card ` A ) ) <-> ( A ~<_ B /\ B ~<_ A ) ) )
5 eqss 
 |-  ( ( card ` A ) = ( card ` B ) <-> ( ( card ` A ) C_ ( card ` B ) /\ ( card ` B ) C_ ( card ` A ) ) )
6 5 bicomi 
 |-  ( ( ( card ` A ) C_ ( card ` B ) /\ ( card ` B ) C_ ( card ` A ) ) <-> ( card ` A ) = ( card ` B ) )
7 sbthb 
 |-  ( ( A ~<_ B /\ B ~<_ A ) <-> A ~~ B )
8 4 6 7 3bitr3g 
 |-  ( ( A e. dom card /\ B e. dom card ) -> ( ( card ` A ) = ( card ` B ) <-> A ~~ B ) )