Theorem f1ss 6782

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 6775	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
2		fss 6723	. . 3 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
3	1, 2	sylan 592	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
4		df-f1 6542	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
5	4	simprbi 503	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
6	5	adantr 486	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → Fun ◡𝐹)
7		df-f1 6542	. 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 3902  ^◡ccnv 5658  Fun wfun 6531  ⟶wf 6533  –1-1→wf1 6534

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 3919  df-f 6541  df-f1 6542

This theorem is used by:  f1un  6842  f1sng  6865  f1prex  7289  domssr  9009  domssex2  9139  ssdomfi  9194  ssdomfi2  9195  marypha1lem  9407  marypha2  9413  isinffi  10001  fseqenlem1  10031  dfac12r  10153  ackbij2  10248  cff1  10264  fin23lem28  10346  fin23lem41  10358  pwfseqlem5  10676  hashf1lem1  14524  s1f1  14680  gsumzres  20042  gsumzcl2  20043  gsumzf1o  20045  gsumzaddlem  20054  gsumzmhm  20070  gsumzoppg  20077  lindfres  22042  islindf3  22045  dvne0f1  26246  oldfib  28650  istrkg2ld  28809  ausgrusgrb  29633  uspgrushgr  29645  usgruspgr  29648  uspgr1e  29712  sizusglecusglem1  29929  s2f1  33397  qqhre  34538  erdsze2lem1  35790  eldioph2lem2  43614  eldioph2  43615  fundcmpsurbijinjpreimafv  48315  fundcmpsurinjimaid  48319  stgrusgra  48883  usgrexmpl1lem  48945  usgrexmpl2lem  48950  gpgusgra  48981