Theorem f1ss 6822

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 6817	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
2		fss 6763	. . 3 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
3	1, 2	sylan 579	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
4		df-f1 6578	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
5	4	simprbi 496	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
6	5	adantr 480	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → Fun ◡𝐹)
7		df-f1 6578	. 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹))
8	3, 6, 7	sylanbrc 582	1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴–1-1→𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3976  ^◡ccnv 5699  Fun wfun 6567  ⟶wf 6569  –1-1→wf1 6570

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3993  df-f 6577  df-f1 6578

This theorem is referenced by:  f1un  6882  f1sng  6904  f1prex  7320  domssr  9059  domssex2  9203  ssdomfi  9262  ssdomfi2  9263  1sdomOLD  9312  marypha1lem  9502  marypha2  9508  isinffi  10061  fseqenlem1  10093  dfac12r  10216  ackbij2  10311  cff1  10327  fin23lem28  10409  fin23lem41  10421  pwfseqlem5  10732  hashf1lem1  14504  gsumzres  19951  gsumzcl2  19952  gsumzf1o  19954  gsumzaddlem  19963  gsumzmhm  19979  gsumzoppg  19986  lindfres  21866  islindf3  21869  dvne0f1  26071  istrkg2ld  28486  ausgrusgrb  29200  uspgrushgr  29212  usgruspgr  29215  uspgr1e  29279  sizusglecusglem1  29497  s1f1  32909  s2f1  32911  qqhre  33966  erdsze2lem1  35171  eldioph2lem2  42717  eldioph2  42718  fundcmpsurbijinjpreimafv  47281  fundcmpsurinjimaid  47285  usgrexmpl1lem  47836  usgrexmpl2lem  47841