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 6381 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ 𝐹:𝐴⟶𝐶) |
3 | frn 6053 | . 2 ⊢ (𝐹:𝐴⟶𝐶 → ran 𝐹 ⊆ 𝐶) | |
4 | 2, 3 | sylbi 207 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran 𝐹 ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1483 ∈ wcel 1990 ∀wral 2912 ⊆ wss 3574 ↦ cmpt 4729 ran crn 5115 ⟶wf 5884 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pr 4906 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-sbc 3436 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-opab 4713 df-mpt 4730 df-id 5024 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-fv 5896 |
This theorem is referenced by: iunon 7436 iinon 7437 gruiun 9621 smadiadetlem3lem2 20473 tgiun 20783 ustuqtop0 22044 metustss 22356 efabl 24296 efsubm 24297 gsummpt2co 29780 psgnfzto1stlem 29850 locfinreflem 29907 prodindf 30085 gsumesum 30121 esumlub 30122 esumgect 30152 esum2d 30155 ldgenpisyslem1 30226 sxbrsigalem0 30333 omscl 30357 omsmon 30360 carsgclctunlem2 30381 carsgclctunlem3 30382 pmeasadd 30387 hgt750lemb 30734 suprnmpt 39355 rnmptssrn 39368 wessf1ornlem 39371 rnmptssd 39385 rnmptssbi 39477 liminflelimsuplem 40007 fourierdlem31 40355 fourierdlem53 40376 fourierdlem111 40434 ioorrnopnlem 40524 saliuncl 40542 salexct3 40560 salgensscntex 40562 sge0rnre 40581 sge0tsms 40597 sge0cl 40598 sge0fsum 40604 sge0sup 40608 sge0gerp 40612 sge0pnffigt 40613 sge0lefi 40615 sge0xaddlem1 40650 sge0xaddlem2 40651 meadjiunlem 40682 meadjiun 40683 |
Copyright terms: Public domain | W3C validator |