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