Theorem fonum

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

	Ref	Expression
Assertion	fonum	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → 𝐵 ∈ dom card )

Proof

Step	Hyp	Ref	Expression
1		fodomnum	⊢ ( 𝐴 ∈ dom card → ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐵 ≼ 𝐴 ) )
2	1	imp	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → 𝐵 ≼ 𝐴 )
3		numdom	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ≼ 𝐴 ) → 𝐵 ∈ dom card )
4	2 3	syldan	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → 𝐵 ∈ dom card )