Theorem f1ores 6821

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 6769	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶–1-1→𝐵)
2		f1f1orn 6818	. . 3 ⊢ ((𝐹 ↾ 𝐶):𝐶–1-1→𝐵 → (𝐹 ↾ 𝐶):𝐶–1-1-onto→ran (𝐹 ↾ 𝐶))
3	1, 2	syl 17	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶–1-1-onto→ran (𝐹 ↾ 𝐶))
4		df-ima 5660	. . 3 ⊢ (𝐹 “ 𝐶) = ran (𝐹 ↾ 𝐶)
5		f1oeq3 6796	. . 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 399   = wceq 1560   ⊆ wss 3904  ran crn 5648   ↾ cres 5649   “ cima 5650  –1-1→wf1 6518  –1-1-onto→wf1o 6520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528

This theorem is referenced by:  f1imacnv  6823  f1oresrab  7109  f1ocoima  7287  isores3  7319  isoini2  7323  f1imaeng  8995  f1imaen2g  8996  f1imaen3g  8997  domunsncan  9049  ssfiALT  9142  f1imaenfi  9163  php3  9177  infdifsn  9612  infxpenlem  9969  ackbij2lem2  10195  fin1a2lem6  10362  grothomex  10787  fsumss  15752  ackbijnn  15858  fprodss  15978  unbenlem  16944  eqgen  19222  symgfixelsi  19475  gsumval3lem1  19945  gsumval3lem2  19946  gsumzaddlem  19961  lindsmm  21877  coe1mul2lem2  22328  tsmsf1o  24202  ovoliunlem1  25561  dvcnvrelem2  26077  logf1o2  26712  dvlog  26713  ushgredgedg  29427  ushgredgedgloop  29429  trlreslem  29895  adjbd1o  32285  rinvf1o  32829  padct  32917  hashimaf1  33010  indf1ofs  33041  eulerpartgbij  34666  eulerpartlemgh  34672  ballotlemfrc  34821  reprpmtf1o  34917  erdsze2lem2  35551  poimirlem4  38120  poimirlem9  38125  ismtyres  38304  pwfi2f1o  43670  sge0f1o  46953  3f1oss1  47666  f1oresf1o  47881  uhgrimisgrgric  48550