Theorem f1ss 6741

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3889  ^◡ccnv 5630  Fun wfun 6492  ⟶wf 6494  –1-1→wf1 6495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3906  df-f 6502  df-f1 6503

This theorem is referenced by:  f1un  6800  f1sng  6823  f1prex  7239  domssr  8946  domssex2  9075  ssdomfi  9130  ssdomfi2  9131  marypha1lem  9346  marypha2  9352  isinffi  9916  fseqenlem1  9946  dfac12r  10069  ackbij2  10164  cff1  10180  fin23lem28  10262  fin23lem41  10274  pwfseqlem5  10586  hashf1lem1  14417  gsumzres  19884  gsumzcl2  19885  gsumzf1o  19887  gsumzaddlem  19896  gsumzmhm  19912  gsumzoppg  19919  lindfres  21803  islindf3  21806  dvne0f1  25979  oldfib  28369  istrkg2ld  28528  ausgrusgrb  29234  uspgrushgr  29246  usgruspgr  29249  uspgr1e  29313  sizusglecusglem1  29530  s1f1  33003  s2f1  33005  qqhre  34164  erdsze2lem1  35385  eldioph2lem2  43193  eldioph2  43194  fundcmpsurbijinjpreimafv  47867  fundcmpsurinjimaid  47871  stgrusgra  48435  usgrexmpl1lem  48497  usgrexmpl2lem  48502  gpgusgra  48533