![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mpt2fun | Structured version Visualization version GIF version |
Description: The maps-to notation for an operation is always a function. (Contributed by Scott Fenton, 21-Mar-2012.) |
Ref | Expression |
---|---|
mpt2fun.1 | ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
Ref | Expression |
---|---|
mpt2fun | ⊢ Fun 𝐹 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqtr3 2773 | . . . . . 6 ⊢ ((𝑧 = 𝐶 ∧ 𝑤 = 𝐶) → 𝑧 = 𝑤) | |
2 | 1 | ad2ant2l 799 | . . . . 5 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)) → 𝑧 = 𝑤) |
3 | 2 | gen2 1864 | . . . 4 ⊢ ∀𝑧∀𝑤((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)) → 𝑧 = 𝑤) |
4 | eqeq1 2756 | . . . . . 6 ⊢ (𝑧 = 𝑤 → (𝑧 = 𝐶 ↔ 𝑤 = 𝐶)) | |
5 | 4 | anbi2d 742 | . . . . 5 ⊢ (𝑧 = 𝑤 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))) |
6 | 5 | mo4 2647 | . . . 4 ⊢ (∃*𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ∀𝑧∀𝑤((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)) → 𝑧 = 𝑤)) |
7 | 3, 6 | mpbir 221 | . . 3 ⊢ ∃*𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) |
8 | 7 | funoprab 6917 | . 2 ⊢ Fun {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
9 | mpt2fun.1 | . . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | |
10 | df-mpt2 6810 | . . . 4 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} | |
11 | 9, 10 | eqtri 2774 | . . 3 ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
12 | 11 | funeqi 6062 | . 2 ⊢ (Fun 𝐹 ↔ Fun {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}) |
13 | 8, 12 | mpbir 221 | 1 ⊢ Fun 𝐹 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∀wal 1622 = wceq 1624 ∈ wcel 2131 ∃*wmo 2600 Fun wfun 6035 {coprab 6806 ↦ cmpt2 6807 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-9 2140 ax-10 2160 ax-11 2175 ax-12 2188 ax-13 2383 ax-ext 2732 ax-sep 4925 ax-nul 4933 ax-pr 5047 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1627 df-ex 1846 df-nf 1851 df-sb 2039 df-eu 2603 df-mo 2604 df-clab 2739 df-cleq 2745 df-clel 2748 df-nfc 2883 df-ral 3047 df-rab 3051 df-v 3334 df-dif 3710 df-un 3712 df-in 3714 df-ss 3721 df-nul 4051 df-if 4223 df-sn 4314 df-pr 4316 df-op 4320 df-br 4797 df-opab 4857 df-id 5166 df-xp 5264 df-rel 5265 df-cnv 5266 df-co 5267 df-fun 6043 df-oprab 6809 df-mpt2 6810 |
This theorem is referenced by: ofexg 7058 mpt2exxg 7404 mpt2curryd 7556 imasvscafn 16391 coapm 16914 oppglsm 18249 gsum2d2lem 18564 evlslem2 19706 xkococnlem 21656 ucnima 22278 ucnprima 22279 fmucnd 22289 smatrcl 30163 smatlem 30164 txomap 30202 tpr2rico 30259 elunirnmbfm 30616 scutf 32217 relowlpssretop 33515 aovmpt4g 41779 mpt2exxg2 42618 |
Copyright terms: Public domain | W3C validator |