Theorem f1ss 6764

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3917  ^◡ccnv 5640  Fun wfun 6508  ⟶wf 6510  –1-1→wf1 6511

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 3934  df-f 6518  df-f1 6519

This theorem is referenced by:  f1un  6823  f1sng  6845  f1prex  7262  domssr  8973  domssex2  9107  ssdomfi  9166  ssdomfi2  9167  1sdomOLD  9203  marypha1lem  9391  marypha2  9397  isinffi  9952  fseqenlem1  9984  dfac12r  10107  ackbij2  10202  cff1  10218  fin23lem28  10300  fin23lem41  10312  pwfseqlem5  10623  hashf1lem1  14427  gsumzres  19846  gsumzcl2  19847  gsumzf1o  19849  gsumzaddlem  19858  gsumzmhm  19874  gsumzoppg  19881  lindfres  21739  islindf3  21742  dvne0f1  25924  istrkg2ld  28394  ausgrusgrb  29099  uspgrushgr  29111  usgruspgr  29114  uspgr1e  29178  sizusglecusglem1  29396  s1f1  32871  s2f1  32873  qqhre  34017  erdsze2lem1  35197  eldioph2lem2  42756  eldioph2  42757  fundcmpsurbijinjpreimafv  47412  fundcmpsurinjimaid  47416  stgrusgra  47962  usgrexmpl1lem  48016  usgrexmpl2lem  48021  gpgusgra  48052