Theorem f1ores 6869

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-1onto(𝐹 “ 𝐶))

Proof of Theorem f1ores

Step	Hyp	Ref	Expression
1		f1ssres 6817	. . 3 ⊢ ((𝐹:𝐴⟶1-1𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶1-1𝐵)
2		f1f1orn 6866	. . 3 ⊢ ((𝐹 ↾ 𝐶):𝐶⟶1-1𝐵 → (𝐹 ↾ 𝐶):𝐶⟶1-1ontoran (𝐹 ↾ 𝐶))
3	1, 2	syl 18	. 2 ⊢ ((𝐹:𝐴⟶1-1𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶1-1ontoran (𝐹 ↾ 𝐶))
4		df-ima 5671	. . 3 ⊢ (𝐹 “ 𝐶) = ran (𝐹 ↾ 𝐶)
5		f1oeq3 6844	. . 3 ⊢ ((𝐹 “ 𝐶) = ran (𝐹 ↾ 𝐶) → ((𝐹 ↾ 𝐶):𝐶⟶1-1onto(𝐹 “ 𝐶) ↔ (𝐹 ↾ 𝐶):𝐶⟶1-1ontoran (𝐹 ↾ 𝐶)))
6	4, 5	ax-mp 5	. 2 ⊢ ((𝐹 ↾ 𝐶):𝐶⟶1-1onto(𝐹 “ 𝐶) ↔ (𝐹 ↾ 𝐶):𝐶⟶1-1ontoran (𝐹 ↾ 𝐶))
7	3, 6	sylibr 237	1 ⊢ ((𝐹:𝐴⟶1-1𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶1-1onto(𝐹 “ 𝐶))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ⊆ wss 3900  ran crn 5659   ↾ cres 5660   “ cima 5661  ⟶1-1wf1 6563  ⟶1-1ontowf1o 6565

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573

This theorem is used by:  f1imacnv  6871  f1oresrab  7160  f1ocoima  7342  isores3  7374  isoini2  7378  f1imaeng  9079  f1imaen2g  9080  f1imaen3g  9081  domunsncan  9134  ssfiALT  9227  f1imaenfi  9248  php3  9262  infdifsn  9695  infxpenlem  10131  ackbij2lem2  10356  fin1a2lem6  10522  grothomex  10953  fsumss  15935  ackbijnn  16041  fprodss  16159  unbenlem  17130  eqgen  19443  symgfixelsi  19700  gsumval3lem1  20170  gsumval3lem2  20171  gsumzaddlem  20186  lindsmm  22189  coe1mul2lem2  22642  tsmsf1o  24519  ovoliunlem1  25878  dvcnvrelem2  26393  logf1o2  27035  dvlog  27036  ushgredgedg  29867  ushgredgedgloop  29869  trlreslem  30339  adjbd1o  32744  rinvf1o  33322  padct  33407  hashimaf1  33498  indf1ofs  33529  eulerpartgbij  35115  eulerpartlemgh  35121  ballotlemfrc  35270  reprpmtf1o  35366  vonf1onprcf1ac  36085  erdsze2lem2  36177  poimirlem4  38810  poimirlem9  38815  ismtyres  39008  pwfi2f1o  44364  sge0f1o  47665  3f1oss1  48418  f1oresf1o  48633  uhgrimisgrgric  49302