Theorem f1ores 6500

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 6453	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶–1-1→𝐵)
2		f1f1orn 6497	. . 3 ⊢ ((𝐹 ↾ 𝐶):𝐶–1-1→𝐵 → (𝐹 ↾ 𝐶):𝐶–1-1-onto→ran (𝐹 ↾ 𝐶))
3	1, 2	syl 17	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶–1-1-onto→ran (𝐹 ↾ 𝐶))
4		df-ima 5459	. . 3 ⊢ (𝐹 “ 𝐶) = ran (𝐹 ↾ 𝐶)
5		f1oeq3 6477	. . 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 235	1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶–1-1-onto→(𝐹 “ 𝐶))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1522   ⊆ wss 3861  ran crn 5447   ↾ cres 5448   “ cima 5449  –1-1→wf1 6225  –1-1-onto→wf1o 6227

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-ext 2768  ax-sep 5097  ax-nul 5104  ax-pr 5224

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1763  df-nf 1767  df-sb 2042  df-clab 2775  df-cleq 2787  df-clel 2862  df-nfc 2934  df-ral 3109  df-rex 3110  df-rab 3113  df-v 3438  df-dif 3864  df-un 3866  df-in 3868  df-ss 3876  df-nul 4214  df-if 4384  df-sn 4475  df-pr 4477  df-op 4481  df-br 4965  df-opab 5027  df-xp 5452  df-rel 5453  df-cnv 5454  df-co 5455  df-dm 5456  df-rn 5457  df-res 5458  df-ima 5459  df-fun 6230  df-fn 6231  df-f 6232  df-f1 6233  df-fo 6234  df-f1o 6235

This theorem is referenced by:  f1imacnv  6502  f1oresrab  6755  isores3  6954  isoini2  6958  f1imaeng  8420  f1imaen2g  8421  domunsncan  8467  php3  8553  ssfi  8587  infdifsn  8969  infxpenlem  9288  ackbij2lem2  9511  fin1a2lem6  9676  grothomex  10100  fsumss  14915  ackbijnn  15016  fprodss  15135  unbenlem  16073  eqgen  18086  symgfixelsi  18294  gsumval3lem1  18746  gsumval3lem2  18747  gsumzaddlem  18761  coe1mul2lem2  20119  lindsmm  20654  tsmsf1o  22436  ovoliunlem1  23786  dvcnvrelem2  24298  logf1o2  24914  dvlog  24915  ushgredgedg  26694  ushgredgedgloop  26696  trlreslem  27163  adjbd1o  29545  rinvf1o  30057  padct  30135  indf1ofs  30894  eulerpartgbij  31239  eulerpartlemgh  31245  ballotlemfrc  31393  reprpmtf1o  31506  erdsze2lem2  32053  poimirlem4  34440  poimirlem9  34445  ismtyres  34631  pwfi2f1o  39194  sge0f1o  42220  f1oresf1o  43019