Theorem f1ss 6793

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3948  ^◡ccnv 5675  Fun wfun 6537  ⟶wf 6539  –1-1→wf1 6540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3955  df-ss 3965  df-f 6547  df-f1 6548

This theorem is referenced by:  f1un  6853  f1sng  6875  f1prex  7285  domssr  9001  domssex2  9143  ssdomfi  9205  ssdomfi2  9206  1sdomOLD  9255  marypha1lem  9434  marypha2  9440  isinffi  9993  fseqenlem1  10025  dfac12r  10147  ackbij2  10244  cff1  10259  fin23lem28  10341  fin23lem41  10353  pwfseqlem5  10664  hashf1lem1  14422  hashf1lem1OLD  14423  gsumzres  19825  gsumzcl2  19826  gsumzf1o  19828  gsumzaddlem  19837  gsumzmhm  19853  gsumzoppg  19860  lindfres  21688  islindf3  21691  dvne0f1  25865  istrkg2ld  28144  ausgrusgrb  28858  uspgrushgr  28868  usgruspgr  28871  uspgr1e  28934  sizusglecusglem1  29151  s1f1  32542  s2f1  32544  qqhre  33464  erdsze2lem1  34658  eldioph2lem2  41962  eldioph2  41963  fundcmpsurbijinjpreimafv  46534  fundcmpsurinjimaid  46538