Theorem f1ss 6566

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 6560	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
2		fss 6512	. . 3 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
3	1, 2	sylan 583	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
4		df-f1 6340	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
5	4	simprbi 500	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
6	5	adantr 484	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → Fun ◡𝐹)
7		df-f1 6340	. 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹))
8	3, 6, 7	sylanbrc 586	1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴–1-1→𝐶)

Syntax hints:   → wi 4   ∧ wa 399   ⊆ wss 3858  ^◡ccnv 5523  Fun wfun 6329  ⟶wf 6331  –1-1→wf1 6332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3865  df-ss 3875  df-f 6339  df-f1 6340

This theorem is referenced by:  f1sng  6643  f1prex  7032  domssex2  8699  1sdom  8759  marypha1lem  8930  marypha2  8936  isinffi  9454  fseqenlem1  9484  dfac12r  9606  ackbij2  9703  cff1  9718  fin23lem28  9800  fin23lem41  9812  pwfseqlem5  10123  hashf1lem1  13864  hashf1lem1OLD  13865  gsumzres  19097  gsumzcl2  19098  gsumzf1o  19100  gsumzaddlem  19109  gsumzmhm  19125  gsumzoppg  19132  lindfres  20588  islindf3  20591  dvne0f1  24711  istrkg2ld  26353  ausgrusgrb  27057  uspgrushgr  27067  usgruspgr  27070  uspgr1e  27133  sizusglecusglem1  27350  s1f1  30741  s2f1  30743  qqhre  31489  erdsze2lem1  32681  eldioph2lem2  40097  eldioph2  40098  fundcmpsurbijinjpreimafv  44314  fundcmpsurinjimaid  44318