Metamath Proof Explorer


Theorem mptct

Description: A countable mapping set is countable. (Contributed by Thierry Arnoux, 29-Dec-2016)

Ref Expression
Assertion mptct ( 𝐴 ≼ ω → ( 𝑥𝐴𝐵 ) ≼ ω )

Proof

Step Hyp Ref Expression
1 funmpt Fun ( 𝑥𝐴𝐵 )
2 ctex ( 𝐴 ≼ ω → 𝐴 ∈ V )
3 eqid ( 𝑥𝐴𝐵 ) = ( 𝑥𝐴𝐵 )
4 3 dmmptss dom ( 𝑥𝐴𝐵 ) ⊆ 𝐴
5 ssdomg ( 𝐴 ∈ V → ( dom ( 𝑥𝐴𝐵 ) ⊆ 𝐴 → dom ( 𝑥𝐴𝐵 ) ≼ 𝐴 ) )
6 2 4 5 mpisyl ( 𝐴 ≼ ω → dom ( 𝑥𝐴𝐵 ) ≼ 𝐴 )
7 domtr ( ( dom ( 𝑥𝐴𝐵 ) ≼ 𝐴𝐴 ≼ ω ) → dom ( 𝑥𝐴𝐵 ) ≼ ω )
8 6 7 mpancom ( 𝐴 ≼ ω → dom ( 𝑥𝐴𝐵 ) ≼ ω )
9 funfn ( Fun ( 𝑥𝐴𝐵 ) ↔ ( 𝑥𝐴𝐵 ) Fn dom ( 𝑥𝐴𝐵 ) )
10 fnct ( ( ( 𝑥𝐴𝐵 ) Fn dom ( 𝑥𝐴𝐵 ) ∧ dom ( 𝑥𝐴𝐵 ) ≼ ω ) → ( 𝑥𝐴𝐵 ) ≼ ω )
11 9 10 sylanb ( ( Fun ( 𝑥𝐴𝐵 ) ∧ dom ( 𝑥𝐴𝐵 ) ≼ ω ) → ( 𝑥𝐴𝐵 ) ≼ ω )
12 1 8 11 sylancr ( 𝐴 ≼ ω → ( 𝑥𝐴𝐵 ) ≼ ω )