MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imafi Structured version   Visualization version   GIF version

Theorem imafi 8809
Description: Images of finite sets are finite. (Contributed by Stefan O'Rear, 22-Feb-2015.)
Assertion
Ref Expression
imafi ((Fun 𝐹𝑋 ∈ Fin) → (𝐹𝑋) ∈ Fin)

Proof of Theorem imafi
StepHypRef Expression
1 imadmres 6084 . 2 (𝐹 “ dom (𝐹𝑋)) = (𝐹𝑋)
2 simpr 487 . . . 4 ((Fun 𝐹𝑋 ∈ Fin) → 𝑋 ∈ Fin)
3 dmres 5868 . . . . 5 dom (𝐹𝑋) = (𝑋 ∩ dom 𝐹)
4 inss1 4203 . . . . 5 (𝑋 ∩ dom 𝐹) ⊆ 𝑋
53, 4eqsstri 3999 . . . 4 dom (𝐹𝑋) ⊆ 𝑋
6 ssfi 8730 . . . 4 ((𝑋 ∈ Fin ∧ dom (𝐹𝑋) ⊆ 𝑋) → dom (𝐹𝑋) ∈ Fin)
72, 5, 6sylancl 588 . . 3 ((Fun 𝐹𝑋 ∈ Fin) → dom (𝐹𝑋) ∈ Fin)
8 resss 5871 . . . . 5 (𝐹𝑋) ⊆ 𝐹
9 dmss 5764 . . . . 5 ((𝐹𝑋) ⊆ 𝐹 → dom (𝐹𝑋) ⊆ dom 𝐹)
108, 9mp1i 13 . . . 4 ((Fun 𝐹𝑋 ∈ Fin) → dom (𝐹𝑋) ⊆ dom 𝐹)
11 fores 6593 . . . 4 ((Fun 𝐹 ∧ dom (𝐹𝑋) ⊆ dom 𝐹) → (𝐹 ↾ dom (𝐹𝑋)):dom (𝐹𝑋)–onto→(𝐹 “ dom (𝐹𝑋)))
1210, 11syldan 593 . . 3 ((Fun 𝐹𝑋 ∈ Fin) → (𝐹 ↾ dom (𝐹𝑋)):dom (𝐹𝑋)–onto→(𝐹 “ dom (𝐹𝑋)))
13 fofi 8802 . . 3 ((dom (𝐹𝑋) ∈ Fin ∧ (𝐹 ↾ dom (𝐹𝑋)):dom (𝐹𝑋)–onto→(𝐹 “ dom (𝐹𝑋))) → (𝐹 “ dom (𝐹𝑋)) ∈ Fin)
147, 12, 13syl2anc 586 . 2 ((Fun 𝐹𝑋 ∈ Fin) → (𝐹 “ dom (𝐹𝑋)) ∈ Fin)
151, 14eqeltrrid 2916 1 ((Fun 𝐹𝑋 ∈ Fin) → (𝐹𝑋) ∈ Fin)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  wcel 2107  cin 3933  wss 3934  dom cdm 5548  cres 5550  cima 5551  Fun wfun 6342  ontowfo 6346  Fincfn 8501
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-ral 3141  df-rex 3142  df-reu 3143  df-rab 3145  df-v 3495  df-sbc 3771  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-om 7573  df-1o 8094  df-er 8281  df-en 8502  df-dom 8503  df-fin 8505
This theorem is referenced by:  fissuni  8821  fipreima  8822  fsuppcolem  8856  cmpfi  22008  mdegldg  24652  mdegcl  24655  trlsegvdeglem6  27996  fsuppcurry1  30453  fsuppcurry2  30454  locfinreflem  31092  sibfof  31586  eulerpartlemgf  31625  poimirlem30  34909  ftc1anclem7  34960  ftc1anc  34962  elrfirn  39277  sge0f1o  42649
  Copyright terms: Public domain W3C validator