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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3914  ^◡ccnv 5637  Fun wfun 6505  ⟶wf 6507  –1-1→wf1 6508

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3931  df-f 6515  df-f1 6516

This theorem is referenced by:  f1un  6820  f1sng  6842  f1prex  7259  domssr  8970  domssex2  9101  ssdomfi  9160  ssdomfi2  9161  1sdomOLD  9196  marypha1lem  9384  marypha2  9390  isinffi  9945  fseqenlem1  9977  dfac12r  10100  ackbij2  10195  cff1  10211  fin23lem28  10293  fin23lem41  10305  pwfseqlem5  10616  hashf1lem1  14420  gsumzres  19839  gsumzcl2  19840  gsumzf1o  19842  gsumzaddlem  19851  gsumzmhm  19867  gsumzoppg  19874  lindfres  21732  islindf3  21735  dvne0f1  25917  istrkg2ld  28387  ausgrusgrb  29092  uspgrushgr  29104  usgruspgr  29107  uspgr1e  29171  sizusglecusglem1  29389  s1f1  32864  s2f1  32866  qqhre  34010  erdsze2lem1  35190  eldioph2lem2  42749  eldioph2  42750  fundcmpsurbijinjpreimafv  47408  fundcmpsurinjimaid  47412  stgrusgra  47958  usgrexmpl1lem  48012  usgrexmpl2lem  48017  gpgusgra  48048