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 )