Theorem f1ss 6729

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3905  ^◡ccnv 5622  Fun wfun 6480  ⟶wf 6482  –1-1→wf1 6483

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 3922  df-f 6490  df-f1 6491

This theorem is referenced by:  f1un  6788  f1sng  6810  f1prex  7225  domssr  8931  domssex2  9061  ssdomfi  9120  ssdomfi2  9121  marypha1lem  9342  marypha2  9348  isinffi  9907  fseqenlem1  9937  dfac12r  10060  ackbij2  10155  cff1  10171  fin23lem28  10253  fin23lem41  10265  pwfseqlem5  10576  hashf1lem1  14380  gsumzres  19806  gsumzcl2  19807  gsumzf1o  19809  gsumzaddlem  19818  gsumzmhm  19834  gsumzoppg  19841  lindfres  21748  islindf3  21751  dvne0f1  25933  istrkg2ld  28423  ausgrusgrb  29128  uspgrushgr  29140  usgruspgr  29143  uspgr1e  29207  sizusglecusglem1  29425  s1f1  32897  s2f1  32899  qqhre  33989  erdsze2lem1  35178  eldioph2lem2  42737  eldioph2  42738  fundcmpsurbijinjpreimafv  47395  fundcmpsurinjimaid  47399  stgrusgra  47947  usgrexmpl1lem  48009  usgrexmpl2lem  48014  gpgusgra  48045