![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rnmpo | Structured version Visualization version GIF version |
Description: The range of an operation given by the maps-to notation. (Contributed by FL, 20-Jun-2011.) |
Ref | Expression |
---|---|
rngop.1 | ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
Ref | Expression |
---|---|
rnmpo | ⊢ ran 𝐹 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = 𝐶} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rngop.1 | . . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | |
2 | df-mpo 7398 | . . . 4 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} | |
3 | 1, 2 | eqtri 2759 | . . 3 ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
4 | 3 | rneqi 5928 | . 2 ⊢ ran 𝐹 = ran {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
5 | rnoprab2 7497 | . 2 ⊢ ran {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = 𝐶} | |
6 | 4, 5 | eqtri 2759 | 1 ⊢ ran 𝐹 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = 𝐶} |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 396 = wceq 1541 ∈ wcel 2106 {cab 2708 ∃wrex 3069 ran crn 5670 {coprab 7394 ∈ cmpo 7395 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-sep 5292 ax-nul 5299 ax-pr 5420 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ral 3061 df-rex 3070 df-rab 3432 df-v 3475 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4319 df-if 4523 df-sn 4623 df-pr 4625 df-op 4629 df-br 5142 df-opab 5204 df-cnv 5677 df-dm 5679 df-rn 5680 df-oprab 7397 df-mpo 7398 |
This theorem is referenced by: elrnmpog 7527 elrnmpo 7528 ralrnmpo 7530 mpoexw 8047 dffi3 9408 ixpiunwdom 9567 qnnen 16138 txuni2 22998 txbas 23000 xkobval 23019 xkoopn 23022 txrest 23064 ptrescn 23072 tx1stc 23083 xkoptsub 23087 xkopt 23088 xkococn 23093 ptcmplem4 23488 met2ndci 23960 i1fadd 25141 i1fmul 25142 scutf 27239 mulsproplem9 27493 ssltmul1 27514 ssltmul2 27515 rnmposs 31768 cnre2csqima 32722 qqhval2 32793 icoreresf 36037 ptrest 36291 eldiophb 41266 |
Copyright terms: Public domain | W3C validator |