|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > f1ssr | Structured version Visualization version GIF version | ||
| 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.) | 
| Ref | Expression | 
|---|---|
| f1ssr | ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 ⊆ 𝐶) → 𝐹:𝐴–1-1→𝐶) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | f1fn 6804 | . . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴) | |
| 2 | 1 | adantr 480 | . . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 ⊆ 𝐶) → 𝐹 Fn 𝐴) | 
| 3 | simpr 484 | . . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 ⊆ 𝐶) → ran 𝐹 ⊆ 𝐶) | |
| 4 | df-f 6564 | . . 3 ⊢ (𝐹:𝐴⟶𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶)) | |
| 5 | 2, 3, 4 | sylanbrc 583 | . 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶) | 
| 6 | df-f1 6565 | . . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)) | |
| 7 | 6 | simprbi 496 | . . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹) | 
| 8 | 7 | adantr 480 | . 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 ⊆ 𝐶) → Fun ◡𝐹) | 
| 9 | df-f1 6565 | . 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹)) | |
| 10 | 5, 8, 9 | sylanbrc 583 | 1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 ⊆ 𝐶) → 𝐹:𝐴–1-1→𝐶) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 ⊆ wss 3950 ◡ccnv 5683 ran crn 5685 Fun wfun 6554 Fn wfn 6555 ⟶wf 6556 –1-1→wf1 6557 | 
| 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 207 df-an 396 df-f 6564 df-f1 6565 | 
| This theorem is referenced by: f1resf1 6811 domdifsn 9095 marypha1 9475 m2cpmf1 22750 ausgrusgri 29186 uspgrupgrushgr 29197 usgrumgruspgr 29200 usgruspgrb 29201 usgrres 29326 usgrres1 29333 lindflbs 33408 dimkerim 33679 cantnfub2 43340 | 
| Copyright terms: Public domain | W3C validator |