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\in \mathrm{dom}\mathrm{card}\leftrightarrow \mathrm{card}\left(A\right)\approx A$$

Proof

Step	Hyp	Ref	Expression
1		cardid2	$$⊢A\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left(A\right)\approx A$$
2		cardon	$$⊢\mathrm{card}\left(A\right)\in \mathrm{On}$$
3		isnumi	$$⊢\left(\mathrm{card}\left(A\right)\in \mathrm{On}\wedge \mathrm{card}\left(A\right)\approx A\right)\to A\in \mathrm{dom}\mathrm{card}$$
4	2 3	mpan	$$⊢\mathrm{card}\left(A\right)\approx A\to A\in \mathrm{dom}\mathrm{card}$$
5	1 4	impbii	$$⊢A\in \mathrm{dom}\mathrm{card}\leftrightarrow \mathrm{card}\left(A\right)\approx A$$