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

Theorem f1ss 6745
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 6739 . . 3 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
2 fss 6686 . . 3 ((𝐹:𝐴𝐵𝐵𝐶) → 𝐹:𝐴𝐶)
31, 2sylan 581 . 2 ((𝐹:𝐴1-1𝐵𝐵𝐶) → 𝐹:𝐴𝐶)
4 df-f1 6502 . . . 4 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
54simprbi 498 . . 3 (𝐹:𝐴1-1𝐵 → Fun 𝐹)
65adantr 482 . 2 ((𝐹:𝐴1-1𝐵𝐵𝐶) → Fun 𝐹)
7 df-f1 6502 . 2 (𝐹:𝐴1-1𝐶 ↔ (𝐹:𝐴𝐶 ∧ Fun 𝐹))
83, 6, 7sylanbrc 584 1 ((𝐹:𝐴1-1𝐵𝐵𝐶) → 𝐹:𝐴1-1𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wss 3911  ccnv 5633  Fun wfun 6491  wf 6493  1-1wf1 6494
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3448  df-in 3918  df-ss 3928  df-f 6501  df-f1 6502
This theorem is referenced by:  f1un  6805  f1sng  6827  f1prex  7231  domssr  8940  domssex2  9082  ssdomfi  9144  ssdomfi2  9145  1sdomOLD  9194  marypha1lem  9370  marypha2  9376  isinffi  9929  fseqenlem1  9961  dfac12r  10083  ackbij2  10180  cff1  10195  fin23lem28  10277  fin23lem41  10289  pwfseqlem5  10600  hashf1lem1  14354  hashf1lem1OLD  14355  gsumzres  19687  gsumzcl2  19688  gsumzf1o  19690  gsumzaddlem  19699  gsumzmhm  19715  gsumzoppg  19722  lindfres  21232  islindf3  21235  dvne0f1  25379  istrkg2ld  27405  ausgrusgrb  28119  uspgrushgr  28129  usgruspgr  28132  uspgr1e  28195  sizusglecusglem1  28412  s1f1  31802  s2f1  31804  qqhre  32604  erdsze2lem1  33800  eldioph2lem2  41087  eldioph2  41088  fundcmpsurbijinjpreimafv  45606  fundcmpsurinjimaid  45610
  Copyright terms: Public domain W3C validator