Theorem ssnnfi

Description: A subset of a natural number is finite. (Contributed by NM, 24-Jun-1998)

	Ref	Expression
Assertion	ssnnfi	|- ( ( A e. _om /\ B C_ A ) -> B e. Fin )

Proof

Step	Hyp	Ref	Expression
1		sspss	|- ( B C_ A <-> ( B C. A \/ B = A ) )
2		pssnn	|- ( ( A e. _om /\ B C. A ) -> E. x e. A B ~~ x )
3		elnn	|- ( ( x e. A /\ A e. _om ) -> x e. _om )
4	3	expcom	|- ( A e. _om -> ( x e. A -> x e. _om ) )
5	4	anim1d	|- ( A e. _om -> ( ( x e. A /\ B ~~ x ) -> ( x e. _om /\ B ~~ x ) ) )
6	5	reximdv2	|- ( A e. _om -> ( E. x e. A B ~~ x -> E. x e. _om B ~~ x ) )
7	6	adantr	|- ( ( A e. _om /\ B C. A ) -> ( E. x e. A B ~~ x -> E. x e. _om B ~~ x ) )
8	2 7	mpd	|- ( ( A e. _om /\ B C. A ) -> E. x e. _om B ~~ x )
9		eleq1	|- ( B = A -> ( B e. _om <-> A e. _om ) )
10	9	biimparc	|- ( ( A e. _om /\ B = A ) -> B e. _om )
11		enrefg	|- ( B e. _om -> B ~~ B )
12		breq2	|- ( x = B -> ( B ~~ x <-> B ~~ B ) )
13	12	rspcev	|- ( ( B e. _om /\ B ~~ B ) -> E. x e. _om B ~~ x )
14	10 11 13	syl2anc2	|- ( ( A e. _om /\ B = A ) -> E. x e. _om B ~~ x )
15	8 14	jaodan	|- ( ( A e. _om /\ ( B C. A \/ B = A ) ) -> E. x e. _om B ~~ x )
16	1 15	sylan2b	|- ( ( A e. _om /\ B C_ A ) -> E. x e. _om B ~~ x )
17		isfi	|- ( B e. Fin <-> E. x e. _om B ~~ x )
18	16 17	sylibr	|- ( ( A e. _om /\ B C_ A ) -> B e. Fin )