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 586	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
4		df-f1 6497	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
5	4	simprbi 498	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
6	5	adantr 481	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → Fun ◡𝐹)
7		df-f1 6497	. 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹))
8	3, 6, 7	sylanbrc 589	1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴–1-1→𝐶)

Syntax hints:   → wi 4   ∧ wa 396   ⊆ wss 3890  ^◡ccnv 5624  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 1802  ax-4 1816

This theorem depends on definitions:  df-bi 208  df-an 397  df-ss 3907  df-f 6496  df-f1 6497

This theorem is referenced by:  f1un  6794  f1sng  6817  f1prex  7235  domssr  8943  domssex2  9072  ssdomfi  9127  ssdomfi2  9128  marypha1lem  9343  marypha2  9349  isinffi  9914  fseqenlem1  9944  dfac12r  10067  ackbij2  10162  cff1  10178  fin23lem28  10260  fin23lem41  10272  pwfseqlem5  10584  hashf1lem1  14415  gsumzres  19882  gsumzcl2  19883  gsumzf1o  19885  gsumzaddlem  19894  gsumzmhm  19910  gsumzoppg  19917  lindfres  21805  islindf3  21808  dvne0f1  26004  oldfib  28394  istrkg2ld  28553  ausgrusgrb  29259  uspgrushgr  29271  usgruspgr  29274  uspgr1e  29338  sizusglecusglem1  29555  s1f1  33029  s2f1  33031  qqhre  34211  erdsze2lem1  35438  eldioph2lem2  43217  eldioph2  43218  fundcmpsurbijinjpreimafv  47889  fundcmpsurinjimaid  47893  stgrusgra  48457  usgrexmpl1lem  48519  usgrexmpl2lem  48524  gpgusgra  48555