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

Theorem fores 6767
Description: Restriction of an onto function. (Contributed by NM, 4-Mar-1997.)
Assertion
Ref Expression
fores ((Fun 𝐹𝐴 ⊆ dom 𝐹) → (𝐹𝐴):𝐴onto→(𝐹𝐴))

Proof of Theorem fores
StepHypRef Expression
1 funres 6544 . . 3 (Fun 𝐹 → Fun (𝐹𝐴))
21anim1i 616 . 2 ((Fun 𝐹𝐴 ⊆ dom 𝐹) → (Fun (𝐹𝐴) ∧ 𝐴 ⊆ dom 𝐹))
3 df-fn 6500 . . 3 ((𝐹𝐴) Fn 𝐴 ↔ (Fun (𝐹𝐴) ∧ dom (𝐹𝐴) = 𝐴))
4 df-ima 5647 . . . . 5 (𝐹𝐴) = ran (𝐹𝐴)
54eqcomi 2746 . . . 4 ran (𝐹𝐴) = (𝐹𝐴)
6 df-fo 6503 . . . 4 ((𝐹𝐴):𝐴onto→(𝐹𝐴) ↔ ((𝐹𝐴) Fn 𝐴 ∧ ran (𝐹𝐴) = (𝐹𝐴)))
75, 6mpbiran2 709 . . 3 ((𝐹𝐴):𝐴onto→(𝐹𝐴) ↔ (𝐹𝐴) Fn 𝐴)
8 ssdmres 5961 . . . 4 (𝐴 ⊆ dom 𝐹 ↔ dom (𝐹𝐴) = 𝐴)
98anbi2i 624 . . 3 ((Fun (𝐹𝐴) ∧ 𝐴 ⊆ dom 𝐹) ↔ (Fun (𝐹𝐴) ∧ dom (𝐹𝐴) = 𝐴))
103, 7, 93bitr4i 303 . 2 ((𝐹𝐴):𝐴onto→(𝐹𝐴) ↔ (Fun (𝐹𝐴) ∧ 𝐴 ⊆ dom 𝐹))
112, 10sylibr 233 1 ((Fun 𝐹𝐴 ⊆ dom 𝐹) → (𝐹𝐴):𝐴onto→(𝐹𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wss 3911  dom cdm 5634  ran crn 5635  cres 5636  cima 5637  Fun wfun 6491   Fn wfn 6492  ontowfo 6495
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107  df-opab 5169  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-res 5646  df-ima 5647  df-fun 6499  df-fn 6500  df-fo 6503
This theorem is referenced by:  fimadmfoALT  6768  resdif  6806  f1oweALT  7906  imafiALT  9290  f1opwfi  9301  fodomfi2  9997  fin1a2lem7  10343  znnen  16095  connima  22779  1stcfb  22799  1stckgenlem  22907  qtoprest  23071  re2ndc  24167  uniiccdif  24945  opnmblALT  24970  mbfimaopnlem  25022  ffsrn  31649  cycpmconjvlem  31993  erdszelem2  33789  ivthALT  34810  poimirlem26  36107  poimirlem27  36108  lmhmfgima  41414
  Copyright terms: Public domain W3C validator