Theorem fin34

Description: Every III-finite set is IV-finite. (Contributed by Stefan O'Rear, 30-Oct-2014)

	Ref	Expression
Assertion	fin34	$$⊢A\in {\mathrm{Fin}}^{\mathrm{III}}\to A\in {\mathrm{Fin}}^{\mathrm{IV}}$$

Proof

Step	Hyp	Ref	Expression
1		isfin3	$$⊢A\in {\mathrm{Fin}}^{\mathrm{III}}\leftrightarrow 𝒫A\in {\mathrm{Fin}}^{\mathrm{IV}}$$
2		isfin4-2	$$⊢𝒫A\in {\mathrm{Fin}}^{\mathrm{IV}}\to \left(𝒫A\in {\mathrm{Fin}}^{\mathrm{IV}}\leftrightarrow \neg \mathrm{\omega }\preccurlyeq 𝒫A\right)$$
3	2	ibi	$$⊢𝒫A\in {\mathrm{Fin}}^{\mathrm{IV}}\to \neg \mathrm{\omega }\preccurlyeq 𝒫A$$
4		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
5	4	brrelex2i	$$⊢\mathrm{\omega }\preccurlyeq A\to A\in \mathrm{V}$$
6		canth2g	$$⊢A\in \mathrm{V}\to A\prec 𝒫A$$
7	5 6	syl	$$⊢\mathrm{\omega }\preccurlyeq A\to A\prec 𝒫A$$
8		domsdomtr	$$⊢\left(\mathrm{\omega }\preccurlyeq A\wedge A\prec 𝒫A\right)\to \mathrm{\omega }\prec 𝒫A$$
9	7 8	mpdan	$$⊢\mathrm{\omega }\preccurlyeq A\to \mathrm{\omega }\prec 𝒫A$$
10		sdomdom	$$⊢\mathrm{\omega }\prec 𝒫A\to \mathrm{\omega }\preccurlyeq 𝒫A$$
11	9 10	syl	$$⊢\mathrm{\omega }\preccurlyeq A\to \mathrm{\omega }\preccurlyeq 𝒫A$$
12	3 11	nsyl	$$⊢𝒫A\in {\mathrm{Fin}}^{\mathrm{IV}}\to \neg \mathrm{\omega }\preccurlyeq A$$
13	1 12	sylbi	$$⊢A\in {\mathrm{Fin}}^{\mathrm{III}}\to \neg \mathrm{\omega }\preccurlyeq A$$
14		isfin4-2	$$⊢A\in {\mathrm{Fin}}^{\mathrm{III}}\to \left(A\in {\mathrm{Fin}}^{\mathrm{IV}}\leftrightarrow \neg \mathrm{\omega }\preccurlyeq A\right)$$
15	13 14	mpbird	$$⊢A\in {\mathrm{Fin}}^{\mathrm{III}}\to A\in {\mathrm{Fin}}^{\mathrm{IV}}$$