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