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

Theorem fores 6367
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 6169 . . 3 (Fun 𝐹 → Fun (𝐹𝐴))
21anim1i 608 . 2 ((Fun 𝐹𝐴 ⊆ dom 𝐹) → (Fun (𝐹𝐴) ∧ 𝐴 ⊆ dom 𝐹))
3 df-fn 6130 . . 3 ((𝐹𝐴) Fn 𝐴 ↔ (Fun (𝐹𝐴) ∧ dom (𝐹𝐴) = 𝐴))
4 df-ima 5359 . . . . 5 (𝐹𝐴) = ran (𝐹𝐴)
54eqcomi 2834 . . . 4 ran (𝐹𝐴) = (𝐹𝐴)
6 df-fo 6133 . . . 4 ((𝐹𝐴):𝐴onto→(𝐹𝐴) ↔ ((𝐹𝐴) Fn 𝐴 ∧ ran (𝐹𝐴) = (𝐹𝐴)))
75, 6mpbiran2 701 . . 3 ((𝐹𝐴):𝐴onto→(𝐹𝐴) ↔ (𝐹𝐴) Fn 𝐴)
8 ssdmres 5660 . . . 4 (𝐴 ⊆ dom 𝐹 ↔ dom (𝐹𝐴) = 𝐴)
98anbi2i 616 . . 3 ((Fun (𝐹𝐴) ∧ 𝐴 ⊆ dom 𝐹) ↔ (Fun (𝐹𝐴) ∧ dom (𝐹𝐴) = 𝐴))
103, 7, 93bitr4i 295 . 2 ((𝐹𝐴):𝐴onto→(𝐹𝐴) ↔ (Fun (𝐹𝐴) ∧ 𝐴 ⊆ dom 𝐹))
112, 10sylibr 226 1 ((Fun 𝐹𝐴 ⊆ dom 𝐹) → (𝐹𝐴):𝐴onto→(𝐹𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386   = wceq 1656  wss 3798  dom cdm 5346  ran crn 5347  cres 5348  cima 5349  Fun wfun 6121   Fn wfn 6122  ontowfo 6125
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5007  ax-nul 5015  ax-pr 5129
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4147  df-if 4309  df-sn 4400  df-pr 4402  df-op 4406  df-br 4876  df-opab 4938  df-xp 5352  df-rel 5353  df-cnv 5354  df-co 5355  df-dm 5356  df-res 5358  df-ima 5359  df-fun 6129  df-fn 6130  df-fo 6133
This theorem is referenced by:  fimadmfoALT  6368  resdif  6402  f1oweALT  7417  imafi  8534  f1opwfi  8545  fodomfi2  9203  fin1a2lem7  9550  znnen  15322  connima  21606  1stcfb  21626  1stckgenlem  21734  qtoprest  21898  re2ndc  22981  uniiccdif  23751  opnmblALT  23776  mbfimaopnlem  23828  ffsrn  30048  erdszelem2  31716  ivthALT  32863  poimirlem26  33974  poimirlem27  33975  lmhmfgima  38492
  Copyright terms: Public domain W3C validator