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 e. Fin5 -> A e. Fin6 )

Proof

Step	Hyp	Ref	Expression
1		orc	|- ( A = (/) -> ( A = (/) \/ A ~~ 1o ) )
2		sdom2en01	|- ( A ~< 2o <-> ( A = (/) \/ A ~~ 1o ) )
3	1 2	sylibr	|- ( A = (/) -> A ~< 2o )
4	3	orcd	|- ( A = (/) -> ( A ~< 2o \/ A ~< ( A X. A ) ) )
5		onfin2	|- _om = ( On i^i Fin )
6		inss2	|- ( On i^i Fin ) C_ Fin
7	5 6	eqsstri	|- _om C_ Fin
8		2onn	|- 2o e. _om
9	7 8	sselii	|- 2o e. Fin
10		relsdom	|- Rel ~<
11	10	brrelex1i	|- ( A ~< ( A |_| A ) -> A e. _V )
12		fidomtri	|- ( ( 2o e. Fin /\ A e. _V ) -> ( 2o ~<_ A <-> -. A ~< 2o ) )
13	9 11 12	sylancr	|- ( A ~< ( A |_| A ) -> ( 2o ~<_ A <-> -. A ~< 2o ) )
14		xp2dju	|- ( 2o X. A ) = ( A |_| A )
15		xpdom1g	|- ( ( A e. _V /\ 2o ~<_ A ) -> ( 2o X. A ) ~<_ ( A X. A ) )
16	11 15	sylan	|- ( ( A ~< ( A |_| A ) /\ 2o ~<_ A ) -> ( 2o X. A ) ~<_ ( A X. A ) )
17	14 16	eqbrtrrid	|- ( ( A ~< ( A |_| A ) /\ 2o ~<_ A ) -> ( A |_| A ) ~<_ ( A X. A ) )
18		sdomdomtr	|- ( ( A ~< ( A |_| A ) /\ ( A |_| A ) ~<_ ( A X. A ) ) -> A ~< ( A X. A ) )
19	17 18	syldan	|- ( ( A ~< ( A |_| A ) /\ 2o ~<_ A ) -> A ~< ( A X. A ) )
20	19	ex	|- ( A ~< ( A |_| A ) -> ( 2o ~<_ A -> A ~< ( A X. A ) ) )
21	13 20	sylbird	|- ( A ~< ( A |_| A ) -> ( -. A ~< 2o -> A ~< ( A X. A ) ) )
22	21	orrd	|- ( A ~< ( A |_| A ) -> ( A ~< 2o \/ A ~< ( A X. A ) ) )
23	4 22	jaoi	|- ( ( A = (/) \/ A ~< ( A |_| A ) ) -> ( A ~< 2o \/ A ~< ( A X. A ) ) )
24		isfin5	|- ( A e. Fin5 <-> ( A = (/) \/ A ~< ( A |_| A ) ) )
25		isfin6	|- ( A e. Fin6 <-> ( A ~< 2o \/ A ~< ( A X. A ) ) )
26	23 24 25	3imtr4i	|- ( A e. Fin5 -> A e. Fin6 )