![]() |
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 6739 | . . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵) | |
2 | fss 6686 | . . 3 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶) | |
3 | 1, 2 | sylan 581 | . 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶) |
4 | df-f1 6502 | . . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)) | |
5 | 4 | simprbi 498 | . . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹) |
6 | 5 | adantr 482 | . 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → Fun ◡𝐹) |
7 | df-f1 6502 | . 2 ⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ Fun ◡𝐹)) | |
8 | 3, 6, 7 | sylanbrc 584 | 1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴–1-1→𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ⊆ wss 3911 ◡ccnv 5633 Fun wfun 6491 ⟶wf 6493 –1-1→wf1 6494 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-v 3448 df-in 3918 df-ss 3928 df-f 6501 df-f1 6502 |
This theorem is referenced by: f1un 6805 f1sng 6827 f1prex 7231 domssr 8940 domssex2 9082 ssdomfi 9144 ssdomfi2 9145 1sdomOLD 9194 marypha1lem 9370 marypha2 9376 isinffi 9929 fseqenlem1 9961 dfac12r 10083 ackbij2 10180 cff1 10195 fin23lem28 10277 fin23lem41 10289 pwfseqlem5 10600 hashf1lem1 14354 hashf1lem1OLD 14355 gsumzres 19687 gsumzcl2 19688 gsumzf1o 19690 gsumzaddlem 19699 gsumzmhm 19715 gsumzoppg 19722 lindfres 21232 islindf3 21235 dvne0f1 25379 istrkg2ld 27405 ausgrusgrb 28119 uspgrushgr 28129 usgruspgr 28132 uspgr1e 28195 sizusglecusglem1 28412 s1f1 31802 s2f1 31804 qqhre 32604 erdsze2lem1 33800 eldioph2lem2 41087 eldioph2 41088 fundcmpsurbijinjpreimafv 45606 fundcmpsurinjimaid 45610 |
Copyright terms: Public domain | W3C validator |