Theorem f1ss 6676

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

Step	Hyp	Ref	Expression
1		f1f 6670	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
2		fss 6617	. . 3 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
3	1, 2	sylan 580	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
4		df-f1 6438	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
5	4	simprbi 497	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
6	5	adantr 481	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → Fun ◡𝐹)
7		df-f1 6438	. 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹))
8	3, 6, 7	sylanbrc 583	1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴–1-1→𝐶)

Syntax hints:   → wi 4   ∧ wa 396   ⊆ wss 3887  ^◡ccnv 5588  Fun wfun 6427  ⟶wf 6429  –1-1→wf1 6430

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-f 6437  df-f1 6438

This theorem is referenced by:  f1un  6736  f1sng  6758  f1prex  7156  domssex2  8924  ssdomfi  8982  ssdomfi2  8983  1sdom  9025  marypha1lem  9192  marypha2  9198  isinffi  9750  fseqenlem1  9780  dfac12r  9902  ackbij2  9999  cff1  10014  fin23lem28  10096  fin23lem41  10108  pwfseqlem5  10419  hashf1lem1  14168  hashf1lem1OLD  14169  gsumzres  19510  gsumzcl2  19511  gsumzf1o  19513  gsumzaddlem  19522  gsumzmhm  19538  gsumzoppg  19545  lindfres  21030  islindf3  21033  dvne0f1  25176  istrkg2ld  26821  ausgrusgrb  27535  uspgrushgr  27545  usgruspgr  27548  uspgr1e  27611  sizusglecusglem1  27828  s1f1  31217  s2f1  31219  qqhre  31970  erdsze2lem1  33165  eldioph2lem2  40583  eldioph2  40584  fundcmpsurbijinjpreimafv  44859  fundcmpsurinjimaid  44863