Theorem f1ss 6761

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 6754	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
2		fss 6702	. . 3 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
3	1, 2	sylan 589	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
4		df-f1 6520	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
5	4	simprbi 501	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
6	5	adantr 484	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → Fun ◡𝐹)
7		df-f1 6520	. 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹))
8	3, 6, 7	sylanbrc 592	1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴–1-1→𝐶)

Syntax hints:   → wi 4   ∧ wa 399   ⊆ wss 3902  ^◡ccnv 5642  Fun wfun 6509  ⟶wf 6511  –1-1→wf1 6512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828

This theorem depends on definitions:  df-bi 209  df-an 400  df-ss 3919  df-f 6519  df-f1 6520

This theorem is referenced by:  f1un  6821  f1sng  6844  f1prex  7262  domssr  8973  domssex2  9102  ssdomfi  9157  ssdomfi2  9158  marypha1lem  9372  marypha2  9378  isinffi  9943  fseqenlem1  9973  dfac12r  10096  ackbij2  10191  cff1  10208  fin23lem28  10290  fin23lem41  10302  pwfseqlem5  10614  hashf1lem1  14461  gsumzres  19939  gsumzcl2  19940  gsumzf1o  19942  gsumzaddlem  19951  gsumzmhm  19967  gsumzoppg  19974  lindfres  21862  islindf3  21865  dvne0f1  26061  oldfib  28457  istrkg2ld  28616  ausgrusgrb  29322  uspgrushgr  29334  usgruspgr  29337  uspgr1e  29401  sizusglecusglem1  29618  s1f1  33081  s2f1  33083  qqhre  34277  erdsze2lem1  35513  eldioph2lem2  43302  eldioph2  43303  fundcmpsurbijinjpreimafv  47973  fundcmpsurinjimaid  47977  stgrusgra  48541  usgrexmpl1lem  48603  usgrexmpl2lem  48608  gpgusgra  48639