This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isnumi

Description: A set equinumerous to an ordinal is numerable. (Contributed by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion isnumi ⊢ A ∈ On ∧ A ≈ B → B ∈ dom ⁡ card

Proof

Step Hyp Ref Expression
1 breq1 ⊢ x = A → x ≈ B ↔ A ≈ B
2 1 rspcev ⊢ A ∈ On ∧ A ≈ B → ∃ x ∈ On x ≈ B
3 isnum2 ⊢ B ∈ dom ⁡ card ↔ ∃ x ∈ On x ≈ B
4 2 3 sylibr ⊢ A ∈ On ∧ A ≈ B → B ∈ dom ⁡ card