Theorem f1ores 6796

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 6745	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶–1-1→𝐵)
2		f1f1orn 6793	. . 3 ⊢ ((𝐹 ↾ 𝐶):𝐶–1-1→𝐵 → (𝐹 ↾ 𝐶):𝐶–1-1-onto→ran (𝐹 ↾ 𝐶))
3	1, 2	syl 17	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶–1-1-onto→ran (𝐹 ↾ 𝐶))
4		df-ima 5645	. . 3 ⊢ (𝐹 “ 𝐶) = ran (𝐹 ↾ 𝐶)
5		f1oeq3 6772	. . 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 234	1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶–1-1-onto→(𝐹 “ 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ⊆ wss 3903  ran crn 5633   ↾ cres 5634   “ cima 5635  –1-1→wf1 6497  –1-1-onto→wf1o 6499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507

This theorem is referenced by:  f1imacnv  6798  f1oresrab  7082  f1ocoima  7259  isores3  7291  isoini2  7295  f1imaeng  8963  f1imaen2g  8964  f1imaen3g  8965  domunsncan  9017  ssfiALT  9110  f1imaenfi  9131  php3  9145  infdifsn  9578  infxpenlem  9935  ackbij2lem2  10161  fin1a2lem6  10327  grothomex  10752  fsumss  15660  ackbijnn  15763  fprodss  15883  unbenlem  16848  eqgen  19122  symgfixelsi  19376  gsumval3lem1  19846  gsumval3lem2  19847  gsumzaddlem  19862  lindsmm  21795  coe1mul2lem2  22222  tsmsf1o  24101  ovoliunlem1  25471  dvcnvrelem2  25991  logf1o2  26627  dvlog  26628  ushgredgedg  29314  ushgredgedgloop  29316  trlreslem  29783  adjbd1o  32173  rinvf1o  32720  padct  32808  hashimaf1  32902  indf1ofs  32959  eulerpartgbij  34550  eulerpartlemgh  34556  ballotlemfrc  34705  reprpmtf1o  34804  erdsze2lem2  35420  poimirlem4  37875  poimirlem9  37880  ismtyres  38059  pwfi2f1o  43453  sge0f1o  46740  3f1oss1  47435  f1oresf1o  47650  uhgrimisgrgric  48291