MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fnfi Structured version   Unicode version

Theorem fnfi 7859
Description: A version of fnex 6148 for finite sets that does not require Replacement. (Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro, 24-Jun-2015.)
Assertion
Ref Expression
fnfi  |-  ( ( F  Fn  A  /\  A  e.  Fin )  ->  F  e.  Fin )

Proof of Theorem fnfi
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fnresdm 5703 . . 3  |-  ( F  Fn  A  ->  ( F  |`  A )  =  F )
21adantr 466 . 2  |-  ( ( F  Fn  A  /\  A  e.  Fin )  ->  ( F  |`  A )  =  F )
3 reseq2 5119 . . . . . 6  |-  ( x  =  (/)  ->  ( F  |`  x )  =  ( F  |`  (/) ) )
43eleq1d 2491 . . . . 5  |-  ( x  =  (/)  ->  ( ( F  |`  x )  e.  Fin  <->  ( F  |`  (/) )  e.  Fin )
)
54imbi2d 317 . . . 4  |-  ( x  =  (/)  ->  ( ( ( F  Fn  A  /\  A  e.  Fin )  ->  ( F  |`  x )  e.  Fin ) 
<->  ( ( F  Fn  A  /\  A  e.  Fin )  ->  ( F  |`  (/) )  e.  Fin )
) )
6 reseq2 5119 . . . . . 6  |-  ( x  =  y  ->  ( F  |`  x )  =  ( F  |`  y
) )
76eleq1d 2491 . . . . 5  |-  ( x  =  y  ->  (
( F  |`  x
)  e.  Fin  <->  ( F  |`  y )  e.  Fin ) )
87imbi2d 317 . . . 4  |-  ( x  =  y  ->  (
( ( F  Fn  A  /\  A  e.  Fin )  ->  ( F  |`  x )  e.  Fin ) 
<->  ( ( F  Fn  A  /\  A  e.  Fin )  ->  ( F  |`  y )  e.  Fin ) ) )
9 reseq2 5119 . . . . . 6  |-  ( x  =  ( y  u. 
{ z } )  ->  ( F  |`  x )  =  ( F  |`  ( y  u.  { z } ) ) )
109eleq1d 2491 . . . . 5  |-  ( x  =  ( y  u. 
{ z } )  ->  ( ( F  |`  x )  e.  Fin  <->  ( F  |`  ( y  u. 
{ z } ) )  e.  Fin )
)
1110imbi2d 317 . . . 4  |-  ( x  =  ( y  u. 
{ z } )  ->  ( ( ( F  Fn  A  /\  A  e.  Fin )  ->  ( F  |`  x
)  e.  Fin )  <->  ( ( F  Fn  A  /\  A  e.  Fin )  ->  ( F  |`  ( y  u.  {
z } ) )  e.  Fin ) ) )
12 reseq2 5119 . . . . . 6  |-  ( x  =  A  ->  ( F  |`  x )  =  ( F  |`  A ) )
1312eleq1d 2491 . . . . 5  |-  ( x  =  A  ->  (
( F  |`  x
)  e.  Fin  <->  ( F  |`  A )  e.  Fin ) )
1413imbi2d 317 . . . 4  |-  ( x  =  A  ->  (
( ( F  Fn  A  /\  A  e.  Fin )  ->  ( F  |`  x )  e.  Fin ) 
<->  ( ( F  Fn  A  /\  A  e.  Fin )  ->  ( F  |`  A )  e.  Fin ) ) )
15 res0 5128 . . . . . 6  |-  ( F  |`  (/) )  =  (/)
16 0fin 7809 . . . . . 6  |-  (/)  e.  Fin
1715, 16eqeltri 2503 . . . . 5  |-  ( F  |`  (/) )  e.  Fin
1817a1i 11 . . . 4  |-  ( ( F  Fn  A  /\  A  e.  Fin )  ->  ( F  |`  (/) )  e. 
Fin )
19 resundi 5137 . . . . . . . 8  |-  ( F  |`  ( y  u.  {
z } ) )  =  ( ( F  |`  y )  u.  ( F  |`  { z } ) )
20 snfi 7661 . . . . . . . . . 10  |-  { <. z ,  ( F `  z ) >. }  e.  Fin
21 fnfun 5691 . . . . . . . . . . . 12  |-  ( F  Fn  A  ->  Fun  F )
22 funressn 6093 . . . . . . . . . . . 12  |-  ( Fun 
F  ->  ( F  |` 
{ z } ) 
C_  { <. z ,  ( F `  z ) >. } )
2321, 22syl 17 . . . . . . . . . . 11  |-  ( F  Fn  A  ->  ( F  |`  { z } )  C_  { <. z ,  ( F `  z ) >. } )
2423adantr 466 . . . . . . . . . 10  |-  ( ( F  Fn  A  /\  A  e.  Fin )  ->  ( F  |`  { z } )  C_  { <. z ,  ( F `  z ) >. } )
25 ssfi 7802 . . . . . . . . . 10  |-  ( ( { <. z ,  ( F `  z )
>. }  e.  Fin  /\  ( F  |`  { z } )  C_  { <. z ,  ( F `  z ) >. } )  ->  ( F  |`  { z } )  e.  Fin )
2620, 24, 25sylancr 667 . . . . . . . . 9  |-  ( ( F  Fn  A  /\  A  e.  Fin )  ->  ( F  |`  { z } )  e.  Fin )
27 unfi 7848 . . . . . . . . 9  |-  ( ( ( F  |`  y
)  e.  Fin  /\  ( F  |`  { z } )  e.  Fin )  ->  ( ( F  |`  y )  u.  ( F  |`  { z } ) )  e.  Fin )
2826, 27sylan2 476 . . . . . . . 8  |-  ( ( ( F  |`  y
)  e.  Fin  /\  ( F  Fn  A  /\  A  e.  Fin ) )  ->  (
( F  |`  y
)  u.  ( F  |`  { z } ) )  e.  Fin )
2919, 28syl5eqel 2511 . . . . . . 7  |-  ( ( ( F  |`  y
)  e.  Fin  /\  ( F  Fn  A  /\  A  e.  Fin ) )  ->  ( F  |`  ( y  u. 
{ z } ) )  e.  Fin )
3029expcom 436 . . . . . 6  |-  ( ( F  Fn  A  /\  A  e.  Fin )  ->  ( ( F  |`  y )  e.  Fin  ->  ( F  |`  (
y  u.  { z } ) )  e. 
Fin ) )
3130a2i 14 . . . . 5  |-  ( ( ( F  Fn  A  /\  A  e.  Fin )  ->  ( F  |`  y )  e.  Fin )  ->  ( ( F  Fn  A  /\  A  e.  Fin )  ->  ( F  |`  ( y  u. 
{ z } ) )  e.  Fin )
)
3231a1i 11 . . . 4  |-  ( y  e.  Fin  ->  (
( ( F  Fn  A  /\  A  e.  Fin )  ->  ( F  |`  y )  e.  Fin )  ->  ( ( F  Fn  A  /\  A  e.  Fin )  ->  ( F  |`  ( y  u. 
{ z } ) )  e.  Fin )
) )
335, 8, 11, 14, 18, 32findcard2 7821 . . 3  |-  ( A  e.  Fin  ->  (
( F  Fn  A  /\  A  e.  Fin )  ->  ( F  |`  A )  e.  Fin ) )
3433anabsi7 826 . 2  |-  ( ( F  Fn  A  /\  A  e.  Fin )  ->  ( F  |`  A )  e.  Fin )
352, 34eqeltrrd 2508 1  |-  ( ( F  Fn  A  /\  A  e.  Fin )  ->  F  e.  Fin )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437    e. wcel 1872    u. cun 3434    C_ wss 3436   (/)c0 3761   {csn 3998   <.cop 4004    |` cres 4855   Fun wfun 5595    Fn wfn 5596   ` cfv 5601   Fincfn 7581
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6598
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-reu 2778  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-int 4256  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6309  df-oprab 6310  df-mpt2 6311  df-om 6708  df-wrecs 7040  df-recs 7102  df-rdg 7140  df-1o 7194  df-oadd 7198  df-er 7375  df-en 7582  df-fin 7585
This theorem is referenced by:  fundmfibi  7865  unirnffid  7876  mptfi  7883  seqf1olem2  12260  seqf1o  12261  hashfzdm  12617  hashfirdm  12619  iswrdOLD  12678  wrdfin  12691  isstruct2  15130  xpsfrnel  15469  usgrafilem2  25139  cmpcref  28686  carsggect  29159  ptrecube  31905  ftc1anclem3  31984  sstotbnd2  32071  prdstotbnd  32091  ffi  37399  stoweidlem59  37861  fourierdlem42  37953  fourierdlem42OLD  37954  fourierdlem54  37965  resfnfinfin  38893
  Copyright terms: Public domain W3C validator