Theorem fin41

Description: Under countable choice, the IV-finite sets (Dedekind-finite) coincide with I-finite (finite in the usual sense) sets. (Contributed by Mario Carneiro, 16-May-2015)

	Ref	Expression
Assertion	fin41	$$⊢{\mathrm{Fin}}^{\mathrm{IV}}=\mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢x\in \mathrm{V}$$
2	1	domtriom	$$⊢\mathrm{\omega }\preccurlyeq x\leftrightarrow \neg x\prec \mathrm{\omega }$$
3	2	con2bii	$$⊢x\prec \mathrm{\omega }\leftrightarrow \neg \mathrm{\omega }\preccurlyeq x$$
4		isfinite	$$⊢x\in \mathrm{Fin}\leftrightarrow x\prec \mathrm{\omega }$$
5		isfin4-2	$$⊢x\in \mathrm{V}\to \left(x\in {\mathrm{Fin}}^{\mathrm{IV}}\leftrightarrow \neg \mathrm{\omega }\preccurlyeq x\right)$$
6	5	elv	$$⊢x\in {\mathrm{Fin}}^{\mathrm{IV}}\leftrightarrow \neg \mathrm{\omega }\preccurlyeq x$$
7	3 4 6	3bitr4ri	$$⊢x\in {\mathrm{Fin}}^{\mathrm{IV}}\leftrightarrow x\in \mathrm{Fin}$$
8	7	eqriv	$$⊢{\mathrm{Fin}}^{\mathrm{IV}}=\mathrm{Fin}$$