Metamath Proof Explorer


Theorem ssfi

Description: A subset of a finite set is finite. Corollary 6G of Enderton p. 138. (Contributed by NM, 24-Jun-1998)

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

Proof

Step Hyp Ref Expression
1 isfi
 |-  ( A e. Fin <-> E. x e. _om A ~~ x )
2 bren
 |-  ( A ~~ x <-> E. z z : A -1-1-onto-> x )
3 f1ofo
 |-  ( z : A -1-1-onto-> x -> z : A -onto-> x )
4 imassrn
 |-  ( z " B ) C_ ran z
5 forn
 |-  ( z : A -onto-> x -> ran z = x )
6 4 5 sseqtrid
 |-  ( z : A -onto-> x -> ( z " B ) C_ x )
7 3 6 syl
 |-  ( z : A -1-1-onto-> x -> ( z " B ) C_ x )
8 ssnnfi
 |-  ( ( x e. _om /\ ( z " B ) C_ x ) -> ( z " B ) e. Fin )
9 isfi
 |-  ( ( z " B ) e. Fin <-> E. y e. _om ( z " B ) ~~ y )
10 8 9 sylib
 |-  ( ( x e. _om /\ ( z " B ) C_ x ) -> E. y e. _om ( z " B ) ~~ y )
11 7 10 sylan2
 |-  ( ( x e. _om /\ z : A -1-1-onto-> x ) -> E. y e. _om ( z " B ) ~~ y )
12 11 adantrr
 |-  ( ( x e. _om /\ ( z : A -1-1-onto-> x /\ B C_ A ) ) -> E. y e. _om ( z " B ) ~~ y )
13 f1of1
 |-  ( z : A -1-1-onto-> x -> z : A -1-1-> x )
14 f1ores
 |-  ( ( z : A -1-1-> x /\ B C_ A ) -> ( z |` B ) : B -1-1-onto-> ( z " B ) )
15 13 14 sylan
 |-  ( ( z : A -1-1-onto-> x /\ B C_ A ) -> ( z |` B ) : B -1-1-onto-> ( z " B ) )
16 vex
 |-  z e. _V
17 16 resex
 |-  ( z |` B ) e. _V
18 f1oeq1
 |-  ( x = ( z |` B ) -> ( x : B -1-1-onto-> ( z " B ) <-> ( z |` B ) : B -1-1-onto-> ( z " B ) ) )
19 17 18 spcev
 |-  ( ( z |` B ) : B -1-1-onto-> ( z " B ) -> E. x x : B -1-1-onto-> ( z " B ) )
20 bren
 |-  ( B ~~ ( z " B ) <-> E. x x : B -1-1-onto-> ( z " B ) )
21 19 20 sylibr
 |-  ( ( z |` B ) : B -1-1-onto-> ( z " B ) -> B ~~ ( z " B ) )
22 entr
 |-  ( ( B ~~ ( z " B ) /\ ( z " B ) ~~ y ) -> B ~~ y )
23 21 22 sylan
 |-  ( ( ( z |` B ) : B -1-1-onto-> ( z " B ) /\ ( z " B ) ~~ y ) -> B ~~ y )
24 15 23 sylan
 |-  ( ( ( z : A -1-1-onto-> x /\ B C_ A ) /\ ( z " B ) ~~ y ) -> B ~~ y )
25 24 ex
 |-  ( ( z : A -1-1-onto-> x /\ B C_ A ) -> ( ( z " B ) ~~ y -> B ~~ y ) )
26 25 reximdv
 |-  ( ( z : A -1-1-onto-> x /\ B C_ A ) -> ( E. y e. _om ( z " B ) ~~ y -> E. y e. _om B ~~ y ) )
27 isfi
 |-  ( B e. Fin <-> E. y e. _om B ~~ y )
28 26 27 syl6ibr
 |-  ( ( z : A -1-1-onto-> x /\ B C_ A ) -> ( E. y e. _om ( z " B ) ~~ y -> B e. Fin ) )
29 28 adantl
 |-  ( ( x e. _om /\ ( z : A -1-1-onto-> x /\ B C_ A ) ) -> ( E. y e. _om ( z " B ) ~~ y -> B e. Fin ) )
30 12 29 mpd
 |-  ( ( x e. _om /\ ( z : A -1-1-onto-> x /\ B C_ A ) ) -> B e. Fin )
31 30 exp32
 |-  ( x e. _om -> ( z : A -1-1-onto-> x -> ( B C_ A -> B e. Fin ) ) )
32 31 exlimdv
 |-  ( x e. _om -> ( E. z z : A -1-1-onto-> x -> ( B C_ A -> B e. Fin ) ) )
33 2 32 syl5bi
 |-  ( x e. _om -> ( A ~~ x -> ( B C_ A -> B e. Fin ) ) )
34 33 rexlimiv
 |-  ( E. x e. _om A ~~ x -> ( B C_ A -> B e. Fin ) )
35 1 34 sylbi
 |-  ( A e. Fin -> ( B C_ A -> B e. Fin ) )
36 35 imp
 |-  ( ( A e. Fin /\ B C_ A ) -> B e. Fin )