Theorem f1ss 6809

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3962  ^◡ccnv 5687  Fun wfun 6556  ⟶wf 6558  –1-1→wf1 6559

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3979  df-f 6566  df-f1 6567

This theorem is referenced by:  f1un  6868  f1sng  6890  f1prex  7303  domssr  9037  domssex2  9175  ssdomfi  9233  ssdomfi2  9234  1sdomOLD  9282  marypha1lem  9470  marypha2  9476  isinffi  10029  fseqenlem1  10061  dfac12r  10184  ackbij2  10279  cff1  10295  fin23lem28  10377  fin23lem41  10389  pwfseqlem5  10700  hashf1lem1  14490  gsumzres  19941  gsumzcl2  19942  gsumzf1o  19944  gsumzaddlem  19953  gsumzmhm  19969  gsumzoppg  19976  lindfres  21860  islindf3  21863  dvne0f1  26065  istrkg2ld  28482  ausgrusgrb  29196  uspgrushgr  29208  usgruspgr  29211  uspgr1e  29275  sizusglecusglem1  29493  s1f1  32911  s2f1  32913  qqhre  33982  erdsze2lem1  35187  eldioph2lem2  42748  eldioph2  42749  fundcmpsurbijinjpreimafv  47331  fundcmpsurinjimaid  47335  stgrusgra  47861  usgrexmpl1lem  47915  usgrexmpl2lem  47920  gpgusgra  47946