| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > f1ss | Structured version Visualization version GIF version | ||
| Description: A function that is one-to-one is also one-to-one on some superset of its codomain. (Contributed by Mario Carneiro, 12-Jan-2013.) |
| Ref | Expression |
|---|---|
| f1ss | ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴–1-1→𝐶) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | f1f 6804 | . . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵) | |
| 2 | fss 6752 | . . 3 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶) | |
| 3 | 1, 2 | sylan 580 | . 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶) |
| 4 | df-f1 6566 | . . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)) | |
| 5 | 4 | simprbi 496 | . . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹) |
| 6 | 5 | adantr 480 | . 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → Fun ◡𝐹) |
| 7 | df-f1 6566 | . 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹)) | |
| 8 | 3, 6, 7 | sylanbrc 583 | 1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴–1-1→𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ⊆ wss 3951 ◡ccnv 5684 Fun wfun 6555 ⟶wf 6557 –1-1→wf1 6558 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ss 3968 df-f 6565 df-f1 6566 |
| This theorem is referenced by: f1un 6868 f1sng 6890 f1prex 7304 domssr 9039 domssex2 9177 ssdomfi 9236 ssdomfi2 9237 1sdomOLD 9285 marypha1lem 9473 marypha2 9479 isinffi 10032 fseqenlem1 10064 dfac12r 10187 ackbij2 10282 cff1 10298 fin23lem28 10380 fin23lem41 10392 pwfseqlem5 10703 hashf1lem1 14494 gsumzres 19927 gsumzcl2 19928 gsumzf1o 19930 gsumzaddlem 19939 gsumzmhm 19955 gsumzoppg 19962 lindfres 21843 islindf3 21846 dvne0f1 26051 istrkg2ld 28468 ausgrusgrb 29182 uspgrushgr 29194 usgruspgr 29197 uspgr1e 29261 sizusglecusglem1 29479 s1f1 32927 s2f1 32929 qqhre 34021 erdsze2lem1 35208 eldioph2lem2 42772 eldioph2 42773 fundcmpsurbijinjpreimafv 47394 fundcmpsurinjimaid 47398 stgrusgra 47926 usgrexmpl1lem 47980 usgrexmpl2lem 47985 gpgusgra 48012 |
| Copyright terms: Public domain | W3C validator |