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 ( 𝐴 ∈ 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 ‘ 𝐴 ) ≈ 𝐴 )