Theorem f1ss 6735

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3901  ^◡ccnv 5623  Fun wfun 6486  ⟶wf 6488  –1-1→wf1 6489

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 3918  df-f 6496  df-f1 6497

This theorem is referenced by:  f1un  6794  f1sng  6817  f1prex  7230  domssr  8936  domssex2  9065  ssdomfi  9120  ssdomfi2  9121  marypha1lem  9336  marypha2  9342  isinffi  9904  fseqenlem1  9934  dfac12r  10057  ackbij2  10152  cff1  10168  fin23lem28  10250  fin23lem41  10262  pwfseqlem5  10574  hashf1lem1  14378  gsumzres  19838  gsumzcl2  19839  gsumzf1o  19841  gsumzaddlem  19850  gsumzmhm  19866  gsumzoppg  19873  lindfres  21778  islindf3  21781  dvne0f1  25973  oldfib  28373  istrkg2ld  28532  ausgrusgrb  29238  uspgrushgr  29250  usgruspgr  29253  uspgr1e  29317  sizusglecusglem1  29535  s1f1  33025  s2f1  33027  qqhre  34177  erdsze2lem1  35397  eldioph2lem2  43003  eldioph2  43004  fundcmpsurbijinjpreimafv  47653  fundcmpsurinjimaid  47657  stgrusgra  48205  usgrexmpl1lem  48267  usgrexmpl2lem  48272  gpgusgra  48303