Theorem f1ores 6832

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 6780	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶–1-1→𝐵)
2		f1f1orn 6829	. . 3 ⊢ ((𝐹 ↾ 𝐶):𝐶–1-1→𝐵 → (𝐹 ↾ 𝐶):𝐶–1-1-onto→ran (𝐹 ↾ 𝐶))
3	1, 2	syl 18	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶–1-1-onto→ran (𝐹 ↾ 𝐶))
4		df-ima 5668	. . 3 ⊢ (𝐹 “ 𝐶) = ran (𝐹 ↾ 𝐶)
5		f1oeq3 6807	. . 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 1570   ⊆ wss 3899  ran crn 5656   ↾ cres 5657   “ cima 5658  –1-1→wf1 6530  –1-1-onto→wf1o 6532

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  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 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540

This theorem is used by:  f1imacnv  6834  f1oresrab  7121  f1ocoima  7304  isores3  7336  isoini2  7340  f1imaeng  9020  f1imaen2g  9021  f1imaen3g  9022  domunsncan  9075  ssfiALT  9168  f1imaenfi  9189  php3  9203  infdifsn  9636  infxpenlem  10016  ackbij2lem2  10241  fin1a2lem6  10407  grothomex  10838  fsumss  15811  ackbijnn  15917  fprodss  16035  unbenlem  17000  eqgen  19306  symgfixelsi  19562  gsumval3lem1  20032  gsumval3lem2  20033  gsumzaddlem  20048  lindsmm  22041  coe1mul2lem2  22494  tsmsf1o  24371  ovoliunlem1  25730  dvcnvrelem2  26245  logf1o2  26887  dvlog  26888  ushgredgedg  29689  ushgredgedgloop  29691  trlreslem  30161  adjbd1o  32566  rinvf1o  33103  padct  33189  hashimaf1  33281  indf1ofs  33312  eulerpartgbij  34883  eulerpartlemgh  34889  ballotlemfrc  35038  reprpmtf1o  35134  erdsze2lem2  35783  poimirlem4  38373  poimirlem9  38378  ismtyres  38558  pwfi2f1o  43937  sge0f1o  47210  3f1oss1  47963  f1oresf1o  48178  uhgrimisgrgric  48847