Metamath Proof Explorer


Theorem isnum3

Description: A set is numerable iff it is equinumerous with its cardinal. (Contributed by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion isnum3
|- ( A e. dom card <-> ( card ` A ) ~~ A )

Proof

Step Hyp Ref Expression
1 cardid2
 |-  ( A e. dom card -> ( card ` A ) ~~ A )
2 cardon
 |-  ( card ` A ) e. On
3 isnumi
 |-  ( ( ( card ` A ) e. On /\ ( card ` A ) ~~ A ) -> A e. dom card )
4 2 3 mpan
 |-  ( ( card ` A ) ~~ A -> A e. dom card )
5 1 4 impbii
 |-  ( A e. dom card <-> ( card ` A ) ~~ A )