Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > rnmptss | Structured version Visualization version GIF version |
Description: The range of an operation given by the maps-to notation as a subset. (Contributed by Thierry Arnoux, 24-Sep-2017.) |
Ref | Expression |
---|---|
rnmptss.1 | ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) |
Ref | Expression |
---|---|
rnmptss | ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran 𝐹 ⊆ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rnmptss.1 | . . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) | |
2 | 1 | fmpt 6866 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ 𝐹:𝐴⟶𝐶) |
3 | frn 6513 | . 2 ⊢ (𝐹:𝐴⟶𝐶 → ran 𝐹 ⊆ 𝐶) | |
4 | 2, 3 | sylbi 218 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran 𝐹 ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ∈ wcel 2105 ∀wral 3135 ⊆ wss 3933 ↦ cmpt 5137 ran crn 5549 ⟶wf 6344 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 ax-nul 5201 ax-pr 5320 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2615 df-eu 2647 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ne 3014 df-ral 3140 df-rex 3141 df-rab 3144 df-v 3494 df-sbc 3770 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4831 df-br 5058 df-opab 5120 df-mpt 5138 df-id 5453 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-res 5560 df-ima 5561 df-iota 6307 df-fun 6350 df-fn 6351 df-f 6352 df-fv 6356 |
This theorem is referenced by: mptexw 7643 iunon 7965 iinon 7966 gruiun 10209 subdrgint 19511 smadiadetlem3lem2 21204 tgiun 21515 ustuqtop0 22776 metustss 23088 efabl 25061 efsubm 25062 fnpreimac 30344 swrdrn2 30555 gsummpt2co 30613 psgnfzto1stlem 30669 locfinreflem 31003 prodindf 31181 gsumesum 31217 esumlub 31218 esumgect 31248 esum2d 31251 ldgenpisyslem1 31321 sxbrsigalem0 31428 omscl 31452 omsmon 31455 carsgclctunlem2 31476 carsgclctunlem3 31477 pmeasadd 31482 hgt750lemb 31826 mnurndlem2 40495 suprnmpt 41306 rnmptssrn 41318 wessf1ornlem 41321 rnmptssd 41334 rnmptssbi 41410 liminflelimsuplem 41932 fourierdlem31 42300 fourierdlem53 42321 fourierdlem111 42379 ioorrnopnlem 42466 saliuncl 42484 salexct3 42502 salgensscntex 42504 sge0rnre 42523 sge0tsms 42539 sge0cl 42540 sge0fsum 42546 sge0sup 42550 sge0gerp 42554 sge0pnffigt 42555 sge0lefi 42557 sge0xaddlem1 42592 sge0xaddlem2 42593 meadjiunlem 42624 meadjiun 42625 |
Copyright terms: Public domain | W3C validator |