Metamath Proof Explorer

Theorem fin67

Description: Every VI-finite set is VII-finite. (Contributed by Stefan O'Rear, 29-Oct-2014) (Revised by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion fin67 
|- ( A e. Fin6 -> A e. Fin7 )

Proof

Step Hyp Ref Expression
1 isfin6 
 |-  ( A e. Fin6 <-> ( A ~< 2o \/ A ~< ( A X. A ) ) )
2 2onn 
 |-  2o e. _om
3 ssid 
 |-  2o C_ 2o
4 ssnnfi 
 |-  ( ( 2o e. _om /\ 2o C_ 2o ) -> 2o e. Fin )
5 2 3 4 mp2an 
 |-  2o e. Fin
6 sdomdom 
 |-  ( A ~< 2o -> A ~<_ 2o )
7 domfi 
 |-  ( ( 2o e. Fin /\ A ~<_ 2o ) -> A e. Fin )
8 5 6 7 sylancr 
 |-  ( A ~< 2o -> A e. Fin )
9 fin17 
 |-  ( A e. Fin -> A e. Fin7 )
10 8 9 syl 
 |-  ( A ~< 2o -> A e. Fin7 )
11 sdomnen 
 |-  ( A ~< ( A X. A ) -> -. A ~~ ( A X. A ) )
12 eldifi 
 |-  ( b e. ( On \ _om ) -> b e. On )
13 ensym 
 |-  ( A ~~ b -> b ~~ A )
14 isnumi 
 |-  ( ( b e. On /\ b ~~ A ) -> A e. dom card )
15 12 13 14 syl2an 
 |-  ( ( b e. ( On \ _om ) /\ A ~~ b ) -> A e. dom card )
16 vex 
 |-  b e. _V
17 eldif 
 |-  ( b e. ( On \ _om ) <-> ( b e. On /\ -. b e. _om ) )
18 ordom 
 |-  Ord _om
19 eloni 
 |-  ( b e. On -> Ord b )
20 ordtri1 
 |-  ( ( Ord _om /\ Ord b ) -> ( _om C_ b <-> -. b e. _om ) )
21 18 19 20 sylancr 
 |-  ( b e. On -> ( _om C_ b <-> -. b e. _om ) )
22 21 biimpar 
 |-  ( ( b e. On /\ -. b e. _om ) -> _om C_ b )
23 17 22 sylbi 
 |-  ( b e. ( On \ _om ) -> _om C_ b )
24 ssdomg 
 |-  ( b e. _V -> ( _om C_ b -> _om ~<_ b ) )
25 16 23 24 mpsyl 
 |-  ( b e. ( On \ _om ) -> _om ~<_ b )
26 domen2 
 |-  ( A ~~ b -> ( _om ~<_ A <-> _om ~<_ b ) )
27 25 26 imbitrrid 
 |-  ( A ~~ b -> ( b e. ( On \ _om ) -> _om ~<_ A ) )
28 27 impcom 
 |-  ( ( b e. ( On \ _om ) /\ A ~~ b ) -> _om ~<_ A )
29 infxpidm2 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( A X. A ) ~~ A )
30 15 28 29 syl2anc 
 |-  ( ( b e. ( On \ _om ) /\ A ~~ b ) -> ( A X. A ) ~~ A )
31 ensym 
 |-  ( ( A X. A ) ~~ A -> A ~~ ( A X. A ) )
32 30 31 syl 
 |-  ( ( b e. ( On \ _om ) /\ A ~~ b ) -> A ~~ ( A X. A ) )
33 32 rexlimiva 
 |-  ( E. b e. ( On \ _om ) A ~~ b -> A ~~ ( A X. A ) )
34 11 33 nsyl 
 |-  ( A ~< ( A X. A ) -> -. E. b e. ( On \ _om ) A ~~ b )
35 relsdom 
 |-  Rel ~<
36 35 brrelex1i 
 |-  ( A ~< ( A X. A ) -> A e. _V )
37 isfin7 
 |-  ( A e. _V -> ( A e. Fin7 <-> -. E. b e. ( On \ _om ) A ~~ b ) )
38 36 37 syl 
 |-  ( A ~< ( A X. A ) -> ( A e. Fin7 <-> -. E. b e. ( On \ _om ) A ~~ b ) )
39 34 38 mpbird 
 |-  ( A ~< ( A X. A ) -> A e. Fin7 )
40 10 39 jaoi 
 |-  ( ( A ~< 2o \/ A ~< ( A X. A ) ) -> A e. Fin7 )
41 1 40 sylbi 
 |-  ( A e. Fin6 -> A e. Fin7 )