Theorem f1ss 6786

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 6779	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
2		fss 6727	. . 3 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
3	1, 2	sylan 592	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
4		df-f1 6544	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
5	4	simprbi 503	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
6	5	adantr 486	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → Fun ◡𝐹)
7		df-f1 6544	. 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 3895  ^◡ccnv 5649  Fun wfun 6533  ⟶wf 6535  –1-1→wf1 6536

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

This proof depends on definitions:  df-bi 210  df-an 402  df-ss 3896  df-f 6543  df-f1 6544

This theorem is used by:  f1un  6846  f1sng  6869  f1prex  7293  domssr  9030  domssex2  9160  ssdomfi  9215  ssdomfi2  9216  marypha1lem  9429  marypha2  9435  isinffi  10077  fseqenlem1  10107  dfac12r  10229  ackbij2  10324  cff1  10340  fin23lem28  10422  fin23lem41  10434  pwfseqlem5  10752  hashf1lem1  14604  s1f1  14761  gsumzres  20129  gsumzcl2  20130  gsumzf1o  20132  gsumzaddlem  20141  gsumzmhm  20157  gsumzoppg  20164  lindfres  22135  islindf3  22138  dvne0f1  26338  oldfib  28769  istrkg2ld  28928  ausgrusgrb  29752  uspgrushgr  29764  usgruspgr  29767  uspgr1e  29831  sizusglecusglem1  30048  s2f1  33557  qqhre  34699  dfac15  35810  erdsze2lem1  36055  eldioph2lem2  43866  eldioph2  43867  fundcmpsurbijinjpreimafv  48583  fundcmpsurinjimaid  48587  stgrusgra  49151  usgrexmpl1lem  49213  usgrexmpl2lem  49218  gpgusgra  49249