Metamath Proof Explorer

Theorem ssfiALT

Description: Shorter proof of ssfi using ax-pow . (Contributed by NM, 24-Jun-1998) (Proof modification is discouraged.) (New usage is discouraged.)

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