Theorem f1ss 6731

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3898  ^◡ccnv 5620  Fun wfun 6482  ⟶wf 6484  –1-1→wf1 6485

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 3915  df-f 6492  df-f1 6493

This theorem is referenced by:  f1un  6790  f1sng  6813  f1prex  7226  domssr  8930  domssex2  9059  ssdomfi  9114  ssdomfi2  9115  marypha1lem  9326  marypha2  9332  isinffi  9894  fseqenlem1  9924  dfac12r  10047  ackbij2  10142  cff1  10158  fin23lem28  10240  fin23lem41  10252  pwfseqlem5  10563  hashf1lem1  14366  gsumzres  19825  gsumzcl2  19826  gsumzf1o  19828  gsumzaddlem  19837  gsumzmhm  19853  gsumzoppg  19860  lindfres  21764  islindf3  21767  dvne0f1  25947  istrkg2ld  28441  ausgrusgrb  29147  uspgrushgr  29159  usgruspgr  29162  uspgr1e  29226  sizusglecusglem1  29444  s1f1  32933  s2f1  32935  qqhre  34056  erdsze2lem1  35270  eldioph2lem2  42881  eldioph2  42882  fundcmpsurbijinjpreimafv  47534  fundcmpsurinjimaid  47538  stgrusgra  48086  usgrexmpl1lem  48148  usgrexmpl2lem  48153  gpgusgra  48184