Metamath Proof Explorer

Theorem ssnnfi

Description: A subset of a natural number is finite. (Contributed by NM, 24-Jun-1998) (Proof shortened by BTernaryTau, 23-Sep-2024)

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 isfi 
 |-  ( B e. Fin <-> E. x e. _om B ~~ x )
10 8 9 sylibr 
 |-  ( ( A e. _om /\ B C. A ) -> B e. Fin )
11 eleq1 
 |-  ( B = A -> ( B e. _om <-> A e. _om ) )
12 11 biimparc 
 |-  ( ( A e. _om /\ B = A ) -> B e. _om )
13 nnfi 
 |-  ( B e. _om -> B e. Fin )
14 12 13 syl 
 |-  ( ( A e. _om /\ B = A ) -> B e. Fin )
15 10 14 jaodan 
 |-  ( ( A e. _om /\ ( B C. A \/ B = A ) ) -> B e. Fin )
16 1 15 sylan2b 
 |-  ( ( A e. _om /\ B C_ A ) -> B e. Fin )