Theorem domtriom

Description: Trichotomy of equinumerosity for _om , proven using countable choice. Equivalently, all Dedekind-finite sets (as in isfin4-2 ) are finite in the usual sense and conversely. (Contributed by Mario Carneiro, 9-Feb-2013)

	Ref	Expression
Hypothesis	domtriom.1	$$⊢A\in \mathrm{V}$$
Assertion	domtriom	$$⊢\mathrm{\omega }\preccurlyeq A\leftrightarrow \neg A\prec \mathrm{\omega }$$

Proof

Step	Hyp	Ref	Expression
1		domtriom.1	$$⊢A\in \mathrm{V}$$
2		domnsym	$$⊢\mathrm{\omega }\preccurlyeq A\to \neg A\prec \mathrm{\omega }$$
3		isfinite	$$⊢A\in \mathrm{Fin}\leftrightarrow A\prec \mathrm{\omega }$$
4		eqid	$$⊢\left\{y|\left(y\subseteq A\wedge y\approx 𝒫n\right)\right\}=\left\{y|\left(y\subseteq A\wedge y\approx 𝒫n\right)\right\}$$
5		fveq2	$$⊢m=n\to b\left(m\right)=b\left(n\right)$$
6		fveq2	$$⊢j=k\to b\left(j\right)=b\left(k\right)$$
7	6	cbviunv	$$⊢\bigcup _{j\in m}b\left(j\right)=\bigcup _{k\in m}b\left(k\right)$$
8		iuneq1	$$⊢m=n\to \bigcup _{k\in m}b\left(k\right)=\bigcup _{k\in n}b\left(k\right)$$
9	7 8	eqtrid	$$⊢m=n\to \bigcup _{j\in m}b\left(j\right)=\bigcup _{k\in n}b\left(k\right)$$
10	5 9	difeq12d	$$⊢m=n\to b\left(m\right)\setminus \bigcup _{j\in m}b\left(j\right)=b\left(n\right)\setminus \bigcup _{k\in n}b\left(k\right)$$
11	10	cbvmptv	$$⊢\left(m\in \mathrm{\omega }⟼b\left(m\right)\setminus \bigcup _{j\in m}b\left(j\right)\right)=\left(n\in \mathrm{\omega }⟼b\left(n\right)\setminus \bigcup _{k\in n}b\left(k\right)\right)$$
12	1 4 11	domtriomlem	$$⊢\neg A\in \mathrm{Fin}\to \mathrm{\omega }\preccurlyeq A$$
13	3 12	sylnbir	$$⊢\neg A\prec \mathrm{\omega }\to \mathrm{\omega }\preccurlyeq A$$
14	2 13	impbii	$$⊢\mathrm{\omega }\preccurlyeq A\leftrightarrow \neg A\prec \mathrm{\omega }$$