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

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

Proof

Step Hyp Ref Expression
1 brwdomi ⊢ ( 𝐵 ≼* 𝐴 → ( 𝐵 = ∅ ∨ ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 ) )
2 simpr ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 = ∅ ) → 𝐵 = ∅ )
3 0fi ⊢ ∅ ∈ Fin
4 finnum ⊢ ( ∅ ∈ Fin → ∅ ∈ dom card )
5 3 4 ax-mp ⊢ ∅ ∈ dom card
6 2 5 eqeltrdi ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 = ∅ ) → 𝐵 ∈ dom card )
7 fonum ⊢ ( ( 𝐴 ∈ dom card ∧ 𝑓 : 𝐴 –onto→ 𝐵 ) → 𝐵 ∈ dom card )
8 7 ex ⊢ ( 𝐴 ∈ dom card → ( 𝑓 : 𝐴 –onto→ 𝐵 → 𝐵 ∈ dom card ) )
9 8 exlimdv ⊢ ( 𝐴 ∈ dom card → ( ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 → 𝐵 ∈ dom card ) )
10 9 imp ⊢ ( ( 𝐴 ∈ dom card ∧ ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 ) → 𝐵 ∈ dom card )
11 6 10 jaodan ⊢ ( ( 𝐴 ∈ dom card ∧ ( 𝐵 = ∅ ∨ ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 ) ) → 𝐵 ∈ dom card )
12 1 11 sylan2 ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ≼* 𝐴 ) → 𝐵 ∈ dom card )