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

Theorem f1ss 6566
 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 6560 . . 3 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
2 fss 6512 . . 3 ((𝐹:𝐴𝐵𝐵𝐶) → 𝐹:𝐴𝐶)
31, 2sylan 583 . 2 ((𝐹:𝐴1-1𝐵𝐵𝐶) → 𝐹:𝐴𝐶)
4 df-f1 6340 . . . 4 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
54simprbi 500 . . 3 (𝐹:𝐴1-1𝐵 → Fun 𝐹)
65adantr 484 . 2 ((𝐹:𝐴1-1𝐵𝐵𝐶) → Fun 𝐹)
7 df-f1 6340 . 2 (𝐹:𝐴1-1𝐶 ↔ (𝐹:𝐴𝐶 ∧ Fun 𝐹))
83, 6, 7sylanbrc 586 1 ((𝐹:𝐴1-1𝐵𝐵𝐶) → 𝐹:𝐴1-1𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ⊆ wss 3858  ◡ccnv 5523  Fun wfun 6329  ⟶wf 6331  –1-1→wf1 6332 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3865  df-ss 3875  df-f 6339  df-f1 6340 This theorem is referenced by:  f1sng  6643  f1prex  7032  domssex2  8699  1sdom  8759  marypha1lem  8930  marypha2  8936  isinffi  9454  fseqenlem1  9484  dfac12r  9606  ackbij2  9703  cff1  9718  fin23lem28  9800  fin23lem41  9812  pwfseqlem5  10123  hashf1lem1  13864  hashf1lem1OLD  13865  gsumzres  19097  gsumzcl2  19098  gsumzf1o  19100  gsumzaddlem  19109  gsumzmhm  19125  gsumzoppg  19132  lindfres  20588  islindf3  20591  dvne0f1  24711  istrkg2ld  26353  ausgrusgrb  27057  uspgrushgr  27067  usgruspgr  27070  uspgr1e  27133  sizusglecusglem1  27350  s1f1  30741  s2f1  30743  qqhre  31489  erdsze2lem1  32681  eldioph2lem2  40097  eldioph2  40098  fundcmpsurbijinjpreimafv  44314  fundcmpsurinjimaid  44318
 Copyright terms: Public domain W3C validator