Theorem f1ss 6724

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3902  ^◡ccnv 5615  Fun wfun 6475  ⟶wf 6477  –1-1→wf1 6478

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3919  df-f 6485  df-f1 6486

This theorem is referenced by:  f1un  6783  f1sng  6805  f1prex  7218  domssr  8921  domssex2  9050  ssdomfi  9105  ssdomfi2  9106  marypha1lem  9317  marypha2  9323  isinffi  9885  fseqenlem1  9915  dfac12r  10038  ackbij2  10133  cff1  10149  fin23lem28  10231  fin23lem41  10243  pwfseqlem5  10554  hashf1lem1  14362  gsumzres  19822  gsumzcl2  19823  gsumzf1o  19825  gsumzaddlem  19834  gsumzmhm  19850  gsumzoppg  19857  lindfres  21761  islindf3  21764  dvne0f1  25945  istrkg2ld  28439  ausgrusgrb  29144  uspgrushgr  29156  usgruspgr  29159  uspgr1e  29223  sizusglecusglem1  29441  s1f1  32922  s2f1  32924  qqhre  34031  erdsze2lem1  35245  eldioph2lem2  42800  eldioph2  42801  fundcmpsurbijinjpreimafv  47444  fundcmpsurinjimaid  47448  stgrusgra  47996  usgrexmpl1lem  48058  usgrexmpl2lem  48063  gpgusgra  48094