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