Theorem f1ores 6629

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 6582	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶–1-1→𝐵)
2		f1f1orn 6626	. . 3 ⊢ ((𝐹 ↾ 𝐶):𝐶–1-1→𝐵 → (𝐹 ↾ 𝐶):𝐶–1-1-onto→ran (𝐹 ↾ 𝐶))
3	1, 2	syl 17	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶–1-1-onto→ran (𝐹 ↾ 𝐶))
4		df-ima 5568	. . 3 ⊢ (𝐹 “ 𝐶) = ran (𝐹 ↾ 𝐶)
5		f1oeq3 6606	. . 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 1537   ⊆ wss 3936  ran crn 5556   ↾ cres 5557   “ cima 5558  –1-1→wf1 6352  –1-1-onto→wf1o 6354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  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 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362

This theorem is referenced by:  f1imacnv  6631  f1oresrab  6889  isores3  7088  isoini2  7092  f1imaeng  8569  f1imaen2g  8570  domunsncan  8617  php3  8703  ssfi  8738  infdifsn  9120  infxpenlem  9439  ackbij2lem2  9662  fin1a2lem6  9827  grothomex  10251  fsumss  15082  ackbijnn  15183  fprodss  15302  unbenlem  16244  eqgen  18333  symgfixelsi  18563  gsumval3lem1  19025  gsumval3lem2  19026  gsumzaddlem  19041  coe1mul2lem2  20436  lindsmm  20972  tsmsf1o  22753  ovoliunlem1  24103  dvcnvrelem2  24615  logf1o2  25233  dvlog  25234  ushgredgedg  27011  ushgredgedgloop  27013  trlreslem  27481  adjbd1o  29862  rinvf1o  30375  padct  30455  indf1ofs  31285  eulerpartgbij  31630  eulerpartlemgh  31636  ballotlemfrc  31784  reprpmtf1o  31897  erdsze2lem2  32451  poimirlem4  34911  poimirlem9  34916  ismtyres  35101  pwfi2f1o  39716  sge0f1o  42684  f1oresf1o  43509