Theorem infinfnum

Description: Equivalence between two infiniteness criteria for numerable sets. (Contributed by BTernaryTau, 15-Jul-2026)

	Ref	Expression
Assertion	infinfnum	$$⊢A\in \mathrm{dom}\mathrm{card}\to \left(\neg A\in \mathrm{Fin}\leftrightarrow \mathrm{\omega }\preccurlyeq A\right)$$

Proof

Step	Hyp	Ref	Expression
1		isfin4-2	$$⊢A\in \mathrm{dom}\mathrm{card}\to \left(A\in {\mathrm{Fin}}^{\mathrm{IV}}\leftrightarrow \neg \mathrm{\omega }\preccurlyeq A\right)$$
2	1	con2bid	$$⊢A\in \mathrm{dom}\mathrm{card}\to \left(\mathrm{\omega }\preccurlyeq A\leftrightarrow \neg A\in {\mathrm{Fin}}^{\mathrm{IV}}\right)$$
3		fin45	$$⊢A\in {\mathrm{Fin}}^{\mathrm{IV}}\to A\in {\mathrm{Fin}}^{\mathrm{V}}$$
4		fin56	$$⊢A\in {\mathrm{Fin}}^{\mathrm{V}}\to A\in {\mathrm{Fin}}^{\mathrm{VI}}$$
5		fin67	$$⊢A\in {\mathrm{Fin}}^{\mathrm{VI}}\to A\in {\mathrm{Fin}}^{\mathrm{VII}}$$
6	3 4 5	3syl	$$⊢A\in {\mathrm{Fin}}^{\mathrm{IV}}\to A\in {\mathrm{Fin}}^{\mathrm{VII}}$$
7		fin71num	$$⊢A\in \mathrm{dom}\mathrm{card}\to \left(A\in {\mathrm{Fin}}^{\mathrm{VII}}\leftrightarrow A\in \mathrm{Fin}\right)$$
8	6 7	imbitrid	$$⊢A\in \mathrm{dom}\mathrm{card}\to \left(A\in {\mathrm{Fin}}^{\mathrm{IV}}\to A\in \mathrm{Fin}\right)$$
9		fin12	$$⊢A\in \mathrm{Fin}\to A\in {\mathrm{Fin}}^{\mathrm{II}}$$
10		fin23	$$⊢A\in {\mathrm{Fin}}^{\mathrm{II}}\to A\in {\mathrm{Fin}}^{\mathrm{III}}$$
11		fin34	$$⊢A\in {\mathrm{Fin}}^{\mathrm{III}}\to A\in {\mathrm{Fin}}^{\mathrm{IV}}$$
12	9 10 11	3syl	$$⊢A\in \mathrm{Fin}\to A\in {\mathrm{Fin}}^{\mathrm{IV}}$$
13	8 12	impbid1	$$⊢A\in \mathrm{dom}\mathrm{card}\to \left(A\in {\mathrm{Fin}}^{\mathrm{IV}}\leftrightarrow A\in \mathrm{Fin}\right)$$
14	13	notbid	$$⊢A\in \mathrm{dom}\mathrm{card}\to \left(\neg A\in {\mathrm{Fin}}^{\mathrm{IV}}\leftrightarrow \neg A\in \mathrm{Fin}\right)$$
15	2 14	bitr2d	$$⊢A\in \mathrm{dom}\mathrm{card}\to \left(\neg A\in \mathrm{Fin}\leftrightarrow \mathrm{\omega }\preccurlyeq A\right)$$