Theorem f1ss 6779

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3926  ^◡ccnv 5653  Fun wfun 6525  ⟶wf 6527  –1-1→wf1 6528

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3943  df-f 6535  df-f1 6536

This theorem is referenced by:  f1un  6838  f1sng  6860  f1prex  7277  domssr  9013  domssex2  9151  ssdomfi  9210  ssdomfi2  9211  1sdomOLD  9257  marypha1lem  9445  marypha2  9451  isinffi  10006  fseqenlem1  10038  dfac12r  10161  ackbij2  10256  cff1  10272  fin23lem28  10354  fin23lem41  10366  pwfseqlem5  10677  hashf1lem1  14473  gsumzres  19890  gsumzcl2  19891  gsumzf1o  19893  gsumzaddlem  19902  gsumzmhm  19918  gsumzoppg  19925  lindfres  21783  islindf3  21786  dvne0f1  25969  istrkg2ld  28439  ausgrusgrb  29144  uspgrushgr  29156  usgruspgr  29159  uspgr1e  29223  sizusglecusglem1  29441  s1f1  32918  s2f1  32920  qqhre  34051  erdsze2lem1  35225  eldioph2lem2  42784  eldioph2  42785  fundcmpsurbijinjpreimafv  47421  fundcmpsurinjimaid  47425  stgrusgra  47971  usgrexmpl1lem  48025  usgrexmpl2lem  48030  gpgusgra  48061