Theorem f1ssr 6772

Description: A function that is one-to-one is also one-to-one on some superset of its range. (Contributed by Stefan O'Rear, 20-Feb-2015.)

Assertion

Ref	Expression
f1ssr	⊢ ((𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 ⊆ 𝐶) → 𝐹:𝐴–1-1→𝐶)

Proof of Theorem f1ssr

Step	Hyp	Ref	Expression
1		f1fn 6765	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2	1	adantr 485	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 ⊆ 𝐶) → 𝐹 Fn 𝐴)
3		simpr 489	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 ⊆ 𝐶) → ran 𝐹 ⊆ 𝐶)
4		df-f 6529	. . 3 ⊢ (𝐹:𝐴⟶𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶))
5	2, 3, 4	sylanbrc 594	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
6		df-f1 6530	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
7	6	simprbi 502	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
8	7	adantr 485	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 ⊆ 𝐶) → Fun ◡𝐹)
9		df-f1 6530	. 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹))
10	5, 8, 9	sylanbrc 594	1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 ⊆ 𝐶) → 𝐹:𝐴–1-1→𝐶)

Syntax hints:   → wi 4   ∧ wa 400   ⊆ wss 3907  ^◡ccnv 5651  ran crn 5653  Fun wfun 6519   Fn wfn 6520  ⟶wf 6521  –1-1→wf1 6522

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-f 6529  df-f1 6530

This theorem is referenced by:  f1resf1  6774  domdifsn  9036  marypha1  9382  m2cpmf1  22861  ausgrusgri  29427  uspgrupgrushgr  29438  usgrumgruspgr  29441  usgruspgrb  29442  usgrres  29567  usgrres1  29574  lindflbs  33608  dimkerim  33934  fineqvinfep  35433  cantnfub2  43911