Theorem ssfiOLD

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

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