![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rnxpss | Structured version Visualization version GIF version |
Description: The range of a Cartesian product is included in its second factor. (Contributed by NM, 16-Jan-2006.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Ref | Expression |
---|---|
rnxpss | ⊢ ran (𝐴 × 𝐵) ⊆ 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rn 5693 | . 2 ⊢ ran (𝐴 × 𝐵) = dom ◡(𝐴 × 𝐵) | |
2 | cnvxp 6168 | . . . 4 ⊢ ◡(𝐴 × 𝐵) = (𝐵 × 𝐴) | |
3 | 2 | dmeqi 5911 | . . 3 ⊢ dom ◡(𝐴 × 𝐵) = dom (𝐵 × 𝐴) |
4 | dmxpss 6182 | . . 3 ⊢ dom (𝐵 × 𝐴) ⊆ 𝐵 | |
5 | 3, 4 | eqsstri 4014 | . 2 ⊢ dom ◡(𝐴 × 𝐵) ⊆ 𝐵 |
6 | 1, 5 | eqsstri 4014 | 1 ⊢ ran (𝐴 × 𝐵) ⊆ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ⊆ wss 3947 × cxp 5680 ◡ccnv 5681 dom cdm 5682 ran crn 5683 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-sep 5304 ax-nul 5311 ax-pr 5433 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-ral 3052 df-rab 3420 df-v 3464 df-dif 3950 df-un 3952 df-ss 3964 df-nul 4326 df-if 4534 df-sn 4634 df-pr 4636 df-op 4640 df-br 5154 df-opab 5216 df-xp 5688 df-rel 5689 df-cnv 5690 df-dm 5692 df-rn 5693 |
This theorem is referenced by: ssxpb 6185 ssrnres 6189 resssxp 6281 funssxp 6757 fconst 6788 dff2 7113 dff3 7114 fliftf 7327 frxp2 8158 frxp3 8165 marypha1lem 9476 marypha1 9477 dfac12lem2 10187 brdom4 10573 nqerf 10973 xptrrel 14985 lern 18616 cnconst2 23278 lmss 23293 tsmsxplem1 24148 causs 25317 i1f0 25707 itg10 25708 taylf 26388 noextendseq 27697 perpln2 28638 gsumpart 32923 locfinref 33656 sitg0 34180 heicant 37356 rntrclfvOAI 42348 rtrclex 43284 trclexi 43287 rtrclexi 43288 cnvtrcl0 43293 rntrcl 43295 brtrclfv2 43394 xphe 43448 rfovcnvf1od 43671 |
Copyright terms: Public domain | W3C validator |