Theorem f1ss 6809

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3951  ^◡ccnv 5684  Fun wfun 6555  ⟶wf 6557  –1-1→wf1 6558

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 3968  df-f 6565  df-f1 6566

This theorem is referenced by:  f1un  6868  f1sng  6890  f1prex  7304  domssr  9039  domssex2  9177  ssdomfi  9236  ssdomfi2  9237  1sdomOLD  9285  marypha1lem  9473  marypha2  9479  isinffi  10032  fseqenlem1  10064  dfac12r  10187  ackbij2  10282  cff1  10298  fin23lem28  10380  fin23lem41  10392  pwfseqlem5  10703  hashf1lem1  14494  gsumzres  19927  gsumzcl2  19928  gsumzf1o  19930  gsumzaddlem  19939  gsumzmhm  19955  gsumzoppg  19962  lindfres  21843  islindf3  21846  dvne0f1  26051  istrkg2ld  28468  ausgrusgrb  29182  uspgrushgr  29194  usgruspgr  29197  uspgr1e  29261  sizusglecusglem1  29479  s1f1  32927  s2f1  32929  qqhre  34021  erdsze2lem1  35208  eldioph2lem2  42772  eldioph2  42773  fundcmpsurbijinjpreimafv  47394  fundcmpsurinjimaid  47398  stgrusgra  47926  usgrexmpl1lem  47980  usgrexmpl2lem  47985  gpgusgra  48012