Theorem f1ss 6777

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 6770	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
2		fss 6718	. . 3 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
3	1, 2	sylan 592	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
4		df-f1 6536	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
5	4	simprbi 503	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
6	5	adantr 486	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → Fun ◡𝐹)
7		df-f1 6536	. 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 3899  ^◡ccnv 5650  Fun wfun 6525  ⟶wf 6527  –1-1→wf1 6528

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 3916  df-f 6535  df-f1 6536

This theorem is used by:  f1un  6837  f1sng  6860  f1prex  7284  domssr  9010  domssex2  9140  ssdomfi  9195  ssdomfi2  9196  marypha1lem  9409  marypha2  9415  isinffi  10054  fseqenlem1  10084  dfac12r  10206  ackbij2  10301  cff1  10317  fin23lem28  10399  fin23lem41  10411  pwfseqlem5  10729  hashf1lem1  14580  s1f1  14736  gsumzres  20103  gsumzcl2  20104  gsumzf1o  20106  gsumzaddlem  20115  gsumzmhm  20131  gsumzoppg  20138  lindfres  22109  islindf3  22112  dvne0f1  26312  oldfib  28745  istrkg2ld  28904  ausgrusgrb  29728  uspgrushgr  29740  usgruspgr  29743  uspgr1e  29807  sizusglecusglem1  30024  s2f1  33492  qqhre  34634  erdsze2lem1  35937  eldioph2lem2  43725  eldioph2  43726  fundcmpsurbijinjpreimafv  48433  fundcmpsurinjimaid  48437  stgrusgra  49001  usgrexmpl1lem  49063  usgrexmpl2lem  49068  gpgusgra  49099