Theorem f1ss 6247

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 6242	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
2		fss 6197	. . 3 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
3	1, 2	sylan 563	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
4		df-f1 6037	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
5	4	simprbi 480	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
6	5	adantr 466	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → Fun ◡𝐹)
7		df-f1 6037	. 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹))
8	3, 6, 7	sylanbrc 566	1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴–1-1→𝐶)

Syntax hints:   → wi 4   ∧ wa 382   ⊆ wss 3724  ^◡ccnv 5249  Fun wfun 6026  ⟶wf 6028  –1-1→wf1 6029

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-in 3731  df-ss 3738  df-f 6036  df-f1 6037

This theorem is referenced by:  f1sng  6320  f1prex  6683  domssex2  8277  1sdom  8320  marypha1lem  8496  marypha2  8502  isinffi  9019  fseqenlem1  9048  dfac12r  9171  ackbij2  9268  cff1  9283  fin23lem28  9365  fin23lem41  9377  pwfseqlem5  9688  hashf1lem1  13442  gsumzres  18518  gsumzcl2  18519  gsumzf1o  18521  gsumzaddlem  18529  gsumzmhm  18545  gsumzoppg  18552  lindfres  20380  islindf3  20383  dvne0f1  23996  istrkg2ld  25581  ausgrusgrb  26283  uspgrushgr  26293  usgruspgr  26296  uspgr1e  26360  sizusglecusglem1  26593  qqhre  30405  erdsze2lem1  31524  eldioph2lem2  37851  eldioph2  37852