Theorem fineqv

Description: If the Axiom of Infinity is denied, then all sets are finite (which implies the Axiom of Choice). (Contributed by Mario Carneiro, 20-Jan-2013) (Revised by Mario Carneiro, 3-Jan-2015)

	Ref	Expression
Assertion	fineqv	$$⊢\neg \mathrm{\omega }\in \mathrm{V}\leftrightarrow \mathrm{Fin}=\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		ssv	$$⊢\mathrm{Fin}\subseteq \mathrm{V}$$
2	1	a1i	$$⊢\neg \mathrm{\omega }\in \mathrm{V}\to \mathrm{Fin}\subseteq \mathrm{V}$$
3		vex	$$⊢a\in \mathrm{V}$$
4		fineqvlem	$$⊢\left(a\in \mathrm{V}\wedge \neg a\in \mathrm{Fin}\right)\to \mathrm{\omega }\preccurlyeq 𝒫𝒫a$$
5	3 4	mpan	$$⊢\neg a\in \mathrm{Fin}\to \mathrm{\omega }\preccurlyeq 𝒫𝒫a$$
6		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
7	6	brrelex1i	$$⊢\mathrm{\omega }\preccurlyeq 𝒫𝒫a\to \mathrm{\omega }\in \mathrm{V}$$
8	5 7	syl	$$⊢\neg a\in \mathrm{Fin}\to \mathrm{\omega }\in \mathrm{V}$$
9	8	con1i	$$⊢\neg \mathrm{\omega }\in \mathrm{V}\to a\in \mathrm{Fin}$$
10	9	a1d	$$⊢\neg \mathrm{\omega }\in \mathrm{V}\to \left(a\in \mathrm{V}\to a\in \mathrm{Fin}\right)$$
11	10	ssrdv	$$⊢\neg \mathrm{\omega }\in \mathrm{V}\to \mathrm{V}\subseteq \mathrm{Fin}$$
12	2 11	eqssd	$$⊢\neg \mathrm{\omega }\in \mathrm{V}\to \mathrm{Fin}=\mathrm{V}$$
13		ominf	$$⊢\neg \mathrm{\omega }\in \mathrm{Fin}$$
14		eleq2	$$⊢\mathrm{Fin}=\mathrm{V}\to \left(\mathrm{\omega }\in \mathrm{Fin}\leftrightarrow \mathrm{\omega }\in \mathrm{V}\right)$$
15	13 14	mtbii	$$⊢\mathrm{Fin}=\mathrm{V}\to \neg \mathrm{\omega }\in \mathrm{V}$$
16	12 15	impbii	$$⊢\neg \mathrm{\omega }\in \mathrm{V}\leftrightarrow \mathrm{Fin}=\mathrm{V}$$