Theorem f1ores 6628

Description: The restriction of a one-to-one function maps one-to-one onto the image. (Contributed by NM, 25-Mar-1998.)

Assertion

Ref	Expression
f1ores	⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶–1-1-onto→(𝐹 “ 𝐶))

Proof of Theorem f1ores

Step	Hyp	Ref	Expression
1		f1ssres 6581	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶–1-1→𝐵)
2		f1f1orn 6625	. . 3 ⊢ ((𝐹 ↾ 𝐶):𝐶–1-1→𝐵 → (𝐹 ↾ 𝐶):𝐶–1-1-onto→ran (𝐹 ↾ 𝐶))
3	1, 2	syl 17	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶–1-1-onto→ran (𝐹 ↾ 𝐶))
4		df-ima 5567	. . 3 ⊢ (𝐹 “ 𝐶) = ran (𝐹 ↾ 𝐶)
5		f1oeq3 6605	. . 3 ⊢ ((𝐹 “ 𝐶) = ran (𝐹 ↾ 𝐶) → ((𝐹 ↾ 𝐶):𝐶–1-1-onto→(𝐹 “ 𝐶) ↔ (𝐹 ↾ 𝐶):𝐶–1-1-onto→ran (𝐹 ↾ 𝐶)))
6	4, 5	ax-mp 5	. 2 ⊢ ((𝐹 ↾ 𝐶):𝐶–1-1-onto→(𝐹 “ 𝐶) ↔ (𝐹 ↾ 𝐶):𝐶–1-1-onto→ran (𝐹 ↾ 𝐶))
7	3, 6	sylibr 236	1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶–1-1-onto→(𝐹 “ 𝐶))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1533   ⊆ wss 3935  ran crn 5555   ↾ cres 5556   “ cima 5557  –1-1→wf1 6351  –1-1-onto→wf1o 6353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pr 5329

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4567  df-pr 4569  df-op 4573  df-br 5066  df-opab 5128  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361

This theorem is referenced by:  f1imacnv  6630  f1oresrab  6888  isores3  7087  isoini2  7091  f1imaeng  8568  f1imaen2g  8569  domunsncan  8616  php3  8702  ssfi  8737  infdifsn  9119  infxpenlem  9438  ackbij2lem2  9661  fin1a2lem6  9826  grothomex  10250  fsumss  15081  ackbijnn  15182  fprodss  15301  unbenlem  16243  eqgen  18332  symgfixelsi  18562  gsumval3lem1  19024  gsumval3lem2  19025  gsumzaddlem  19040  coe1mul2lem2  20435  lindsmm  20971  tsmsf1o  22752  ovoliunlem1  24102  dvcnvrelem2  24614  logf1o2  25232  dvlog  25233  ushgredgedg  27010  ushgredgedgloop  27012  trlreslem  27480  adjbd1o  29861  rinvf1o  30374  padct  30454  indf1ofs  31285  eulerpartgbij  31630  eulerpartlemgh  31636  ballotlemfrc  31784  reprpmtf1o  31897  erdsze2lem2  32451  poimirlem4  34895  poimirlem9  34900  ismtyres  35085  pwfi2f1o  39694  sge0f1o  42663  f1oresf1o  43488