Theorem fin1a2lem7

Description: Lemma for fin1a2 . Split a III-infinite set in two pieces. (Contributed by Stefan O'Rear, 7-Nov-2014)

	Ref	Expression
Hypotheses	fin1a2lem.b	$$⊢E=\left(x\in \mathrm{\omega }⟼2_{𝑜}{\cdot }_{𝑜}x\right)$$
	fin1a2lem.aa	$$⊢S=\left(x\in \mathrm{On}⟼\mathrm{suc}x\right)$$
Assertion	fin1a2lem7	$$⊢\left(A\in V\wedge \forall y\in 𝒫A\left(y\in {\mathrm{Fin}}^{\mathrm{III}}\vee A\setminus y\in {\mathrm{Fin}}^{\mathrm{III}}\right)\right)\to A\in {\mathrm{Fin}}^{\mathrm{III}}$$

Proof

Step	Hyp	Ref	Expression
1		fin1a2lem.b	$$⊢E=\left(x\in \mathrm{\omega }⟼2_{𝑜}{\cdot }_{𝑜}x\right)$$
2		fin1a2lem.aa	$$⊢S=\left(x\in \mathrm{On}⟼\mathrm{suc}x\right)$$
3		peano1	$$⊢\varnothing \in \mathrm{\omega }$$
4		ne0i	$$⊢\varnothing \in \mathrm{\omega }\to \mathrm{\omega }\ne \varnothing$$
5		brwdomn0	$$⊢\mathrm{\omega }\ne \varnothing \to \left(\mathrm{\omega }{\preccurlyeq }^{*}A\leftrightarrow \exists ff:A\underset{onto}{⟶}\mathrm{\omega }\right)$$
6	3 4 5	mp2b	$$⊢\mathrm{\omega }{\preccurlyeq }^{*}A\leftrightarrow \exists ff:A\underset{onto}{⟶}\mathrm{\omega }$$
7		vex	$$⊢f\in \mathrm{V}$$
8		fof	$$⊢f:A\underset{onto}{⟶}\mathrm{\omega }\to f:A⟶\mathrm{\omega }$$
9		dmfex	$$⊢\left(f\in \mathrm{V}\wedge f:A⟶\mathrm{\omega }\right)\to A\in \mathrm{V}$$
10	7 8 9	sylancr	$$⊢f:A\underset{onto}{⟶}\mathrm{\omega }\to A\in \mathrm{V}$$
11		cnvimass	$$⊢f^{-1}\left[\mathrm{ran}E\right]\subseteq \mathrm{dom}f$$
12	11 8	fssdm	$$⊢f:A\underset{onto}{⟶}\mathrm{\omega }\to f^{-1}\left[\mathrm{ran}E\right]\subseteq A$$
13	10 12	sselpwd	$$⊢f:A\underset{onto}{⟶}\mathrm{\omega }\to f^{-1}\left[\mathrm{ran}E\right]\in 𝒫A$$
14	1	fin1a2lem4	$$⊢E:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{\omega }$$
15		f1cnv	$$⊢E:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{\omega }\to E^{-1}:\mathrm{ran}E\underset{1-1\; onto}{⟶}\mathrm{\omega }$$
16		f1ofo	$$⊢E^{-1}:\mathrm{ran}E\underset{1-1\; onto}{⟶}\mathrm{\omega }\to E^{-1}:\mathrm{ran}E\underset{onto}{⟶}\mathrm{\omega }$$
17	14 15 16	mp2b	$$⊢E^{-1}:\mathrm{ran}E\underset{onto}{⟶}\mathrm{\omega }$$
18		fofun	$$⊢E^{-1}:\mathrm{ran}E\underset{onto}{⟶}\mathrm{\omega }\to \mathrm{Fun}{E}^{-1}$$
19	17 18	ax-mp	$$⊢\mathrm{Fun}{E}^{-1}$$
20	7	resex	$$⊢{f\upharpoonright }_{f^{-1}\left[\mathrm{ran}E\right]}\in \mathrm{V}$$
21		cofunexg	$$⊢\left(\mathrm{Fun}{E}^{-1}\wedge {f\upharpoonright }_{f^{-1}\left[\mathrm{ran}E\right]}\in \mathrm{V}\right)\to E^{-1}\circ \left({f\upharpoonright }_{f^{-1}\left[\mathrm{ran}E\right]}\right)\in \mathrm{V}$$
22	19 20 21	mp2an	$$⊢E^{-1}\circ \left({f\upharpoonright }_{f^{-1}\left[\mathrm{ran}E\right]}\right)\in \mathrm{V}$$
23		fofun	$$⊢f:A\underset{onto}{⟶}\mathrm{\omega }\to \mathrm{Fun}f$$
24		fores	$$⊢\left(\mathrm{Fun}f\wedge f^{-1}\left[\mathrm{ran}E\right]\subseteq \mathrm{dom}f\right)\to \left({f\upharpoonright }_{f^{-1}\left[\mathrm{ran}E\right]}\right):f^{-1}\left[\mathrm{ran}E\right]\underset{onto}{⟶}f\left[f^{-1}\left[\mathrm{ran}E\right]\right]$$
25	23 11 24	sylancl	$$⊢f:A\underset{onto}{⟶}\mathrm{\omega }\to \left({f\upharpoonright }_{f^{-1}\left[\mathrm{ran}E\right]}\right):f^{-1}\left[\mathrm{ran}E\right]\underset{onto}{⟶}f\left[f^{-1}\left[\mathrm{ran}E\right]\right]$$
26		f1f	$$⊢E:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{\omega }\to E:\mathrm{\omega }⟶\mathrm{\omega }$$
27		frn	$$⊢E:\mathrm{\omega }⟶\mathrm{\omega }\to \mathrm{ran}E\subseteq \mathrm{\omega }$$
28	14 26 27	mp2b	$$⊢\mathrm{ran}E\subseteq \mathrm{\omega }$$
29		foimacnv	$$⊢\left(f:A\underset{onto}{⟶}\mathrm{\omega }\wedge \mathrm{ran}E\subseteq \mathrm{\omega }\right)\to f\left[f^{-1}\left[\mathrm{ran}E\right]\right]=\mathrm{ran}E$$
30	28 29	mpan2	$$⊢f:A\underset{onto}{⟶}\mathrm{\omega }\to f\left[f^{-1}\left[\mathrm{ran}E\right]\right]=\mathrm{ran}E$$
31		foeq3	$$⊢f\left[f^{-1}\left[\mathrm{ran}E\right]\right]=\mathrm{ran}E\to \left(\left({f\upharpoonright }_{f^{-1}\left[\mathrm{ran}E\right]}\right):f^{-1}\left[\mathrm{ran}E\right]\underset{onto}{⟶}f\left[f^{-1}\left[\mathrm{ran}E\right]\right]\leftrightarrow \left({f\upharpoonright }_{f^{-1}\left[\mathrm{ran}E\right]}\right):f^{-1}\left[\mathrm{ran}E\right]\underset{onto}{⟶}\mathrm{ran}E\right)$$
32	30 31	syl	$$⊢f:A\underset{onto}{⟶}\mathrm{\omega }\to \left(\left({f\upharpoonright }_{f^{-1}\left[\mathrm{ran}E\right]}\right):f^{-1}\left[\mathrm{ran}E\right]\underset{onto}{⟶}f\left[f^{-1}\left[\mathrm{ran}E\right]\right]\leftrightarrow \left({f\upharpoonright }_{f^{-1}\left[\mathrm{ran}E\right]}\right):f^{-1}\left[\mathrm{ran}E\right]\underset{onto}{⟶}\mathrm{ran}E\right)$$
33	25 32	mpbid	$$⊢f:A\underset{onto}{⟶}\mathrm{\omega }\to \left({f\upharpoonright }_{f^{-1}\left[\mathrm{ran}E\right]}\right):f^{-1}\left[\mathrm{ran}E\right]\underset{onto}{⟶}\mathrm{ran}E$$
34		foco	$$⊢\left(E^{-1}:\mathrm{ran}E\underset{onto}{⟶}\mathrm{\omega }\wedge \left({f\upharpoonright }_{f^{-1}\left[\mathrm{ran}E\right]}\right):f^{-1}\left[\mathrm{ran}E\right]\underset{onto}{⟶}\mathrm{ran}E\right)\to \left(E^{-1}\circ \left({f\upharpoonright }_{f^{-1}\left[\mathrm{ran}E\right]}\right)\right):f^{-1}\left[\mathrm{ran}E\right]\underset{onto}{⟶}\mathrm{\omega }$$
35	17 33 34	sylancr	$$⊢f:A\underset{onto}{⟶}\mathrm{\omega }\to \left(E^{-1}\circ \left({f\upharpoonright }_{f^{-1}\left[\mathrm{ran}E\right]}\right)\right):f^{-1}\left[\mathrm{ran}E\right]\underset{onto}{⟶}\mathrm{\omega }$$
36		fowdom	$$⊢\left(E^{-1}\circ \left({f\upharpoonright }_{f^{-1}\left[\mathrm{ran}E\right]}\right)\in \mathrm{V}\wedge \left(E^{-1}\circ \left({f\upharpoonright }_{f^{-1}\left[\mathrm{ran}E\right]}\right)\right):f^{-1}\left[\mathrm{ran}E\right]\underset{onto}{⟶}\mathrm{\omega }\right)\to \mathrm{\omega }{\preccurlyeq }^{*}{f}^{-1}\left[\mathrm{ran}E\right]$$
37	22 35 36	sylancr	$$⊢f:A\underset{onto}{⟶}\mathrm{\omega }\to \mathrm{\omega }{\preccurlyeq }^{*}{f}^{-1}\left[\mathrm{ran}E\right]$$
38	7	cnvex	$$⊢f^{-1}\in \mathrm{V}$$
39	38	imaex	$$⊢f^{-1}\left[\mathrm{ran}E\right]\in \mathrm{V}$$
40		isfin3-2	$$⊢f^{-1}\left[\mathrm{ran}E\right]\in \mathrm{V}\to \left(f^{-1}\left[\mathrm{ran}E\right]\in {\mathrm{Fin}}^{\mathrm{III}}\leftrightarrow \neg \mathrm{\omega }{\preccurlyeq }^{*}{f}^{-1}\left[\mathrm{ran}E\right]\right)$$
41	39 40	ax-mp	$$⊢f^{-1}\left[\mathrm{ran}E\right]\in {\mathrm{Fin}}^{\mathrm{III}}\leftrightarrow \neg \mathrm{\omega }{\preccurlyeq }^{*}{f}^{-1}\left[\mathrm{ran}E\right]$$
42	41	con2bii	$$⊢\mathrm{\omega }{\preccurlyeq }^{*}{f}^{-1}\left[\mathrm{ran}E\right]\leftrightarrow \neg f^{-1}\left[\mathrm{ran}E\right]\in {\mathrm{Fin}}^{\mathrm{III}}$$
43	37 42	sylib	$$⊢f:A\underset{onto}{⟶}\mathrm{\omega }\to \neg f^{-1}\left[\mathrm{ran}E\right]\in {\mathrm{Fin}}^{\mathrm{III}}$$
44	1 2	fin1a2lem6	$$⊢\left({S\upharpoonright }_{\mathrm{ran}E}\right):\mathrm{ran}E\underset{1-1\; onto}{⟶}\mathrm{\omega }\setminus \mathrm{ran}E$$
45		f1ocnv	$$⊢\left({S\upharpoonright }_{\mathrm{ran}E}\right):\mathrm{ran}E\underset{1-1\; onto}{⟶}\mathrm{\omega }\setminus \mathrm{ran}E\to {\left({S\upharpoonright }_{\mathrm{ran}E}\right)}^{-1}:\mathrm{\omega }\setminus \mathrm{ran}E\underset{1-1\; onto}{⟶}\mathrm{ran}E$$
46		f1ofo	$$⊢{\left({S\upharpoonright }_{\mathrm{ran}E}\right)}^{-1}:\mathrm{\omega }\setminus \mathrm{ran}E\underset{1-1\; onto}{⟶}\mathrm{ran}E\to {\left({S\upharpoonright }_{\mathrm{ran}E}\right)}^{-1}:\mathrm{\omega }\setminus \mathrm{ran}E\underset{onto}{⟶}\mathrm{ran}E$$
47	44 45 46	mp2b	$$⊢{\left({S\upharpoonright }_{\mathrm{ran}E}\right)}^{-1}:\mathrm{\omega }\setminus \mathrm{ran}E\underset{onto}{⟶}\mathrm{ran}E$$
48		foco	$$⊢\left(E^{-1}:\mathrm{ran}E\underset{onto}{⟶}\mathrm{\omega }\wedge {\left({S\upharpoonright }_{\mathrm{ran}E}\right)}^{-1}:\mathrm{\omega }\setminus \mathrm{ran}E\underset{onto}{⟶}\mathrm{ran}E\right)\to \left(E^{-1}\circ {\left({S\upharpoonright }_{\mathrm{ran}E}\right)}^{-1}\right):\mathrm{\omega }\setminus \mathrm{ran}E\underset{onto}{⟶}\mathrm{\omega }$$
49	17 47 48	mp2an	$$⊢\left(E^{-1}\circ {\left({S\upharpoonright }_{\mathrm{ran}E}\right)}^{-1}\right):\mathrm{\omega }\setminus \mathrm{ran}E\underset{onto}{⟶}\mathrm{\omega }$$
50		fofun	$$⊢\left(E^{-1}\circ {\left({S\upharpoonright }_{\mathrm{ran}E}\right)}^{-1}\right):\mathrm{\omega }\setminus \mathrm{ran}E\underset{onto}{⟶}\mathrm{\omega }\to \mathrm{Fun}\left(E^{-1}\circ {\left({S\upharpoonright }_{\mathrm{ran}E}\right)}^{-1}\right)$$
51	49 50	ax-mp	$$⊢\mathrm{Fun}\left(E^{-1}\circ {\left({S\upharpoonright }_{\mathrm{ran}E}\right)}^{-1}\right)$$
52	7	resex	$$⊢{f\upharpoonright }_{\left(A\setminus f^{-1}\left[\mathrm{ran}E\right]\right)}\in \mathrm{V}$$
53		cofunexg	$$⊢\left(\mathrm{Fun}\left(E^{-1}\circ {\left({S\upharpoonright }_{\mathrm{ran}E}\right)}^{-1}\right)\wedge {f\upharpoonright }_{\left(A\setminus f^{-1}\left[\mathrm{ran}E\right]\right)}\in \mathrm{V}\right)\to \left(E^{-1}\circ {\left({S\upharpoonright }_{\mathrm{ran}E}\right)}^{-1}\right)\circ \left({f\upharpoonright }_{\left(A\setminus f^{-1}\left[\mathrm{ran}E\right]\right)}\right)\in \mathrm{V}$$
54	51 52 53	mp2an	$$⊢\left(E^{-1}\circ {\left({S\upharpoonright }_{\mathrm{ran}E}\right)}^{-1}\right)\circ \left({f\upharpoonright }_{\left(A\setminus f^{-1}\left[\mathrm{ran}E\right]\right)}\right)\in \mathrm{V}$$
55		difss	$$⊢A\setminus f^{-1}\left[\mathrm{ran}E\right]\subseteq A$$
56	8	fdmd	$$⊢f:A\underset{onto}{⟶}\mathrm{\omega }\to \mathrm{dom}f=A$$
57	55 56	sseqtrrid	$$⊢f:A\underset{onto}{⟶}\mathrm{\omega }\to A\setminus f^{-1}\left[\mathrm{ran}E\right]\subseteq \mathrm{dom}f$$
58		fores	$$⊢\left(\mathrm{Fun}f\wedge A\setminus f^{-1}\left[\mathrm{ran}E\right]\subseteq \mathrm{dom}f\right)\to \left({f\upharpoonright }_{\left(A\setminus f^{-1}\left[\mathrm{ran}E\right]\right)}\right):A\setminus f^{-1}\left[\mathrm{ran}E\right]\underset{onto}{⟶}f\left[A\setminus f^{-1}\left[\mathrm{ran}E\right]\right]$$
59	23 57 58	syl2anc	$$⊢f:A\underset{onto}{⟶}\mathrm{\omega }\to \left({f\upharpoonright }_{\left(A\setminus f^{-1}\left[\mathrm{ran}E\right]\right)}\right):A\setminus f^{-1}\left[\mathrm{ran}E\right]\underset{onto}{⟶}f\left[A\setminus f^{-1}\left[\mathrm{ran}E\right]\right]$$
60		funcnvcnv	$$⊢\mathrm{Fun}f\to \mathrm{Fun}{f^{-1}}^{-1}$$
61		imadif	$$⊢\mathrm{Fun}{f^{-1}}^{-1}\to f^{-1}\left[\mathrm{\omega }\setminus \mathrm{ran}E\right]=f^{-1}\left[\mathrm{\omega }\right]\setminus f^{-1}\left[\mathrm{ran}E\right]$$
62	23 60 61	3syl	$$⊢f:A\underset{onto}{⟶}\mathrm{\omega }\to f^{-1}\left[\mathrm{\omega }\setminus \mathrm{ran}E\right]=f^{-1}\left[\mathrm{\omega }\right]\setminus f^{-1}\left[\mathrm{ran}E\right]$$
63	62	imaeq2d	$$⊢f:A\underset{onto}{⟶}\mathrm{\omega }\to f\left[f^{-1}\left[\mathrm{\omega }\setminus \mathrm{ran}E\right]\right]=f\left[f^{-1}\left[\mathrm{\omega }\right]\setminus f^{-1}\left[\mathrm{ran}E\right]\right]$$
64		difss	$$⊢\mathrm{\omega }\setminus \mathrm{ran}E\subseteq \mathrm{\omega }$$
65		foimacnv	$$⊢\left(f:A\underset{onto}{⟶}\mathrm{\omega }\wedge \mathrm{\omega }\setminus \mathrm{ran}E\subseteq \mathrm{\omega }\right)\to f\left[f^{-1}\left[\mathrm{\omega }\setminus \mathrm{ran}E\right]\right]=\mathrm{\omega }\setminus \mathrm{ran}E$$
66	64 65	mpan2	$$⊢f:A\underset{onto}{⟶}\mathrm{\omega }\to f\left[f^{-1}\left[\mathrm{\omega }\setminus \mathrm{ran}E\right]\right]=\mathrm{\omega }\setminus \mathrm{ran}E$$
67		fimacnv	$$⊢f:A⟶\mathrm{\omega }\to f^{-1}\left[\mathrm{\omega }\right]=A$$
68	8 67	syl	$$⊢f:A\underset{onto}{⟶}\mathrm{\omega }\to f^{-1}\left[\mathrm{\omega }\right]=A$$
69	68	difeq1d	$$⊢f:A\underset{onto}{⟶}\mathrm{\omega }\to f^{-1}\left[\mathrm{\omega }\right]\setminus f^{-1}\left[\mathrm{ran}E\right]=A\setminus f^{-1}\left[\mathrm{ran}E\right]$$
70	69	imaeq2d	$$⊢f:A\underset{onto}{⟶}\mathrm{\omega }\to f\left[f^{-1}\left[\mathrm{\omega }\right]\setminus f^{-1}\left[\mathrm{ran}E\right]\right]=f\left[A\setminus f^{-1}\left[\mathrm{ran}E\right]\right]$$
71	63 66 70	3eqtr3rd	$$⊢f:A\underset{onto}{⟶}\mathrm{\omega }\to f\left[A\setminus f^{-1}\left[\mathrm{ran}E\right]\right]=\mathrm{\omega }\setminus \mathrm{ran}E$$
72		foeq3	$$⊢f\left[A\setminus f^{-1}\left[\mathrm{ran}E\right]\right]=\mathrm{\omega }\setminus \mathrm{ran}E\to \left(\left({f\upharpoonright }_{\left(A\setminus f^{-1}\left[\mathrm{ran}E\right]\right)}\right):A\setminus f^{-1}\left[\mathrm{ran}E\right]\underset{onto}{⟶}f\left[A\setminus f^{-1}\left[\mathrm{ran}E\right]\right]\leftrightarrow \left({f\upharpoonright }_{\left(A\setminus f^{-1}\left[\mathrm{ran}E\right]\right)}\right):A\setminus f^{-1}\left[\mathrm{ran}E\right]\underset{onto}{⟶}\mathrm{\omega }\setminus \mathrm{ran}E\right)$$
73	71 72	syl	$$⊢f:A\underset{onto}{⟶}\mathrm{\omega }\to \left(\left({f\upharpoonright }_{\left(A\setminus f^{-1}\left[\mathrm{ran}E\right]\right)}\right):A\setminus f^{-1}\left[\mathrm{ran}E\right]\underset{onto}{⟶}f\left[A\setminus f^{-1}\left[\mathrm{ran}E\right]\right]\leftrightarrow \left({f\upharpoonright }_{\left(A\setminus f^{-1}\left[\mathrm{ran}E\right]\right)}\right):A\setminus f^{-1}\left[\mathrm{ran}E\right]\underset{onto}{⟶}\mathrm{\omega }\setminus \mathrm{ran}E\right)$$
74	59 73	mpbid	$$⊢f:A\underset{onto}{⟶}\mathrm{\omega }\to \left({f\upharpoonright }_{\left(A\setminus f^{-1}\left[\mathrm{ran}E\right]\right)}\right):A\setminus f^{-1}\left[\mathrm{ran}E\right]\underset{onto}{⟶}\mathrm{\omega }\setminus \mathrm{ran}E$$
75		foco	$$⊢\left(\left(E^{-1}\circ {\left({S\upharpoonright }_{\mathrm{ran}E}\right)}^{-1}\right):\mathrm{\omega }\setminus \mathrm{ran}E\underset{onto}{⟶}\mathrm{\omega }\wedge \left({f\upharpoonright }_{\left(A\setminus f^{-1}\left[\mathrm{ran}E\right]\right)}\right):A\setminus f^{-1}\left[\mathrm{ran}E\right]\underset{onto}{⟶}\mathrm{\omega }\setminus \mathrm{ran}E\right)\to \left(\left(E^{-1}\circ {\left({S\upharpoonright }_{\mathrm{ran}E}\right)}^{-1}\right)\circ \left({f\upharpoonright }_{\left(A\setminus f^{-1}\left[\mathrm{ran}E\right]\right)}\right)\right):A\setminus f^{-1}\left[\mathrm{ran}E\right]\underset{onto}{⟶}\mathrm{\omega }$$
76	49 74 75	sylancr	$$⊢f:A\underset{onto}{⟶}\mathrm{\omega }\to \left(\left(E^{-1}\circ {\left({S\upharpoonright }_{\mathrm{ran}E}\right)}^{-1}\right)\circ \left({f\upharpoonright }_{\left(A\setminus f^{-1}\left[\mathrm{ran}E\right]\right)}\right)\right):A\setminus f^{-1}\left[\mathrm{ran}E\right]\underset{onto}{⟶}\mathrm{\omega }$$
77		fowdom	$$⊢\left(\left(E^{-1}\circ {\left({S\upharpoonright }_{\mathrm{ran}E}\right)}^{-1}\right)\circ \left({f\upharpoonright }_{\left(A\setminus f^{-1}\left[\mathrm{ran}E\right]\right)}\right)\in \mathrm{V}\wedge \left(\left(E^{-1}\circ {\left({S\upharpoonright }_{\mathrm{ran}E}\right)}^{-1}\right)\circ \left({f\upharpoonright }_{\left(A\setminus f^{-1}\left[\mathrm{ran}E\right]\right)}\right)\right):A\setminus f^{-1}\left[\mathrm{ran}E\right]\underset{onto}{⟶}\mathrm{\omega }\right)\to \mathrm{\omega }{\preccurlyeq }^{*}\left(A\setminus f^{-1}\left[\mathrm{ran}E\right]\right)$$
78	54 76 77	sylancr	$$⊢f:A\underset{onto}{⟶}\mathrm{\omega }\to \mathrm{\omega }{\preccurlyeq }^{*}\left(A\setminus f^{-1}\left[\mathrm{ran}E\right]\right)$$
79		difexg	$$⊢A\in \mathrm{V}\to A\setminus f^{-1}\left[\mathrm{ran}E\right]\in \mathrm{V}$$
80		isfin3-2	$$⊢A\setminus f^{-1}\left[\mathrm{ran}E\right]\in \mathrm{V}\to \left(A\setminus f^{-1}\left[\mathrm{ran}E\right]\in {\mathrm{Fin}}^{\mathrm{III}}\leftrightarrow \neg \mathrm{\omega }{\preccurlyeq }^{*}\left(A\setminus f^{-1}\left[\mathrm{ran}E\right]\right)\right)$$
81	10 79 80	3syl	$$⊢f:A\underset{onto}{⟶}\mathrm{\omega }\to \left(A\setminus f^{-1}\left[\mathrm{ran}E\right]\in {\mathrm{Fin}}^{\mathrm{III}}\leftrightarrow \neg \mathrm{\omega }{\preccurlyeq }^{*}\left(A\setminus f^{-1}\left[\mathrm{ran}E\right]\right)\right)$$
82	81	con2bid	$$⊢f:A\underset{onto}{⟶}\mathrm{\omega }\to \left(\mathrm{\omega }{\preccurlyeq }^{*}\left(A\setminus f^{-1}\left[\mathrm{ran}E\right]\right)\leftrightarrow \neg A\setminus f^{-1}\left[\mathrm{ran}E\right]\in {\mathrm{Fin}}^{\mathrm{III}}\right)$$
83	78 82	mpbid	$$⊢f:A\underset{onto}{⟶}\mathrm{\omega }\to \neg A\setminus f^{-1}\left[\mathrm{ran}E\right]\in {\mathrm{Fin}}^{\mathrm{III}}$$
84		eleq1	$$⊢y=f^{-1}\left[\mathrm{ran}E\right]\to \left(y\in {\mathrm{Fin}}^{\mathrm{III}}\leftrightarrow f^{-1}\left[\mathrm{ran}E\right]\in {\mathrm{Fin}}^{\mathrm{III}}\right)$$
85		difeq2	$$⊢y=f^{-1}\left[\mathrm{ran}E\right]\to A\setminus y=A\setminus f^{-1}\left[\mathrm{ran}E\right]$$
86	85	eleq1d	$$⊢y=f^{-1}\left[\mathrm{ran}E\right]\to \left(A\setminus y\in {\mathrm{Fin}}^{\mathrm{III}}\leftrightarrow A\setminus f^{-1}\left[\mathrm{ran}E\right]\in {\mathrm{Fin}}^{\mathrm{III}}\right)$$
87	84 86	orbi12d	$$⊢y=f^{-1}\left[\mathrm{ran}E\right]\to \left(\left(y\in {\mathrm{Fin}}^{\mathrm{III}}\vee A\setminus y\in {\mathrm{Fin}}^{\mathrm{III}}\right)\leftrightarrow \left(f^{-1}\left[\mathrm{ran}E\right]\in {\mathrm{Fin}}^{\mathrm{III}}\vee A\setminus f^{-1}\left[\mathrm{ran}E\right]\in {\mathrm{Fin}}^{\mathrm{III}}\right)\right)$$
88	87	notbid	$$⊢y=f^{-1}\left[\mathrm{ran}E\right]\to \left(\neg \left(y\in {\mathrm{Fin}}^{\mathrm{III}}\vee A\setminus y\in {\mathrm{Fin}}^{\mathrm{III}}\right)\leftrightarrow \neg \left(f^{-1}\left[\mathrm{ran}E\right]\in {\mathrm{Fin}}^{\mathrm{III}}\vee A\setminus f^{-1}\left[\mathrm{ran}E\right]\in {\mathrm{Fin}}^{\mathrm{III}}\right)\right)$$
89		ioran	$$⊢\neg \left(f^{-1}\left[\mathrm{ran}E\right]\in {\mathrm{Fin}}^{\mathrm{III}}\vee A\setminus f^{-1}\left[\mathrm{ran}E\right]\in {\mathrm{Fin}}^{\mathrm{III}}\right)\leftrightarrow \left(\neg f^{-1}\left[\mathrm{ran}E\right]\in {\mathrm{Fin}}^{\mathrm{III}}\wedge \neg A\setminus f^{-1}\left[\mathrm{ran}E\right]\in {\mathrm{Fin}}^{\mathrm{III}}\right)$$
90	88 89	bitrdi	$$⊢y=f^{-1}\left[\mathrm{ran}E\right]\to \left(\neg \left(y\in {\mathrm{Fin}}^{\mathrm{III}}\vee A\setminus y\in {\mathrm{Fin}}^{\mathrm{III}}\right)\leftrightarrow \left(\neg f^{-1}\left[\mathrm{ran}E\right]\in {\mathrm{Fin}}^{\mathrm{III}}\wedge \neg A\setminus f^{-1}\left[\mathrm{ran}E\right]\in {\mathrm{Fin}}^{\mathrm{III}}\right)\right)$$
91	90	rspcev	$$⊢\left(f^{-1}\left[\mathrm{ran}E\right]\in 𝒫A\wedge \left(\neg f^{-1}\left[\mathrm{ran}E\right]\in {\mathrm{Fin}}^{\mathrm{III}}\wedge \neg A\setminus f^{-1}\left[\mathrm{ran}E\right]\in {\mathrm{Fin}}^{\mathrm{III}}\right)\right)\to \exists y\in 𝒫A\neg \left(y\in {\mathrm{Fin}}^{\mathrm{III}}\vee A\setminus y\in {\mathrm{Fin}}^{\mathrm{III}}\right)$$
92	13 43 83 91	syl12anc	$$⊢f:A\underset{onto}{⟶}\mathrm{\omega }\to \exists y\in 𝒫A\neg \left(y\in {\mathrm{Fin}}^{\mathrm{III}}\vee A\setminus y\in {\mathrm{Fin}}^{\mathrm{III}}\right)$$
93		rexnal	$$⊢\exists y\in 𝒫A\neg \left(y\in {\mathrm{Fin}}^{\mathrm{III}}\vee A\setminus y\in {\mathrm{Fin}}^{\mathrm{III}}\right)\leftrightarrow \neg \forall y\in 𝒫A\left(y\in {\mathrm{Fin}}^{\mathrm{III}}\vee A\setminus y\in {\mathrm{Fin}}^{\mathrm{III}}\right)$$
94	92 93	sylib	$$⊢f:A\underset{onto}{⟶}\mathrm{\omega }\to \neg \forall y\in 𝒫A\left(y\in {\mathrm{Fin}}^{\mathrm{III}}\vee A\setminus y\in {\mathrm{Fin}}^{\mathrm{III}}\right)$$
95	94	exlimiv	$$⊢\exists ff:A\underset{onto}{⟶}\mathrm{\omega }\to \neg \forall y\in 𝒫A\left(y\in {\mathrm{Fin}}^{\mathrm{III}}\vee A\setminus y\in {\mathrm{Fin}}^{\mathrm{III}}\right)$$
96	6 95	sylbi	$$⊢\mathrm{\omega }{\preccurlyeq }^{*}A\to \neg \forall y\in 𝒫A\left(y\in {\mathrm{Fin}}^{\mathrm{III}}\vee A\setminus y\in {\mathrm{Fin}}^{\mathrm{III}}\right)$$
97	96	con2i	$$⊢\forall y\in 𝒫A\left(y\in {\mathrm{Fin}}^{\mathrm{III}}\vee A\setminus y\in {\mathrm{Fin}}^{\mathrm{III}}\right)\to \neg \mathrm{\omega }{\preccurlyeq }^{*}A$$
98		isfin3-2	$$⊢A\in V\to \left(A\in {\mathrm{Fin}}^{\mathrm{III}}\leftrightarrow \neg \mathrm{\omega }{\preccurlyeq }^{*}A\right)$$
99	97 98	imbitrrid	$$⊢A\in V\to \left(\forall y\in 𝒫A\left(y\in {\mathrm{Fin}}^{\mathrm{III}}\vee A\setminus y\in {\mathrm{Fin}}^{\mathrm{III}}\right)\to A\in {\mathrm{Fin}}^{\mathrm{III}}\right)$$
100	99	imp	$$⊢\left(A\in V\wedge \forall y\in 𝒫A\left(y\in {\mathrm{Fin}}^{\mathrm{III}}\vee A\setminus y\in {\mathrm{Fin}}^{\mathrm{III}}\right)\right)\to A\in {\mathrm{Fin}}^{\mathrm{III}}$$