![]() |
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 6549 | . . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵) | |
2 | fss 6501 | . . 3 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶) | |
3 | 1, 2 | sylan 583 | . 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶) |
4 | df-f1 6329 | . . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)) | |
5 | 4 | simprbi 500 | . . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹) |
6 | 5 | adantr 484 | . 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → Fun ◡𝐹) |
7 | df-f1 6329 | . 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹)) | |
8 | 3, 6, 7 | sylanbrc 586 | 1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴–1-1→𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ⊆ wss 3881 ◡ccnv 5518 Fun wfun 6318 ⟶wf 6320 –1-1→wf1 6321 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-v 3443 df-in 3888 df-ss 3898 df-f 6328 df-f1 6329 |
This theorem is referenced by: f1sng 6631 f1prex 7018 domssex2 8661 1sdom 8705 marypha1lem 8881 marypha2 8887 isinffi 9405 fseqenlem1 9435 dfac12r 9557 ackbij2 9654 cff1 9669 fin23lem28 9751 fin23lem41 9763 pwfseqlem5 10074 hashf1lem1 13809 gsumzres 19022 gsumzcl2 19023 gsumzf1o 19025 gsumzaddlem 19034 gsumzmhm 19050 gsumzoppg 19057 lindfres 20512 islindf3 20515 dvne0f1 24615 istrkg2ld 26254 ausgrusgrb 26958 uspgrushgr 26968 usgruspgr 26971 uspgr1e 27034 sizusglecusglem1 27251 s1f1 30645 s2f1 30647 qqhre 31371 erdsze2lem1 32563 eldioph2lem2 39702 eldioph2 39703 fundcmpsurbijinjpreimafv 43924 fundcmpsurinjimaid 43928 |
Copyright terms: Public domain | W3C validator |