Theorem infinf

Description: Equivalence between two infiniteness criteria for sets. (Contributed by David Moews, 1-May-2017)

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

Proof

Step	Hyp	Ref	Expression
1		isfinite	$$⊢A\in \mathrm{Fin}\leftrightarrow A\prec \mathrm{\omega }$$
2	1	notbii	$$⊢\neg A\in \mathrm{Fin}\leftrightarrow \neg A\prec \mathrm{\omega }$$
3		omex	$$⊢\mathrm{\omega }\in \mathrm{V}$$
4		domtri	$$⊢\left(\mathrm{\omega }\in \mathrm{V}\wedge A\in B\right)\to \left(\mathrm{\omega }\preccurlyeq A\leftrightarrow \neg A\prec \mathrm{\omega }\right)$$
5	3 4	mpan	$$⊢A\in B\to \left(\mathrm{\omega }\preccurlyeq A\leftrightarrow \neg A\prec \mathrm{\omega }\right)$$
6	2 5	bitr4id	$$⊢A\in B\to \left(\neg A\in \mathrm{Fin}\leftrightarrow \mathrm{\omega }\preccurlyeq A\right)$$