Theorem f1ss 6783

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 6776	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
2		fss 6724	. . 3 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
3	1, 2	sylan 591	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
4		df-f1 6543	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
5	4	simprbi 502	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
6	5	adantr 485	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → Fun ◡𝐹)
7		df-f1 6543	. 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹))
8	3, 6, 7	sylanbrc 594	1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴–1-1→𝐶)

Syntax hints:   → wi 4   ∧ wa 400   ⊆ wss 3906  ^◡ccnv 5662  Fun wfun 6532  ⟶wf 6534  –1-1→wf1 6535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839

This theorem depends on definitions:  df-bi 210  df-an 401  df-ss 3923  df-f 6542  df-f1 6543

This theorem is referenced by:  f1un  6843  f1sng  6866  f1prex  7284  domssr  8997  domssex2  9126  ssdomfi  9181  ssdomfi2  9182  marypha1lem  9394  marypha2  9400  isinffi  9979  fseqenlem1  10009  dfac12r  10131  ackbij2  10226  cff1  10243  fin23lem28  10325  fin23lem41  10337  pwfseqlem5  10649  hashf1lem1  14494  gsumzres  19980  gsumzcl2  19981  gsumzf1o  19983  gsumzaddlem  19992  gsumzmhm  20008  gsumzoppg  20015  lindfres  21954  islindf3  21957  dvne0f1  26152  oldfib  28551  istrkg2ld  28710  ausgrusgrb  29496  uspgrushgr  29508  usgruspgr  29511  uspgr1e  29575  sizusglecusglem1  29792  s1f1  33244  s2f1  33246  qqhre  34391  erdsze2lem1  35676  eldioph2lem2  43475  eldioph2  43476  fundcmpsurbijinjpreimafv  48139  fundcmpsurinjimaid  48143  stgrusgra  48707  usgrexmpl1lem  48769  usgrexmpl2lem  48774  gpgusgra  48805