Metamath Proof Explorer

Theorem numdom

Description: A set dominated by a numerable set is numerable. (Contributed by Mario Carneiro, 28-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 cardon ⊢ card ⁡ A ∈ On
2 cardid2 ⊢ A ∈ dom ⁡ card → card ⁡ A ≈ A
3 domen2 ⊢ card ⁡ A ≈ A → B ≼ card ⁡ A ↔ B ≼ A
4 2 3 syl ⊢ A ∈ dom ⁡ card → B ≼ card ⁡ A ↔ B ≼ A
5 4 biimpar ⊢ A ∈ dom ⁡ card ∧ B ≼ A → B ≼ card ⁡ A
6 ondomen ⊢ card ⁡ A ∈ On ∧ B ≼ card ⁡ A → B ∈ dom ⁡ card
7 1 5 6 sylancr ⊢ A ∈ dom ⁡ card ∧ B ≼ A → B ∈ dom ⁡ card