Theorem dmct

Description: The domain of a countable set is countable. (Contributed by Thierry Arnoux, 29-Dec-2016)

	Ref	Expression
Assertion	dmct	$$⊢A\preccurlyeq \mathrm{\omega }\to \mathrm{dom}A\preccurlyeq \mathrm{\omega }$$

Proof

Step	Hyp	Ref	Expression
1		dmresv	$$⊢\mathrm{dom}\left({A\upharpoonright }_{\mathrm{V}}\right)=\mathrm{dom}A$$
2		resss	$$⊢{A\upharpoonright }_{\mathrm{V}}\subseteq A$$
3		ctex	$$⊢A\preccurlyeq \mathrm{\omega }\to A\in \mathrm{V}$$
4		ssexg	$$⊢\left({A\upharpoonright }_{\mathrm{V}}\subseteq A\wedge A\in \mathrm{V}\right)\to {A\upharpoonright }_{\mathrm{V}}\in \mathrm{V}$$
5	2 3 4	sylancr	$$⊢A\preccurlyeq \mathrm{\omega }\to {A\upharpoonright }_{\mathrm{V}}\in \mathrm{V}$$
6		fvex	$$⊢1^{st}\left(x\right)\in \mathrm{V}$$
7		eqid	$$⊢\left(x\in \left({A\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right)=\left(x\in \left({A\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right)$$
8	6 7	fnmpti	$$⊢\left(x\in \left({A\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right)Fn\left({A\upharpoonright }_{\mathrm{V}}\right)$$
9		dffn4	$$⊢\left(x\in \left({A\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right)Fn\left({A\upharpoonright }_{\mathrm{V}}\right)\leftrightarrow \left(x\in \left({A\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right):{A\upharpoonright }_{\mathrm{V}}\underset{onto}{⟶}\mathrm{ran}\left(x\in \left({A\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right)$$
10	8 9	mpbi	$$⊢\left(x\in \left({A\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right):{A\upharpoonright }_{\mathrm{V}}\underset{onto}{⟶}\mathrm{ran}\left(x\in \left({A\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right)$$
11		relres	$$⊢\mathrm{Rel}\left({A\upharpoonright }_{\mathrm{V}}\right)$$
12		reldm	$$⊢\mathrm{Rel}\left({A\upharpoonright }_{\mathrm{V}}\right)\to \mathrm{dom}\left({A\upharpoonright }_{\mathrm{V}}\right)=\mathrm{ran}\left(x\in \left({A\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right)$$
13		foeq3	$$⊢\mathrm{dom}\left({A\upharpoonright }_{\mathrm{V}}\right)=\mathrm{ran}\left(x\in \left({A\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right)\to \left(\left(x\in \left({A\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right):{A\upharpoonright }_{\mathrm{V}}\underset{onto}{⟶}\mathrm{dom}\left({A\upharpoonright }_{\mathrm{V}}\right)\leftrightarrow \left(x\in \left({A\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right):{A\upharpoonright }_{\mathrm{V}}\underset{onto}{⟶}\mathrm{ran}\left(x\in \left({A\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right)\right)$$
14	11 12 13	mp2b	$$⊢\left(x\in \left({A\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right):{A\upharpoonright }_{\mathrm{V}}\underset{onto}{⟶}\mathrm{dom}\left({A\upharpoonright }_{\mathrm{V}}\right)\leftrightarrow \left(x\in \left({A\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right):{A\upharpoonright }_{\mathrm{V}}\underset{onto}{⟶}\mathrm{ran}\left(x\in \left({A\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right)$$
15	10 14	mpbir	$$⊢\left(x\in \left({A\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right):{A\upharpoonright }_{\mathrm{V}}\underset{onto}{⟶}\mathrm{dom}\left({A\upharpoonright }_{\mathrm{V}}\right)$$
16		fodomg	$$⊢{A\upharpoonright }_{\mathrm{V}}\in \mathrm{V}\to \left(\left(x\in \left({A\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right):{A\upharpoonright }_{\mathrm{V}}\underset{onto}{⟶}\mathrm{dom}\left({A\upharpoonright }_{\mathrm{V}}\right)\to \mathrm{dom}\left({A\upharpoonright }_{\mathrm{V}}\right)\preccurlyeq \left({A\upharpoonright }_{\mathrm{V}}\right)\right)$$
17	5 15 16	mpisyl	$$⊢A\preccurlyeq \mathrm{\omega }\to \mathrm{dom}\left({A\upharpoonright }_{\mathrm{V}}\right)\preccurlyeq \left({A\upharpoonright }_{\mathrm{V}}\right)$$
18		ssdomg	$$⊢A\in \mathrm{V}\to \left({A\upharpoonright }_{\mathrm{V}}\subseteq A\to \left({A\upharpoonright }_{\mathrm{V}}\right)\preccurlyeq A\right)$$
19	3 2 18	mpisyl	$$⊢A\preccurlyeq \mathrm{\omega }\to \left({A\upharpoonright }_{\mathrm{V}}\right)\preccurlyeq A$$
20		domtr	$$⊢\left(\left({A\upharpoonright }_{\mathrm{V}}\right)\preccurlyeq A\wedge A\preccurlyeq \mathrm{\omega }\right)\to \left({A\upharpoonright }_{\mathrm{V}}\right)\preccurlyeq \mathrm{\omega }$$
21	19 20	mpancom	$$⊢A\preccurlyeq \mathrm{\omega }\to \left({A\upharpoonright }_{\mathrm{V}}\right)\preccurlyeq \mathrm{\omega }$$
22		domtr	$$⊢\left(\mathrm{dom}\left({A\upharpoonright }_{\mathrm{V}}\right)\preccurlyeq \left({A\upharpoonright }_{\mathrm{V}}\right)\wedge \left({A\upharpoonright }_{\mathrm{V}}\right)\preccurlyeq \mathrm{\omega }\right)\to \mathrm{dom}\left({A\upharpoonright }_{\mathrm{V}}\right)\preccurlyeq \mathrm{\omega }$$
23	17 21 22	syl2anc	$$⊢A\preccurlyeq \mathrm{\omega }\to \mathrm{dom}\left({A\upharpoonright }_{\mathrm{V}}\right)\preccurlyeq \mathrm{\omega }$$
24	1 23	eqbrtrrid	$$⊢A\preccurlyeq \mathrm{\omega }\to \mathrm{dom}A\preccurlyeq \mathrm{\omega }$$