Theorem f1ss 6794

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 6788	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
2		fss 6735	. . 3 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
3	1, 2	sylan 581	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
4		df-f1 6549	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
5	4	simprbi 498	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
6	5	adantr 482	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → Fun ◡𝐹)
7		df-f1 6549	. 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹))
8	3, 6, 7	sylanbrc 584	1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴–1-1→𝐶)

Syntax hints:   → wi 4   ∧ wa 397   ⊆ wss 3949  ^◡ccnv 5676  Fun wfun 6538  ⟶wf 6540  –1-1→wf1 6541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-f 6548  df-f1 6549

This theorem is referenced by:  f1un  6854  f1sng  6876  f1prex  7282  domssr  8995  domssex2  9137  ssdomfi  9199  ssdomfi2  9200  1sdomOLD  9249  marypha1lem  9428  marypha2  9434  isinffi  9987  fseqenlem1  10019  dfac12r  10141  ackbij2  10238  cff1  10253  fin23lem28  10335  fin23lem41  10347  pwfseqlem5  10658  hashf1lem1  14415  hashf1lem1OLD  14416  gsumzres  19777  gsumzcl2  19778  gsumzf1o  19780  gsumzaddlem  19789  gsumzmhm  19805  gsumzoppg  19812  lindfres  21378  islindf3  21381  dvne0f1  25529  istrkg2ld  27711  ausgrusgrb  28425  uspgrushgr  28435  usgruspgr  28438  uspgr1e  28501  sizusglecusglem1  28718  s1f1  32109  s2f1  32111  qqhre  33000  erdsze2lem1  34194  eldioph2lem2  41499  eldioph2  41500  fundcmpsurbijinjpreimafv  46075  fundcmpsurinjimaid  46079