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

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 ⊢ ( 𝐴 ≼ ω → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≼ ω )