# Metamath Proof Explorer

## 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}}^{V}\to {A}\in {\mathrm{Fin}}^{VI}$

### Proof

Step Hyp Ref Expression
1 orc ${⊢}{A}=\varnothing \to \left({A}=\varnothing \vee {A}\approx {1}_{𝑜}\right)$
2 sdom2en01 ${⊢}{A}\prec {2}_{𝑜}↔\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}×{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}↔¬{A}\prec {2}_{𝑜}\right)$
13 9 11 12 sylancr ${⊢}{A}\prec \left({A}\mathrm{\bigsqcup ︀}{A}\right)\to \left({2}_{𝑜}\preccurlyeq {A}↔¬{A}\prec {2}_{𝑜}\right)$
14 xp2dju ${⊢}{2}_{𝑜}×{A}=\left({A}\mathrm{\bigsqcup ︀}{A}\right)$
15 xpdom1g ${⊢}\left({A}\in \mathrm{V}\wedge {2}_{𝑜}\preccurlyeq {A}\right)\to \left({2}_{𝑜}×{A}\right)\preccurlyeq \left({A}×{A}\right)$
16 11 15 sylan ${⊢}\left({A}\prec \left({A}\mathrm{\bigsqcup ︀}{A}\right)\wedge {2}_{𝑜}\preccurlyeq {A}\right)\to \left({2}_{𝑜}×{A}\right)\preccurlyeq \left({A}×{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}×{A}\right)$
18 sdomdomtr ${⊢}\left({A}\prec \left({A}\mathrm{\bigsqcup ︀}{A}\right)\wedge \left({A}\mathrm{\bigsqcup ︀}{A}\right)\preccurlyeq \left({A}×{A}\right)\right)\to {A}\prec \left({A}×{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}×{A}\right)$
20 19 ex ${⊢}{A}\prec \left({A}\mathrm{\bigsqcup ︀}{A}\right)\to \left({2}_{𝑜}\preccurlyeq {A}\to {A}\prec \left({A}×{A}\right)\right)$
21 13 20 sylbird ${⊢}{A}\prec \left({A}\mathrm{\bigsqcup ︀}{A}\right)\to \left(¬{A}\prec {2}_{𝑜}\to {A}\prec \left({A}×{A}\right)\right)$
22 21 orrd ${⊢}{A}\prec \left({A}\mathrm{\bigsqcup ︀}{A}\right)\to \left({A}\prec {2}_{𝑜}\vee {A}\prec \left({A}×{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}×{A}\right)\right)$
24 isfin5 ${⊢}{A}\in {\mathrm{Fin}}^{V}↔\left({A}=\varnothing \vee {A}\prec \left({A}\mathrm{\bigsqcup ︀}{A}\right)\right)$
25 isfin6 ${⊢}{A}\in {\mathrm{Fin}}^{VI}↔\left({A}\prec {2}_{𝑜}\vee {A}\prec \left({A}×{A}\right)\right)$
26 23 24 25 3imtr4i ${⊢}{A}\in {\mathrm{Fin}}^{V}\to {A}\in {\mathrm{Fin}}^{VI}$