Theorem f1ss 6788

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 6781	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
2		fss 6729	. . 3 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
3	1, 2	sylan 592	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
4		df-f1 6548	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
5	4	simprbi 503	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
6	5	adantr 486	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → Fun ◡𝐹)
7		df-f1 6548	. 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 3908  ^◡ccnv 5665  Fun wfun 6537  ⟶wf 6539  –1-1→wf1 6540

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 3925  df-f 6547  df-f1 6548

This theorem is used by:  f1un  6848  f1sng  6871  f1prex  7293  domssr  9005  domssex2  9135  ssdomfi  9190  ssdomfi2  9191  marypha1lem  9403  marypha2  9409  isinffi  9997  fseqenlem1  10027  dfac12r  10149  ackbij2  10244  cff1  10260  fin23lem28  10342  fin23lem41  10354  pwfseqlem5  10666  hashf1lem1  14512  s1f1  14668  gsumzres  20010  gsumzcl2  20011  gsumzf1o  20013  gsumzaddlem  20022  gsumzmhm  20038  gsumzoppg  20045  lindfres  22010  islindf3  22013  dvne0f1  26208  oldfib  28607  istrkg2ld  28766  ausgrusgrb  29552  uspgrushgr  29564  usgruspgr  29567  uspgr1e  29631  sizusglecusglem1  29848  s2f1  33300  qqhre  34441  erdsze2lem1  35716  eldioph2lem2  43533  eldioph2  43534  fundcmpsurbijinjpreimafv  48197  fundcmpsurinjimaid  48201  stgrusgra  48765  usgrexmpl1lem  48827  usgrexmpl2lem  48832  gpgusgra  48863