Theorem f1ss 6810

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 6803	. . 3 ⊢ (𝐹:𝐴⟶1-1𝐵 → 𝐹:𝐴⟶𝐵)
2		fss 6751	. . 3 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
3	1, 2	sylan 592	. 2 ⊢ ((𝐹:𝐴⟶1-1𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
4		df-f1 6566	. . . 4 ⊢ (𝐹:𝐴⟶1-1𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
5	4	simprbi 503	. . 3 ⊢ (𝐹:𝐴⟶1-1𝐵 → Fun ◡𝐹)
6	5	adantr 486	. 2 ⊢ ((𝐹:𝐴⟶1-1𝐵 ∧ 𝐵 ⊆ 𝐶) → Fun ◡𝐹)
7		df-f1 6566	. 2 ⊢ (𝐹:𝐴⟶1-1𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹))
8	3, 6, 7	sylanbrc 595	1 ⊢ ((𝐹:𝐴⟶1-1𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶1-1𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ⊆ wss 3900  ^◡ccnv 5655  Fun wfun 6555  ⟶wf 6557  ⟶1-1wf1 6558

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ss 3901  df-f 6565  df-f1 6566

This theorem is used by:  f1un  6870  f1sng  6894  f1prex  7318  domssr  9057  domssex2  9187  ssdomfi  9242  ssdomfi2  9243  marypha1lem  9455  marypha2  9461  isinffi  10103  fseqenlem1  10133  dfac12r  10255  ackbij2  10350  cff1  10366  fin23lem28  10448  fin23lem41  10460  pwfseqlem5  10778  hashf1lem1  14630  s1f1  14787  gsumzres  20156  gsumzcl2  20157  gsumzf1o  20159  gsumzaddlem  20168  gsumzmhm  20184  gsumzoppg  20191  lindfres  22162  islindf3  22165  dvne0f1  26365  oldfib  28796  istrkg2ld  28955  ausgrusgrb  29779  uspgrushgr  29791  usgruspgr  29794  uspgr1e  29858  sizusglecusglem1  30075  s2f1  33583  qqhre  34735  dfac15  35858  erdsze2lem1  36148  eldioph2lem2  43976  eldioph2  43977  fundcmpsurbijinjpreimafv  48704  fundcmpsurinjimaid  48708  stgrusgra  49272  usgrexmpl1lem  49334  usgrexmpl2lem  49339  gpgusgra  49370