Theorem f1ss 6743

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 6738	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
2		fss 6686	. . 3 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
3	1, 2	sylan 581	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
4		df-f1 6505	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
5	4	simprbi 497	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
6	5	adantr 480	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → Fun ◡𝐹)
7		df-f1 6505	. 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹))
8	3, 6, 7	sylanbrc 584	1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴–1-1→𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3903  ^◡ccnv 5631  Fun wfun 6494  ⟶wf 6496  –1-1→wf1 6497

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3920  df-f 6504  df-f1 6505

This theorem is referenced by:  f1un  6802  f1sng  6825  f1prex  7240  domssr  8948  domssex2  9077  ssdomfi  9132  ssdomfi2  9133  marypha1lem  9348  marypha2  9354  isinffi  9916  fseqenlem1  9946  dfac12r  10069  ackbij2  10164  cff1  10180  fin23lem28  10262  fin23lem41  10274  pwfseqlem5  10586  hashf1lem1  14390  gsumzres  19850  gsumzcl2  19851  gsumzf1o  19853  gsumzaddlem  19862  gsumzmhm  19878  gsumzoppg  19885  lindfres  21790  islindf3  21793  dvne0f1  25985  oldfib  28385  istrkg2ld  28544  ausgrusgrb  29250  uspgrushgr  29262  usgruspgr  29265  uspgr1e  29329  sizusglecusglem1  29547  s1f1  33035  s2f1  33037  qqhre  34197  erdsze2lem1  35416  eldioph2lem2  43115  eldioph2  43116  fundcmpsurbijinjpreimafv  47764  fundcmpsurinjimaid  47768  stgrusgra  48316  usgrexmpl1lem  48378  usgrexmpl2lem  48383  gpgusgra  48414