Theorem f1ss 6790

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

Syntax hints:   → wi 4   ∧ wa 396   ⊆ wss 3947  ^◡ccnv 5674  Fun wfun 6534  ⟶wf 6536  –1-1→wf1 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954  df-ss 3964  df-f 6544  df-f1 6545

This theorem is referenced by:  f1un  6850  f1sng  6872  f1prex  7278  domssr  8991  domssex2  9133  ssdomfi  9195  ssdomfi2  9196  1sdomOLD  9245  marypha1lem  9424  marypha2  9430  isinffi  9983  fseqenlem1  10015  dfac12r  10137  ackbij2  10234  cff1  10249  fin23lem28  10331  fin23lem41  10343  pwfseqlem5  10654  hashf1lem1  14411  hashf1lem1OLD  14412  gsumzres  19771  gsumzcl2  19772  gsumzf1o  19774  gsumzaddlem  19783  gsumzmhm  19799  gsumzoppg  19806  lindfres  21369  islindf3  21372  dvne0f1  25520  istrkg2ld  27700  ausgrusgrb  28414  uspgrushgr  28424  usgruspgr  28427  uspgr1e  28490  sizusglecusglem1  28707  s1f1  32096  s2f1  32098  qqhre  32988  erdsze2lem1  34182  eldioph2lem2  41484  eldioph2  41485  fundcmpsurbijinjpreimafv  46061  fundcmpsurinjimaid  46065