Metamath Proof Explorer


Theorem ssnnfiOLD

Description: Obsolete version of ssnnfi as of 23-Sep-2024. (Contributed by NM, 24-Jun-1998) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ssnnfiOLD
|- ( ( 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 enrefnn
 |-  ( 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 )