Theorem f1ss 6771

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

Syntax hints:   → wi 4   ∧ wa 400   ⊆ wss 3907  ^◡ccnv 5650  Fun wfun 6519  ⟶wf 6521  –1-1→wf1 6522

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ss 3924  df-f 6529  df-f1 6530

This theorem is referenced by:  f1un  6831  f1sng  6854  f1prex  7272  domssr  8984  domssex2  9113  ssdomfi  9168  ssdomfi2  9169  marypha1lem  9381  marypha2  9387  isinffi  9966  fseqenlem1  9996  dfac12r  10118  ackbij2  10213  cff1  10230  fin23lem28  10312  fin23lem41  10324  pwfseqlem5  10636  hashf1lem1  14480  gsumzres  19967  gsumzcl2  19968  gsumzf1o  19970  gsumzaddlem  19979  gsumzmhm  19995  gsumzoppg  20002  lindfres  21930  islindf3  21933  dvne0f1  26128  oldfib  28524  istrkg2ld  28683  ausgrusgrb  29420  uspgrushgr  29432  usgruspgr  29435  uspgr1e  29499  sizusglecusglem1  29716  s1f1  33171  s2f1  33173  qqhre  34322  erdsze2lem1  35561  eldioph2lem2  43349  eldioph2  43350  fundcmpsurbijinjpreimafv  48012  fundcmpsurinjimaid  48016  stgrusgra  48580  usgrexmpl1lem  48642  usgrexmpl2lem  48647  gpgusgra  48678