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 )