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	⊢ ( 𝐴 ∈ dom card ↔ ( card ‘ 𝐴 ) ≈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		cardid2	⊢ ( 𝐴 ∈ dom card → ( card ‘ 𝐴 ) ≈ 𝐴 )
2		cardon	⊢ ( card ‘ 𝐴 ) ∈ On
3		isnumi	⊢ ( ( ( card ‘ 𝐴 ) ∈ On ∧ ( card ‘ 𝐴 ) ≈ 𝐴 ) → 𝐴 ∈ dom card )
4	2 3	mpan	⊢ ( ( card ‘ 𝐴 ) ≈ 𝐴 → 𝐴 ∈ dom card )
5	1 4	impbii	⊢ ( 𝐴 ∈ dom card ↔ ( card ‘ 𝐴 ) ≈ 𝐴 )