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

Theorem f1ss 6019
 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 6014 . . 3 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
2 fss 5969 . . 3 ((𝐹:𝐴𝐵𝐵𝐶) → 𝐹:𝐴𝐶)
31, 2sylan 487 . 2 ((𝐹:𝐴1-1𝐵𝐵𝐶) → 𝐹:𝐴𝐶)
4 df-f1 5809 . . . 4 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
54simprbi 479 . . 3 (𝐹:𝐴1-1𝐵 → Fun 𝐹)
65adantr 480 . 2 ((𝐹:𝐴1-1𝐵𝐵𝐶) → Fun 𝐹)
7 df-f1 5809 . 2 (𝐹:𝐴1-1𝐶 ↔ (𝐹:𝐴𝐶 ∧ Fun 𝐹))
83, 6, 7sylanbrc 695 1 ((𝐹:𝐴1-1𝐵𝐵𝐶) → 𝐹:𝐴1-1𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ⊆ wss 3540  ◡ccnv 5037  Fun wfun 5798  ⟶wf 5800  –1-1→wf1 5801 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554  df-f 5808  df-f1 5809 This theorem is referenced by:  f1sng  6090  f1prex  6439  domssex2  8005  1sdom  8048  marypha1lem  8222  marypha2  8228  isinffi  8701  fseqenlem1  8730  dfac12r  8851  ackbij2  8948  cff1  8963  fin23lem28  9045  fin23lem41  9057  pwfseqlem5  9364  hashf1lem1  13096  gsumzres  18133  gsumzcl2  18134  gsumzf1o  18136  gsumzaddlem  18144  gsumzmhm  18160  gsumzoppg  18167  lindfres  19981  islindf3  19984  dvne0f1  23579  istrkg2ld  25159  ausisusgra  25884  uslisushgra  25892  usisuslgra  25894  uslgra1  25901  usgra1  25902  sizeusglecusglem1  26012  2trllemE  26083  constr1trl  26118  frgrancvvdeqlem8  26567  qqhre  29392  erdsze2lem1  30439  eldioph2lem2  36342  eldioph2  36343  ausgrusgrb  40395  uspgrushgr  40405  usgruspgr  40408  uspgr1e  40470  sizusglecusglem1  40677  frgrncvvdeqlem8  41479
 Copyright terms: Public domain W3C validator