Metamath Proof Explorer

Theorem mptct

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

Ref Expression
Assertion mptct ⊢ A ≼ ω → x ∈ A ⟼ B ≼ ω

Proof

Step Hyp Ref Expression
1 funmpt ⊢ Fun ⁡ x ∈ A ⟼ B
2 ctex ⊢ A ≼ ω → A ∈ V
3 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
4 3 dmmptss ⊢ dom ⁡ x ∈ A ⟼ B ⊆ A
5 ssdomg ⊢ A ∈ V → dom ⁡ x ∈ A ⟼ B ⊆ A → dom ⁡ x ∈ A ⟼ B ≼ A
6 2 4 5 mpisyl ⊢ A ≼ ω → dom ⁡ x ∈ A ⟼ B ≼ A
7 domtr ⊢ dom ⁡ x ∈ A ⟼ B ≼ A ∧ A ≼ ω → dom ⁡ x ∈ A ⟼ B ≼ ω
8 6 7 mpancom ⊢ A ≼ ω → dom ⁡ x ∈ A ⟼ B ≼ ω
9 funfn ⊢ Fun ⁡ x ∈ A ⟼ B ↔ x ∈ A ⟼ B Fn dom ⁡ x ∈ A ⟼ B
10 fnct ⊢ x ∈ A ⟼ B Fn dom ⁡ x ∈ A ⟼ B ∧ dom ⁡ x ∈ A ⟼ B ≼ ω → x ∈ A ⟼ B ≼ ω
11 9 10 sylanb ⊢ Fun ⁡ x ∈ A ⟼ B ∧ dom ⁡ x ∈ A ⟼ B ≼ ω → x ∈ A ⟼ B ≼ ω
12 1 8 11 sylancr ⊢ A ≼ ω → x ∈ A ⟼ B ≼ ω