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

Theorem f1ss 6063
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 6058 . . 3 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
2 fss 6013 . . 3 ((𝐹:𝐴𝐵𝐵𝐶) → 𝐹:𝐴𝐶)
31, 2sylan 488 . 2 ((𝐹:𝐴1-1𝐵𝐵𝐶) → 𝐹:𝐴𝐶)
4 df-f1 5852 . . . 4 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
54simprbi 480 . . 3 (𝐹:𝐴1-1𝐵 → Fun 𝐹)
65adantr 481 . 2 ((𝐹:𝐴1-1𝐵𝐵𝐶) → Fun 𝐹)
7 df-f1 5852 . 2 (𝐹:𝐴1-1𝐶 ↔ (𝐹:𝐴𝐶 ∧ Fun 𝐹))
83, 6, 7sylanbrc 697 1 ((𝐹:𝐴1-1𝐵𝐵𝐶) → 𝐹:𝐴1-1𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wss 3555  ccnv 5073  Fun wfun 5841  wf 5843  1-1wf1 5844
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3562  df-ss 3569  df-f 5851  df-f1 5852
This theorem is referenced by:  f1sng  6135  f1prex  6493  domssex2  8064  1sdom  8107  marypha1lem  8283  marypha2  8289  isinffi  8762  fseqenlem1  8791  dfac12r  8912  ackbij2  9009  cff1  9024  fin23lem28  9106  fin23lem41  9118  pwfseqlem5  9429  hashf1lem1  13177  gsumzres  18231  gsumzcl2  18232  gsumzf1o  18234  gsumzaddlem  18242  gsumzmhm  18258  gsumzoppg  18265  lindfres  20081  islindf3  20084  dvne0f1  23679  istrkg2ld  25259  ausgrusgrb  25953  uspgrushgr  25963  usgruspgr  25966  uspgr1e  26029  sizusglecusglem1  26244  frgrncvvdeqlem8  27037  qqhre  29846  erdsze2lem1  30893  eldioph2lem2  36804  eldioph2  36805
  Copyright terms: Public domain W3C validator