Metamath Proof Explorer

Theorem ondomen

Description: If a set is dominated by an ordinal, then it is numerable. (Contributed by Mario Carneiro, 5-Jan-2013)

Ref Expression
Assertion ondomen ⊢ A ∈ On ∧ B ≼ A → B ∈ dom ⁡ card

Proof

Step Hyp Ref Expression
1 breq2 ⊢ x = A → B ≼ x ↔ B ≼ A
2 1 rspcev ⊢ A ∈ On ∧ B ≼ A → ∃ x ∈ On B ≼ x
3 ac10ct ⊢ ∃ x ∈ On B ≼ x → ∃ r r We B
4 2 3 syl ⊢ A ∈ On ∧ B ≼ A → ∃ r r We B
5 ween ⊢ B ∈ dom ⁡ card ↔ ∃ r r We B
6 4 5 sylibr ⊢ A ∈ On ∧ B ≼ A → B ∈ dom ⁡ card