Theorem f1ores 6847

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 6795	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶–1-1→𝐵)
2		f1f1orn 6844	. . 3 ⊢ ((𝐹 ↾ 𝐶):𝐶–1-1→𝐵 → (𝐹 ↾ 𝐶):𝐶–1-1-onto→ran (𝐹 ↾ 𝐶))
3	1, 2	syl 18	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶–1-1-onto→ran (𝐹 ↾ 𝐶))
4		df-ima 5667	. . 3 ⊢ (𝐹 “ 𝐶) = ran (𝐹 ↾ 𝐶)
5		f1oeq3 6822	. . 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 237	1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶–1-1-onto→(𝐹 “ 𝐶))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ⊆ wss 3899  ran crn 5655   ↾ cres 5656   “ cima 5657  –1-1→wf1 6543  –1-1-onto→wf1o 6545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-sep 5251  ax-pr 5394

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-br 5106  df-opab 5170  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553

This theorem is used by:  f1imacnv  6849  f1oresrab  7136  f1ocoima  7318  isores3  7350  isoini2  7354  f1imaeng  9052  f1imaen2g  9053  f1imaen3g  9054  domunsncan  9107  ssfiALT  9200  f1imaenfi  9221  php3  9235  infdifsn  9668  infxpenlem  10102  ackbij2lem2  10327  fin1a2lem6  10493  grothomex  10924  fsumss  15903  ackbijnn  16009  fprodss  16127  unbenlem  17098  eqgen  19405  symgfixelsi  19661  gsumval3lem1  20131  gsumval3lem2  20132  gsumzaddlem  20147  lindsmm  22146  coe1mul2lem2  22599  tsmsf1o  24476  ovoliunlem1  25835  dvcnvrelem2  26350  logf1o2  26990  dvlog  26991  ushgredgedg  29822  ushgredgedgloop  29824  trlreslem  30294  adjbd1o  32699  rinvf1o  33278  padct  33364  hashimaf1  33455  indf1ofs  33486  eulerpartgbij  35057  eulerpartlemgh  35063  ballotlemfrc  35212  reprpmtf1o  35308  vonf1onprcf1ac  35998  erdsze2lem2  36090  poimirlem4  38682  poimirlem9  38687  ismtyres  38882  pwfi2f1o  44238  sge0f1o  47531  3f1oss1  48284  f1oresf1o  48499  uhgrimisgrgric  49168