Theorem dmct

Description: The domain of a countable set is countable. The proof uses fodomnum rather than fodomg , and so does not require ax-ac . (Contributed by Thierry Arnoux, 29-Dec-2016) (Revised by Vincent Gonzalez, 24-Aug-2026)

	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		omelon	$$⊢\mathrm{\omega }\in \mathrm{On}$$
3	2	a1i	$$⊢A\preccurlyeq \mathrm{\omega }\to \mathrm{\omega }\in \mathrm{On}$$
4		id	$$⊢A\preccurlyeq \mathrm{\omega }\to A\preccurlyeq \mathrm{\omega }$$
5		ondomen	$$⊢\left(\mathrm{\omega }\in \mathrm{On}\wedge A\preccurlyeq \mathrm{\omega }\right)\to A\in \mathrm{dom}\mathrm{card}$$
6	3 4 5	syl2anc	$$⊢A\preccurlyeq \mathrm{\omega }\to A\in \mathrm{dom}\mathrm{card}$$
7		resss	$$⊢{A\upharpoonright }_{\mathrm{V}}\subseteq A$$
8	7	a1i	$$⊢A\preccurlyeq \mathrm{\omega }\to {A\upharpoonright }_{\mathrm{V}}\subseteq A$$
9		ssnum	$$⊢\left(A\in \mathrm{dom}\mathrm{card}\wedge {A\upharpoonright }_{\mathrm{V}}\subseteq A\right)\to {A\upharpoonright }_{\mathrm{V}}\in \mathrm{dom}\mathrm{card}$$
10	6 8 9	syl2anc	$$⊢A\preccurlyeq \mathrm{\omega }\to {A\upharpoonright }_{\mathrm{V}}\in \mathrm{dom}\mathrm{card}$$
11		fvex	$$⊢1^{st}\left(x\right)\in \mathrm{V}$$
12		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)$$
13	11 12	fnmpti	$$⊢\left(x\in \left({A\upharpoonright }_{\mathrm{V}}\right)⟼1^{st}\left(x\right)\right)Fn\left({A\upharpoonright }_{\mathrm{V}}\right)$$
14		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)$$
15	13 14	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)$$
16		relres	$$⊢\mathrm{Rel}\left({A\upharpoonright }_{\mathrm{V}}\right)$$
17		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)$$
18		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)$$
19	16 17 18	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)$$
20	15 19	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)$$
21		fodomnum	$$⊢{A\upharpoonright }_{\mathrm{V}}\in \mathrm{dom}\mathrm{card}\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)$$
22	10 20 21	mpisyl	$$⊢A\preccurlyeq \mathrm{\omega }\to \mathrm{dom}\left({A\upharpoonright }_{\mathrm{V}}\right)\preccurlyeq \left({A\upharpoonright }_{\mathrm{V}}\right)$$
23		ctex	$$⊢A\preccurlyeq \mathrm{\omega }\to A\in \mathrm{V}$$
24		ssdomg	$$⊢A\in \mathrm{V}\to \left({A\upharpoonright }_{\mathrm{V}}\subseteq A\to \left({A\upharpoonright }_{\mathrm{V}}\right)\preccurlyeq A\right)$$
25	23 7 24	mpisyl	$$⊢A\preccurlyeq \mathrm{\omega }\to \left({A\upharpoonright }_{\mathrm{V}}\right)\preccurlyeq A$$
26		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 }$$
27	25 26	mpancom	$$⊢A\preccurlyeq \mathrm{\omega }\to \left({A\upharpoonright }_{\mathrm{V}}\right)\preccurlyeq \mathrm{\omega }$$
28		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 }$$
29	22 27 28	syl2anc	$$⊢A\preccurlyeq \mathrm{\omega }\to \mathrm{dom}\left({A\upharpoonright }_{\mathrm{V}}\right)\preccurlyeq \mathrm{\omega }$$
30	1 29	eqbrtrrid	$$⊢A\preccurlyeq \mathrm{\omega }\to \mathrm{dom}A\preccurlyeq \mathrm{\omega }$$