Theorem f1ssr 6764

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 6757	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2	1	adantr 484	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 ⊆ 𝐶) → 𝐹 Fn 𝐴)
3		simpr 488	. . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 ⊆ 𝐶) → ran 𝐹 ⊆ 𝐶)
4		df-f 6521	. . 3 ⊢ (𝐹:𝐴⟶𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶))
5	2, 3, 4	sylanbrc 592	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
6		df-f1 6522	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
7	6	simprbi 501	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
8	7	adantr 484	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 ⊆ 𝐶) → Fun ◡𝐹)
9		df-f1 6522	. 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹))
10	5, 8, 9	sylanbrc 592	1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 ⊆ 𝐶) → 𝐹:𝐴–1-1→𝐶)

Syntax hints:   → wi 4   ∧ wa 399   ⊆ wss 3904  ^◡ccnv 5644  ran crn 5646  Fun wfun 6511   Fn wfn 6512  ⟶wf 6513  –1-1→wf1 6514

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 209  df-an 400  df-f 6521  df-f1 6522

This theorem is referenced by:  f1resf1  6766  domdifsn  9028  marypha1  9377  m2cpmf1  22783  ausgrusgri  29315  uspgrupgrushgr  29326  usgrumgruspgr  29329  usgruspgrb  29330  usgrres  29455  usgrres1  29462  lindflbs  33526  dimkerim  33885  fineqvinfep  35385  cantnfub2  43863