Theorem mptct

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

	Ref	Expression
Assertion	mptct	$$⊢A\preccurlyeq \mathrm{\omega }\to \left(x\in A⟼B\right)\preccurlyeq \mathrm{\omega }$$

Proof

Step	Hyp	Ref	Expression
1		funmpt	$$⊢\mathrm{Fun}\left(x\in A⟼B\right)$$
2		ctex	$$⊢A\preccurlyeq \mathrm{\omega }\to A\in \mathrm{V}$$
3		eqid	$$⊢\left(x\in A⟼B\right)=\left(x\in A⟼B\right)$$
4	3	dmmptss	$$⊢\mathrm{dom}\left(x\in A⟼B\right)\subseteq A$$
5		ssdomg	$$⊢A\in \mathrm{V}\to \left(\mathrm{dom}\left(x\in A⟼B\right)\subseteq A\to \mathrm{dom}\left(x\in A⟼B\right)\preccurlyeq A\right)$$
6	2 4 5	mpisyl	$$⊢A\preccurlyeq \mathrm{\omega }\to \mathrm{dom}\left(x\in A⟼B\right)\preccurlyeq A$$
7		domtr	$$⊢\left(\mathrm{dom}\left(x\in A⟼B\right)\preccurlyeq A\wedge A\preccurlyeq \mathrm{\omega }\right)\to \mathrm{dom}\left(x\in A⟼B\right)\preccurlyeq \mathrm{\omega }$$
8	6 7	mpancom	$$⊢A\preccurlyeq \mathrm{\omega }\to \mathrm{dom}\left(x\in A⟼B\right)\preccurlyeq \mathrm{\omega }$$
9		funfn	$$⊢\mathrm{Fun}\left(x\in A⟼B\right)\leftrightarrow \left(x\in A⟼B\right)Fn\mathrm{dom}\left(x\in A⟼B\right)$$
10		fnct	$$⊢\left(\left(x\in A⟼B\right)Fn\mathrm{dom}\left(x\in A⟼B\right)\wedge \mathrm{dom}\left(x\in A⟼B\right)\preccurlyeq \mathrm{\omega }\right)\to \left(x\in A⟼B\right)\preccurlyeq \mathrm{\omega }$$
11	9 10	sylanb	$$⊢\left(\mathrm{Fun}\left(x\in A⟼B\right)\wedge \mathrm{dom}\left(x\in A⟼B\right)\preccurlyeq \mathrm{\omega }\right)\to \left(x\in A⟼B\right)\preccurlyeq \mathrm{\omega }$$
12	1 8 11	sylancr	$$⊢A\preccurlyeq \mathrm{\omega }\to \left(x\in A⟼B\right)\preccurlyeq \mathrm{\omega }$$