Theorem f1ss 6580

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 6575	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
2		fss 6527	. . 3 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
3	1, 2	sylan 582	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
4		df-f1 6360	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
5	4	simprbi 499	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
6	5	adantr 483	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → Fun ◡𝐹)
7		df-f1 6360	. 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹))
8	3, 6, 7	sylanbrc 585	1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴–1-1→𝐶)

Syntax hints:   → wi 4   ∧ wa 398   ⊆ wss 3936  ^◡ccnv 5554  Fun wfun 6349  ⟶wf 6351  –1-1→wf1 6352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952  df-f 6359  df-f1 6360

This theorem is referenced by:  f1sng  6656  f1prex  7040  domssex2  8677  1sdom  8721  marypha1lem  8897  marypha2  8903  isinffi  9421  fseqenlem1  9450  dfac12r  9572  ackbij2  9665  cff1  9680  fin23lem28  9762  fin23lem41  9774  pwfseqlem5  10085  hashf1lem1  13814  gsumzres  19029  gsumzcl2  19030  gsumzf1o  19032  gsumzaddlem  19041  gsumzmhm  19057  gsumzoppg  19064  lindfres  20967  islindf3  20970  dvne0f1  24609  istrkg2ld  26246  ausgrusgrb  26950  uspgrushgr  26960  usgruspgr  26963  uspgr1e  27026  sizusglecusglem1  27243  s1f1  30619  s2f1  30621  qqhre  31261  erdsze2lem1  32450  eldioph2lem2  39378  eldioph2  39379  fundcmpsurbijinjpreimafv  43587  fundcmpsurinjimaid  43591