Theorem f1ss 6735

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3890  ^◡ccnv 5623  Fun wfun 6486  ⟶wf 6488  –1-1→wf1 6489

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 3907  df-f 6496  df-f1 6497

This theorem is referenced by:  f1un  6794  f1sng  6817  f1prex  7232  domssr  8939  domssex2  9068  ssdomfi  9123  ssdomfi2  9124  marypha1lem  9339  marypha2  9345  isinffi  9907  fseqenlem1  9937  dfac12r  10060  ackbij2  10155  cff1  10171  fin23lem28  10253  fin23lem41  10265  pwfseqlem5  10577  hashf1lem1  14408  gsumzres  19875  gsumzcl2  19876  gsumzf1o  19878  gsumzaddlem  19887  gsumzmhm  19903  gsumzoppg  19910  lindfres  21813  islindf3  21816  dvne0f1  25989  oldfib  28383  istrkg2ld  28542  ausgrusgrb  29248  uspgrushgr  29260  usgruspgr  29263  uspgr1e  29327  sizusglecusglem1  29545  s1f1  33018  s2f1  33020  qqhre  34180  erdsze2lem1  35401  eldioph2lem2  43207  eldioph2  43208  fundcmpsurbijinjpreimafv  47879  fundcmpsurinjimaid  47883  stgrusgra  48447  usgrexmpl1lem  48509  usgrexmpl2lem  48514  gpgusgra  48545