Theorem f1ss 6019

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 6014	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
2		fss 5969	. . 3 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
3	1, 2	sylan 487	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
4		df-f1 5809	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
5	4	simprbi 479	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
6	5	adantr 480	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → Fun ◡𝐹)
7		df-f1 5809	. 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹))
8	3, 6, 7	sylanbrc 695	1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴–1-1→𝐶)

Syntax hints:   → wi 4   ∧ wa 383   ⊆ wss 3540  ^◡ccnv 5037  Fun wfun 5798  ⟶wf 5800  –1-1→wf1 5801

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554  df-f 5808  df-f1 5809

This theorem is referenced by:  f1sng  6090  f1prex  6439  domssex2  8005  1sdom  8048  marypha1lem  8222  marypha2  8228  isinffi  8701  fseqenlem1  8730  dfac12r  8851  ackbij2  8948  cff1  8963  fin23lem28  9045  fin23lem41  9057  pwfseqlem5  9364  hashf1lem1  13096  gsumzres  18133  gsumzcl2  18134  gsumzf1o  18136  gsumzaddlem  18144  gsumzmhm  18160  gsumzoppg  18167  lindfres  19981  islindf3  19984  dvne0f1  23579  istrkg2ld  25159  ausisusgra  25884  uslisushgra  25892  usisuslgra  25894  uslgra1  25901  usgra1  25902  sizeusglecusglem1  26012  2trllemE  26083  constr1trl  26118  frgrancvvdeqlem8  26567  qqhre  29392  erdsze2lem1  30439  eldioph2lem2  36342  eldioph2  36343  ausgrusgrb  40395  uspgrushgr  40405  usgruspgr  40408  uspgr1e  40470  sizusglecusglem1  40677  frgrncvvdeqlem8  41479