Theorem f1ss 6660

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 6654	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
2		fss 6601	. . 3 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
3	1, 2	sylan 579	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
4		df-f1 6423	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
5	4	simprbi 496	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
6	5	adantr 480	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → Fun ◡𝐹)
7		df-f1 6423	. 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹))
8	3, 6, 7	sylanbrc 582	1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴–1-1→𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3883  ^◡ccnv 5579  Fun wfun 6412  ⟶wf 6414  –1-1→wf1 6415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-f 6422  df-f1 6423

This theorem is referenced by:  f1sng  6741  f1prex  7136  domssex2  8873  ssdomfi  8940  1sdom  8955  marypha1lem  9122  marypha2  9128  isinffi  9681  fseqenlem1  9711  dfac12r  9833  ackbij2  9930  cff1  9945  fin23lem28  10027  fin23lem41  10039  pwfseqlem5  10350  hashf1lem1  14096  hashf1lem1OLD  14097  gsumzres  19425  gsumzcl2  19426  gsumzf1o  19428  gsumzaddlem  19437  gsumzmhm  19453  gsumzoppg  19460  lindfres  20940  islindf3  20943  dvne0f1  25081  istrkg2ld  26725  ausgrusgrb  27438  uspgrushgr  27448  usgruspgr  27451  uspgr1e  27514  sizusglecusglem1  27731  s1f1  31119  s2f1  31121  qqhre  31870  erdsze2lem1  33065  eldioph2lem2  40499  eldioph2  40500  fundcmpsurbijinjpreimafv  44747  fundcmpsurinjimaid  44751