Theorem ssnnfi 7673

Description: A subset of a natural number is finite. (Contributed by NM, 24-Jun-1998.)

Assertion

Ref	Expression
ssnnfi	|- ( ( A e. om /\ B C_ A ) -> B e. Fin )

Proof of Theorem ssnnfi

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sspss 3530	. . 3 |- ( B C_ A <-> ( B C. A \/ B = A ) )
2		pssnn 7672	. . . . 5 |- ( ( A e. om /\ B C. A ) -> E. x e. A B ~~ x )
3		elnn 6627	. . . . . . . . 9 |- ( ( x e. A /\ A e. om ) -> x e. om )
4	3	expcom 433	. . . . . . . 8 |- ( A e. om -> ( x e. A -> x e. om ) )
5	4	anim1d 562	. . . . . . 7 |- ( A e. om -> ( ( x e. A /\ B ~~ x ) -> ( x e. om /\ B ~~ x ) ) )
6	5	reximdv2 2863	. . . . . 6 |- ( A e. om -> ( E. x e. A B ~~ x -> E. x e. om B ~~ x ) )
7	6	adantr 463	. . . . 5 |- ( ( A e. om /\ B C. A ) -> ( E. x e. A B ~~ x -> E. x e. om B ~~ x ) )
8	2, 7	mpd 15	. . . 4 |- ( ( A e. om /\ B C. A ) -> E. x e. om B ~~ x )
9		eleq1 2464	. . . . . 6 |- ( B = A -> ( B e. om <-> A e. om ) )
10	9	biimparc 485	. . . . 5 |- ( ( A e. om /\ B = A ) -> B e. om )
11		enrefg 7484	. . . . . 6 |- ( B e. om -> B ~~ B )
12	11	ancli 549	. . . . 5 |- ( B e. om -> ( B e. om /\ B ~~ B ) )
13		breq2 4384	. . . . . 6 |- ( x = B -> ( B ~~ x <-> B ~~ B ) )
14	13	rspcev 3148	. . . . 5 |- ( ( B e. om /\ B ~~ B ) -> E. x e. om B ~~ x )
15	10, 12, 14	3syl 20	. . . 4 |- ( ( A e. om /\ B = A ) -> E. x e. om B ~~ x )
16	8, 15	jaodan 783	. . 3 |- ( ( A e. om /\ ( B C. A \/ B = A ) ) -> E. x e. om B ~~ x )
17	1, 16	sylan2b 473	. 2 |- ( ( A e. om /\ B C_ A ) -> E. x e. om B ~~ x )
18		isfi 7476	. 2 |- ( B e. Fin <-> E. x e. om B ~~ x )
19	17, 18	sylibr 212	1 |- ( ( A e. om /\ B C_ A ) -> B e. Fin )

Syntax hints:   -> wi 4   \/ wo 366   /\ wa 367   = wceq 1399   e. wcel 1836   E.wrex 2743   C_ wss 3402   C. wpss 3403   class class class wbr 4380   omcom 6617   ~~ cen 7450   Fincfn 7453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-sep 4501  ax-nul 4509  ax-pow 4556  ax-pr 4614  ax-un 6509

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-ral 2747  df-rex 2748  df-rab 2751  df-v 3049  df-sbc 3266  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-pss 3418  df-nul 3725  df-if 3871  df-pw 3942  df-sn 3958  df-pr 3960  df-tp 3962  df-op 3964  df-uni 4177  df-br 4381  df-opab 4439  df-tr 4474  df-eprel 4718  df-id 4722  df-po 4727  df-so 4728  df-fr 4765  df-we 4767  df-ord 4808  df-on 4809  df-lim 4810  df-suc 4811  df-xp 4932  df-rel 4933  df-cnv 4934  df-co 4935  df-dm 4936  df-rn 4937  df-res 4938  df-ima 4939  df-fun 5511  df-fn 5512  df-f 5513  df-f1 5514  df-fo 5515  df-f1o 5516  df-om 6618  df-en 7454  df-fin 7457

This theorem is referenced by:  ssfi  7674  0fin  7681  en1eqsn  7683  isfinite2  7711  pwfi  7748  wofib  7903  infpwfien  8374  fin67  8706  hashcard  12348  rexpen  13982