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 ( ( 𝐴 ∈ On ∧ 𝐴𝐵 ) → 𝐵 ∈ dom card )

Proof

Step Hyp Ref Expression
1 breq1 ( 𝑥 = 𝐴 → ( 𝑥𝐵𝐴𝐵 ) )
2 1 rspcev ( ( 𝐴 ∈ On ∧ 𝐴𝐵 ) → ∃ 𝑥 ∈ On 𝑥𝐵 )
3 isnum2 ( 𝐵 ∈ dom card ↔ ∃ 𝑥 ∈ On 𝑥𝐵 )
4 2 3 sylibr ( ( 𝐴 ∈ On ∧ 𝐴𝐵 ) → 𝐵 ∈ dom card )