Theorem f1ssr 6661

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 6655	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2	1	adantr 480	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 ⊆ 𝐶) → 𝐹 Fn 𝐴)
3		simpr 484	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 ⊆ 𝐶) → ran 𝐹 ⊆ 𝐶)
4		df-f 6422	. . 3 ⊢ (𝐹:𝐴⟶𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶))
5	2, 3, 4	sylanbrc 582	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
6		df-f1 6423	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
7	6	simprbi 496	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
8	7	adantr 480	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 ⊆ 𝐶) → Fun ◡𝐹)
9		df-f1 6423	. 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹))
10	5, 8, 9	sylanbrc 582	1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 ⊆ 𝐶) → 𝐹:𝐴–1-1→𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3883  ^◡ccnv 5579  ran crn 5581  Fun wfun 6412   Fn wfn 6413  ⟶wf 6414  –1-1→wf1 6415

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 206  df-an 396  df-f 6422  df-f1 6423

This theorem is referenced by:  f1resf1  6663  domdifsn  8795  marypha1  9123  m2cpmf1  21800  ausgrusgri  27441  uspgrupgrushgr  27450  usgrumgruspgr  27453  usgruspgrb  27454  usgrres  27578  usgrres1  27585  lindflbs  31476  dimkerim  31610