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

Theorem f1ss 6809
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 6804 . . 3 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
2 fss 6752 . . 3 ((𝐹:𝐴𝐵𝐵𝐶) → 𝐹:𝐴𝐶)
31, 2sylan 580 . 2 ((𝐹:𝐴1-1𝐵𝐵𝐶) → 𝐹:𝐴𝐶)
4 df-f1 6566 . . . 4 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
54simprbi 496 . . 3 (𝐹:𝐴1-1𝐵 → Fun 𝐹)
65adantr 480 . 2 ((𝐹:𝐴1-1𝐵𝐵𝐶) → Fun 𝐹)
7 df-f1 6566 . 2 (𝐹:𝐴1-1𝐶 ↔ (𝐹:𝐴𝐶 ∧ Fun 𝐹))
83, 6, 7sylanbrc 583 1 ((𝐹:𝐴1-1𝐵𝐵𝐶) → 𝐹:𝐴1-1𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wss 3951  ccnv 5684  Fun wfun 6555  wf 6557  1-1wf1 6558
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809
This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3968  df-f 6565  df-f1 6566
This theorem is referenced by:  f1un  6868  f1sng  6890  f1prex  7304  domssr  9039  domssex2  9177  ssdomfi  9236  ssdomfi2  9237  1sdomOLD  9285  marypha1lem  9473  marypha2  9479  isinffi  10032  fseqenlem1  10064  dfac12r  10187  ackbij2  10282  cff1  10298  fin23lem28  10380  fin23lem41  10392  pwfseqlem5  10703  hashf1lem1  14494  gsumzres  19927  gsumzcl2  19928  gsumzf1o  19930  gsumzaddlem  19939  gsumzmhm  19955  gsumzoppg  19962  lindfres  21843  islindf3  21846  dvne0f1  26051  istrkg2ld  28468  ausgrusgrb  29182  uspgrushgr  29194  usgruspgr  29197  uspgr1e  29261  sizusglecusglem1  29479  s1f1  32927  s2f1  32929  qqhre  34021  erdsze2lem1  35208  eldioph2lem2  42772  eldioph2  42773  fundcmpsurbijinjpreimafv  47394  fundcmpsurinjimaid  47398  stgrusgra  47926  usgrexmpl1lem  47980  usgrexmpl2lem  47985  gpgusgra  48012
  Copyright terms: Public domain W3C validator