Metamath Proof Explorer

Theorem numwdom

Description: A surjection maps numerable sets to numerable sets. (Contributed by Mario Carneiro, 27-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 brwdomi ⊢ B ≼ * A → B = ∅ ∨ ∃ f f : A ⟶ onto B
2 simpr ⊢ A ∈ dom ⁡ card ∧ B = ∅ → B = ∅
3 0fin ⊢ ∅ ∈ Fin
4 finnum ⊢ ∅ ∈ Fin → ∅ ∈ dom ⁡ card
5 3 4 ax-mp ⊢ ∅ ∈ dom ⁡ card
6 2 5 eqeltrdi ⊢ A ∈ dom ⁡ card ∧ B = ∅ → B ∈ dom ⁡ card
7 fonum ⊢ A ∈ dom ⁡ card ∧ f : A ⟶ onto B → B ∈ dom ⁡ card
8 7 ex ⊢ A ∈ dom ⁡ card → f : A ⟶ onto B → B ∈ dom ⁡ card
9 8 exlimdv ⊢ A ∈ dom ⁡ card → ∃ f f : A ⟶ onto B → B ∈ dom ⁡ card
10 9 imp ⊢ A ∈ dom ⁡ card ∧ ∃ f f : A ⟶ onto B → B ∈ dom ⁡ card
11 6 10 jaodan ⊢ A ∈ dom ⁡ card ∧ B = ∅ ∨ ∃ f f : A ⟶ onto B → B ∈ dom ⁡ card
12 1 11 sylan2 ⊢ A ∈ dom ⁡ card ∧ B ≼ * A → B ∈ dom ⁡ card