Theorem isfin32i

Description: One half of isfin3-2 . (Contributed by Mario Carneiro, 3-Jun-2015)

	Ref	Expression
Assertion	isfin32i	$$⊢A\in {\mathrm{Fin}}^{\mathrm{III}}\to \neg \mathrm{\omega }{\preccurlyeq }^{*}A$$

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		relwdom	$$⊢\mathrm{Rel}{\preccurlyeq }^{*}$$
5	4	brrelex1i	$$⊢\mathrm{\omega }{\preccurlyeq }^{*}A\to \mathrm{\omega }\in \mathrm{V}$$
6		canth2g	$$⊢\mathrm{\omega }\in \mathrm{V}\to \mathrm{\omega }\prec 𝒫\mathrm{\omega }$$
7		sdomdom	$$⊢\mathrm{\omega }\prec 𝒫\mathrm{\omega }\to \mathrm{\omega }\preccurlyeq 𝒫\mathrm{\omega }$$
8	5 6 7	3syl	$$⊢\mathrm{\omega }{\preccurlyeq }^{*}A\to \mathrm{\omega }\preccurlyeq 𝒫\mathrm{\omega }$$
9		wdompwdom	$$⊢\mathrm{\omega }{\preccurlyeq }^{*}A\to 𝒫\mathrm{\omega }\preccurlyeq 𝒫A$$
10		domtr	$$⊢\left(\mathrm{\omega }\preccurlyeq 𝒫\mathrm{\omega }\wedge 𝒫\mathrm{\omega }\preccurlyeq 𝒫A\right)\to \mathrm{\omega }\preccurlyeq 𝒫A$$
11	8 9 10	syl2anc	$$⊢\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$$