![]() |
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 6789 | . . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴) | |
2 | 1 | adantr 482 | . . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 ⊆ 𝐶) → 𝐹 Fn 𝐴) |
3 | simpr 486 | . . 3 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 ⊆ 𝐶) → ran 𝐹 ⊆ 𝐶) | |
4 | df-f 6548 | . . 3 ⊢ (𝐹:𝐴⟶𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶)) | |
5 | 2, 3, 4 | sylanbrc 584 | . 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶) |
6 | df-f1 6549 | . . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)) | |
7 | 6 | simprbi 498 | . . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹) |
8 | 7 | adantr 482 | . 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 ⊆ 𝐶) → Fun ◡𝐹) |
9 | df-f1 6549 | . 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹)) | |
10 | 5, 8, 9 | sylanbrc 584 | 1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 ⊆ 𝐶) → 𝐹:𝐴–1-1→𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ⊆ wss 3949 ◡ccnv 5676 ran crn 5678 Fun wfun 6538 Fn wfn 6539 ⟶wf 6540 –1-1→wf1 6541 |
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 398 df-f 6548 df-f1 6549 |
This theorem is referenced by: f1resf1 6797 domdifsn 9054 marypha1 9429 m2cpmf1 22245 ausgrusgri 28428 uspgrupgrushgr 28437 usgrumgruspgr 28440 usgruspgrb 28441 usgrres 28565 usgrres1 28572 lindflbs 32495 dimkerim 32712 cantnfub2 42072 |
Copyright terms: Public domain | W3C validator |