Theorem f1ssr 6811

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 6804	. . . 4 ⊢ (𝐹:𝐴⟶1-1𝐵 → 𝐹 Fn 𝐴)
2	1	adantr 486	. . 3 ⊢ ((𝐹:𝐴⟶1-1𝐵 ∧ ran 𝐹 ⊆ 𝐶) → 𝐹 Fn 𝐴)
3		simpr 490	. . 3 ⊢ ((𝐹:𝐴⟶1-1𝐵 ∧ ran 𝐹 ⊆ 𝐶) → ran 𝐹 ⊆ 𝐶)
4		df-f 6565	. . 3 ⊢ (𝐹:𝐴⟶𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶))
5	2, 3, 4	sylanbrc 595	. 2 ⊢ ((𝐹:𝐴⟶1-1𝐵 ∧ ran 𝐹 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
6		df-f1 6566	. . . 4 ⊢ (𝐹:𝐴⟶1-1𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
7	6	simprbi 503	. . 3 ⊢ (𝐹:𝐴⟶1-1𝐵 → Fun ◡𝐹)
8	7	adantr 486	. 2 ⊢ ((𝐹:𝐴⟶1-1𝐵 ∧ ran 𝐹 ⊆ 𝐶) → Fun ◡𝐹)
9		df-f1 6566	. 2 ⊢ (𝐹:𝐴⟶1-1𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹))
10	5, 8, 9	sylanbrc 595	1 ⊢ ((𝐹:𝐴⟶1-1𝐵 ∧ ran 𝐹 ⊆ 𝐶) → 𝐹:𝐴⟶1-1𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ⊆ wss 3900  ^◡ccnv 5655  ran crn 5657  Fun wfun 6555   Fn wfn 6556  ⟶wf 6557  ⟶1-1wf1 6558

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-f 6565  df-f1 6566

This theorem is used by:  f1resf1  6813  domdifsn  9110  marypha1  9456  m2cpmf1  23094  ausgrusgri  29782  uspgrupgrushgr  29793  usgrumgruspgr  29796  usgruspgrb  29797  usgrres  29922  usgrres1  29929  lindflbs  34018  dimkerim  34342  fineqvinfep  35906  cantnfub2  44527