Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mpt20 | Structured version Visualization version GIF version |
Description: A mapping operation with empty domain. (Contributed by Stefan O'Rear, 29-Jan-2015.) (Revised by Mario Carneiro, 15-May-2015.) |
Ref | Expression |
---|---|
mpt20 | ⊢ (𝑥 ∈ ∅, 𝑦 ∈ 𝐵 ↦ 𝐶) = ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-mpt2 6554 | . 2 ⊢ (𝑥 ∈ ∅, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} | |
2 | df-oprab 6553 | . 2 ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ ((𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶))} | |
3 | noel 3878 | . . . . . . 7 ⊢ ¬ 𝑥 ∈ ∅ | |
4 | simprll 798 | . . . . . . 7 ⊢ ((𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ ((𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)) → 𝑥 ∈ ∅) | |
5 | 3, 4 | mto 187 | . . . . . 6 ⊢ ¬ (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ ((𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)) |
6 | 5 | nex 1722 | . . . . 5 ⊢ ¬ ∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ ((𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)) |
7 | 6 | nex 1722 | . . . 4 ⊢ ¬ ∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ ((𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)) |
8 | 7 | nex 1722 | . . 3 ⊢ ¬ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ ((𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)) |
9 | 8 | abf 3930 | . 2 ⊢ {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ ((𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶))} = ∅ |
10 | 1, 2, 9 | 3eqtri 2636 | 1 ⊢ (𝑥 ∈ ∅, 𝑦 ∈ 𝐵 ↦ 𝐶) = ∅ |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 383 = wceq 1475 ∃wex 1695 ∈ wcel 1977 {cab 2596 ∅c0 3874 〈cop 4131 {coprab 6550 ↦ cmpt2 6551 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-dif 3543 df-nul 3875 df-oprab 6553 df-mpt2 6554 |
This theorem is referenced by: homffval 16173 comfffval 16181 natfval 16429 coafval 16537 xpchomfval 16642 xpccofval 16645 plusffval 17070 grpsubfval 17287 oppglsm 17880 dvrfval 18507 scaffval 18704 psrmulr 19205 ipffval 19812 marrepfval 20185 marepvfval 20190 d0mat2pmat 20362 pcofval 22618 mendplusgfval 36774 mendmulrfval 36776 mendvscafval 36779 |
Copyright terms: Public domain | W3C validator |