MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1ss Structured version   Visualization version   GIF version

Theorem f1ss 6319
Description: A function that is one-to-one is also one-to-one on some superset of its codomain. (Contributed by Mario Carneiro, 12-Jan-2013.)
Assertion
Ref Expression
f1ss ((𝐹:𝐴1-1𝐵𝐵𝐶) → 𝐹:𝐴1-1𝐶)

Proof of Theorem f1ss
StepHypRef Expression
1 f1f 6314 . . 3 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
2 fss 6267 . . 3 ((𝐹:𝐴𝐵𝐵𝐶) → 𝐹:𝐴𝐶)
31, 2sylan 576 . 2 ((𝐹:𝐴1-1𝐵𝐵𝐶) → 𝐹:𝐴𝐶)
4 df-f1 6104 . . . 4 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
54simprbi 491 . . 3 (𝐹:𝐴1-1𝐵 → Fun 𝐹)
65adantr 473 . 2 ((𝐹:𝐴1-1𝐵𝐵𝐶) → Fun 𝐹)
7 df-f1 6104 . 2 (𝐹:𝐴1-1𝐶 ↔ (𝐹:𝐴𝐶 ∧ Fun 𝐹))
83, 6, 7sylanbrc 579 1 ((𝐹:𝐴1-1𝐵𝐵𝐶) → 𝐹:𝐴1-1𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385  wss 3767  ccnv 5309  Fun wfun 6093  wf 6095  1-1wf1 6096
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2775
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-in 3774  df-ss 3781  df-f 6103  df-f1 6104
This theorem is referenced by:  f1sng  6395  f1prex  6765  domssex2  8360  1sdom  8403  marypha1lem  8579  marypha2  8585  isinffi  9102  fseqenlem1  9131  dfac12r  9254  ackbij2  9351  cff1  9366  fin23lem28  9448  fin23lem41  9460  pwfseqlem5  9771  hashf1lem1  13484  gsumzres  18622  gsumzcl2  18623  gsumzf1o  18625  gsumzaddlem  18633  gsumzmhm  18649  gsumzoppg  18656  lindfres  20484  islindf3  20487  dvne0f1  24113  istrkg2ld  25708  ausgrusgrb  26393  uspgrushgr  26403  usgruspgr  26406  uspgr1e  26470  sizusglecusglem1  26703  qqhre  30572  erdsze2lem1  31694  eldioph2lem2  38098  eldioph2  38099
  Copyright terms: Public domain W3C validator