Metamath Proof Explorer


Theorem fimact

Description: The image by a function of a countable set is countable. (Contributed by Thierry Arnoux, 27-Mar-2018)

Ref Expression
Assertion fimact ( ( 𝐴 ≼ ω ∧ Fun 𝐹 ) → ( 𝐹𝐴 ) ≼ ω )

Proof

Step Hyp Ref Expression
1 ctex ( 𝐴 ≼ ω → 𝐴 ∈ V )
2 imadomg ( 𝐴 ∈ V → ( Fun 𝐹 → ( 𝐹𝐴 ) ≼ 𝐴 ) )
3 2 imp ( ( 𝐴 ∈ V ∧ Fun 𝐹 ) → ( 𝐹𝐴 ) ≼ 𝐴 )
4 1 3 sylan ( ( 𝐴 ≼ ω ∧ Fun 𝐹 ) → ( 𝐹𝐴 ) ≼ 𝐴 )
5 simpl ( ( 𝐴 ≼ ω ∧ Fun 𝐹 ) → 𝐴 ≼ ω )
6 domtr ( ( ( 𝐹𝐴 ) ≼ 𝐴𝐴 ≼ ω ) → ( 𝐹𝐴 ) ≼ ω )
7 4 5 6 syl2anc ( ( 𝐴 ≼ ω ∧ Fun 𝐹 ) → ( 𝐹𝐴 ) ≼ ω )