Theorem fin56

Description: Every V-finite set is VI-finite because multiplication dominates addition for cardinals. (Contributed by Stefan O'Rear, 29-Oct-2014) (Revised by Mario Carneiro, 17-May-2015)

	Ref	Expression
Assertion	fin56	$$⊢A\in {\mathrm{Fin}}^{\mathrm{V}}\to A\in {\mathrm{Fin}}^{\mathrm{VI}}$$

Proof

Step	Hyp	Ref	Expression
1		orc	$$⊢A=\varnothing \to \left(A=\varnothing \vee A\approx 1_{𝑜}\right)$$
2		sdom2en01	$$⊢A\prec 2_{𝑜}\leftrightarrow \left(A=\varnothing \vee A\approx 1_{𝑜}\right)$$
3	1 2	sylibr	$$⊢A=\varnothing \to A\prec 2_{𝑜}$$
4	3	orcd	$$⊢A=\varnothing \to \left(A\prec 2_{𝑜}\vee A\prec \left(A\times A\right)\right)$$
5		onfin2	$$⊢\mathrm{\omega }=\mathrm{On}\cap \mathrm{Fin}$$
6		inss2	$$⊢\mathrm{On}\cap \mathrm{Fin}\subseteq \mathrm{Fin}$$
7	5 6	eqsstri	$$⊢\mathrm{\omega }\subseteq \mathrm{Fin}$$
8		2onn	$$⊢2_{𝑜}\in \mathrm{\omega }$$
9	7 8	sselii	$$⊢2_{𝑜}\in \mathrm{Fin}$$
10		relsdom	$$⊢\mathrm{Rel}\prec$$
11	10	brrelex1i	$$⊢A\prec \left(A\mathrm{\bigsqcup ︀}A\right)\to A\in \mathrm{V}$$
12		fidomtri	$$⊢\left(2_{𝑜}\in \mathrm{Fin}\wedge A\in \mathrm{V}\right)\to \left(2_{𝑜}\preccurlyeq A\leftrightarrow \neg A\prec 2_{𝑜}\right)$$
13	9 11 12	sylancr	$$⊢A\prec \left(A\mathrm{\bigsqcup ︀}A\right)\to \left(2_{𝑜}\preccurlyeq A\leftrightarrow \neg A\prec 2_{𝑜}\right)$$
14		xp2dju	$$⊢2_{𝑜}\times A=\left(A\mathrm{\bigsqcup ︀}A\right)$$
15		xpdom1g	$$⊢\left(A\in \mathrm{V}\wedge 2_{𝑜}\preccurlyeq A\right)\to \left(2_{𝑜}\times A\right)\preccurlyeq \left(A\times A\right)$$
16	11 15	sylan	$$⊢\left(A\prec \left(A\mathrm{\bigsqcup ︀}A\right)\wedge 2_{𝑜}\preccurlyeq A\right)\to \left(2_{𝑜}\times A\right)\preccurlyeq \left(A\times A\right)$$
17	14 16	eqbrtrrid	$$⊢\left(A\prec \left(A\mathrm{\bigsqcup ︀}A\right)\wedge 2_{𝑜}\preccurlyeq A\right)\to \left(A\mathrm{\bigsqcup ︀}A\right)\preccurlyeq \left(A\times A\right)$$
18		sdomdomtr	$$⊢\left(A\prec \left(A\mathrm{\bigsqcup ︀}A\right)\wedge \left(A\mathrm{\bigsqcup ︀}A\right)\preccurlyeq \left(A\times A\right)\right)\to A\prec \left(A\times A\right)$$
19	17 18	syldan	$$⊢\left(A\prec \left(A\mathrm{\bigsqcup ︀}A\right)\wedge 2_{𝑜}\preccurlyeq A\right)\to A\prec \left(A\times A\right)$$
20	19	ex	$$⊢A\prec \left(A\mathrm{\bigsqcup ︀}A\right)\to \left(2_{𝑜}\preccurlyeq A\to A\prec \left(A\times A\right)\right)$$
21	13 20	sylbird	$$⊢A\prec \left(A\mathrm{\bigsqcup ︀}A\right)\to \left(\neg A\prec 2_{𝑜}\to A\prec \left(A\times A\right)\right)$$
22	21	orrd	$$⊢A\prec \left(A\mathrm{\bigsqcup ︀}A\right)\to \left(A\prec 2_{𝑜}\vee A\prec \left(A\times A\right)\right)$$
23	4 22	jaoi	$$⊢\left(A=\varnothing \vee A\prec \left(A\mathrm{\bigsqcup ︀}A\right)\right)\to \left(A\prec 2_{𝑜}\vee A\prec \left(A\times A\right)\right)$$
24		isfin5	$$⊢A\in {\mathrm{Fin}}^{\mathrm{V}}\leftrightarrow \left(A=\varnothing \vee A\prec \left(A\mathrm{\bigsqcup ︀}A\right)\right)$$
25		isfin6	$$⊢A\in {\mathrm{Fin}}^{\mathrm{VI}}\leftrightarrow \left(A\prec 2_{𝑜}\vee A\prec \left(A\times A\right)\right)$$
26	23 24 25	3imtr4i	$$⊢A\in {\mathrm{Fin}}^{\mathrm{V}}\to A\in {\mathrm{Fin}}^{\mathrm{VI}}$$