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

Metamath Proof Explorer

Theorem fin17

Description: Every I-finite set is VII-finite. (Contributed by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion fin17 
|- ( A e. Fin -> A e. Fin7 )

Proof

Step Hyp Ref Expression
1 eldif 
 |-  ( b e. ( On \ _om ) <-> ( b e. On /\ -. b e. _om ) )
2 enfi 
 |-  ( A ~~ b -> ( A e. Fin <-> b e. Fin ) )
3 onfin 
 |-  ( b e. On -> ( b e. Fin <-> b e. _om ) )
4 2 3 sylan9bbr 
 |-  ( ( b e. On /\ A ~~ b ) -> ( A e. Fin <-> b e. _om ) )
5 4 biimpd 
 |-  ( ( b e. On /\ A ~~ b ) -> ( A e. Fin -> b e. _om ) )
6 5 con3d 
 |-  ( ( b e. On /\ A ~~ b ) -> ( -. b e. _om -> -. A e. Fin ) )
7 6 impancom 
 |-  ( ( b e. On /\ -. b e. _om ) -> ( A ~~ b -> -. A e. Fin ) )
8 1 7 sylbi 
 |-  ( b e. ( On \ _om ) -> ( A ~~ b -> -. A e. Fin ) )
9 8 rexlimiv 
 |-  ( E. b e. ( On \ _om ) A ~~ b -> -. A e. Fin )
10 9 con2i 
 |-  ( A e. Fin -> -. E. b e. ( On \ _om ) A ~~ b )
11 isfin7 
 |-  ( A e. Fin -> ( A e. Fin7 <-> -. E. b e. ( On \ _om ) A ~~ b ) )
12 10 11 mpbird 
 |-  ( A e. Fin -> A e. Fin7 )