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

Syntax hints:   → wi 4   ∧ wa 396   ⊆ 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 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965  df-f 6547  df-f1 6548

This theorem is referenced by:  f1un  6853  f1sng  6875  f1prex  7284  domssr  8997  domssex2  9139  ssdomfi  9201  ssdomfi2  9202  1sdomOLD  9251  marypha1lem  9430  marypha2  9436  isinffi  9989  fseqenlem1  10021  dfac12r  10143  ackbij2  10240  cff1  10255  fin23lem28  10337  fin23lem41  10349  pwfseqlem5  10660  hashf1lem1  14417  hashf1lem1OLD  14418  gsumzres  19779  gsumzcl2  19780  gsumzf1o  19782  gsumzaddlem  19791  gsumzmhm  19807  gsumzoppg  19814  lindfres  21384  islindf3  21387  dvne0f1  25536  istrkg2ld  27749  ausgrusgrb  28463  uspgrushgr  28473  usgruspgr  28476  uspgr1e  28539  sizusglecusglem1  28756  s1f1  32147  s2f1  32149  qqhre  33069  erdsze2lem1  34263  eldioph2lem2  41587  eldioph2  41588  fundcmpsurbijinjpreimafv  46160  fundcmpsurinjimaid  46164