This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 )