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

Theorem f1ss 6259
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 6254 . . 3 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
2 fss 6209 . . 3 ((𝐹:𝐴𝐵𝐵𝐶) → 𝐹:𝐴𝐶)
31, 2sylan 489 . 2 ((𝐹:𝐴1-1𝐵𝐵𝐶) → 𝐹:𝐴𝐶)
4 df-f1 6046 . . . 4 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
54simprbi 483 . . 3 (𝐹:𝐴1-1𝐵 → Fun 𝐹)
65adantr 472 . 2 ((𝐹:𝐴1-1𝐵𝐵𝐶) → Fun 𝐹)
7 df-f1 6046 . 2 (𝐹:𝐴1-1𝐶 ↔ (𝐹:𝐴𝐶 ∧ Fun 𝐹))
83, 6, 7sylanbrc 701 1 ((𝐹:𝐴1-1𝐵𝐵𝐶) → 𝐹:𝐴1-1𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wss 3707  ccnv 5257  Fun wfun 6035  wf 6037  1-1wf1 6038
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-in 3714  df-ss 3721  df-f 6045  df-f1 6046
This theorem is referenced by:  f1sng  6331  f1prex  6694  domssex2  8277  1sdom  8320  marypha1lem  8496  marypha2  8502  isinffi  9000  fseqenlem1  9029  dfac12r  9152  ackbij2  9249  cff1  9264  fin23lem28  9346  fin23lem41  9358  pwfseqlem5  9669  hashf1lem1  13423  gsumzres  18502  gsumzcl2  18503  gsumzf1o  18505  gsumzaddlem  18513  gsumzmhm  18529  gsumzoppg  18536  lindfres  20356  islindf3  20359  dvne0f1  23966  istrkg2ld  25550  ausgrusgrb  26251  uspgrushgr  26261  usgruspgr  26264  uspgr1e  26327  sizusglecusglem1  26559  qqhre  30365  erdsze2lem1  31484  eldioph2lem2  37818  eldioph2  37819
  Copyright terms: Public domain W3C validator