Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > elpm2r | Structured version Visualization version GIF version |
Description: Sufficient condition for being a partial function. (Contributed by NM, 31-Dec-2013.) |
Ref | Expression |
---|---|
elpm2r | ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐹:𝐶⟶𝐴 ∧ 𝐶 ⊆ 𝐵)) → 𝐹 ∈ (𝐴 ↑pm 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fdm 6516 | . . . . . . 7 ⊢ (𝐹:𝐶⟶𝐴 → dom 𝐹 = 𝐶) | |
2 | 1 | feq2d 6494 | . . . . . 6 ⊢ (𝐹:𝐶⟶𝐴 → (𝐹:dom 𝐹⟶𝐴 ↔ 𝐹:𝐶⟶𝐴)) |
3 | 1 | sseq1d 3997 | . . . . . 6 ⊢ (𝐹:𝐶⟶𝐴 → (dom 𝐹 ⊆ 𝐵 ↔ 𝐶 ⊆ 𝐵)) |
4 | 2, 3 | anbi12d 630 | . . . . 5 ⊢ (𝐹:𝐶⟶𝐴 → ((𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐵) ↔ (𝐹:𝐶⟶𝐴 ∧ 𝐶 ⊆ 𝐵))) |
5 | 4 | adantr 481 | . . . 4 ⊢ ((𝐹:𝐶⟶𝐴 ∧ 𝐶 ⊆ 𝐵) → ((𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐵) ↔ (𝐹:𝐶⟶𝐴 ∧ 𝐶 ⊆ 𝐵))) |
6 | 5 | ibir 269 | . . 3 ⊢ ((𝐹:𝐶⟶𝐴 ∧ 𝐶 ⊆ 𝐵) → (𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐵)) |
7 | elpm2g 8413 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐹 ∈ (𝐴 ↑pm 𝐵) ↔ (𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐵))) | |
8 | 6, 7 | syl5ibr 247 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐹:𝐶⟶𝐴 ∧ 𝐶 ⊆ 𝐵) → 𝐹 ∈ (𝐴 ↑pm 𝐵))) |
9 | 8 | imp 407 | 1 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐹:𝐶⟶𝐴 ∧ 𝐶 ⊆ 𝐵)) → 𝐹 ∈ (𝐴 ↑pm 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 ∈ wcel 2105 ⊆ wss 3935 dom cdm 5549 ⟶wf 6345 (class class class)co 7145 ↑pm cpm 8397 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 ax-un 7450 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3497 df-sbc 3772 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4466 df-pw 4539 df-sn 4560 df-pr 4562 df-op 4566 df-uni 4833 df-br 5059 df-opab 5121 df-id 5454 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-iota 6308 df-fun 6351 df-fn 6352 df-f 6353 df-fv 6357 df-ov 7148 df-oprab 7149 df-mpo 7150 df-pm 8399 |
This theorem is referenced by: fpmg 8422 pmresg 8424 rlim 14842 ello12 14863 elo12 14874 sscpwex 17075 catcfuccl 17359 catcxpccl 17447 lmbrf 21798 cnextfval 22600 lmmbrf 23794 iscauf 23812 caucfil 23815 cmetcaulem 23820 lmclimf 23836 ismbf 24158 ismbfcn 24159 mbfconst 24163 cncombf 24188 cnmbf 24189 limcfval 24399 dvfval 24424 dvnff 24449 dvn2bss 24456 dvnfre 24478 taylfvallem1 24874 taylfval 24876 tayl0 24879 taylplem1 24880 taylply2 24885 taylply 24886 dvtaylp 24887 dvntaylp 24888 dvntaylp0 24889 taylthlem1 24890 taylthlem2 24891 ulmval 24897 ulmpm 24900 iscgrgd 26227 esumcvg 31245 mrsubfval 32653 elmrsubrn 32665 msubfval 32669 fwddifval 33521 fwddifnval 33522 fpmd 41418 xlimmnfvlem2 41994 xlimpnfvlem2 41998 dvnmptdivc 42103 dvnxpaek 42107 etransclem46 42446 issmflem 42885 fdivpm 44501 refdivpm 44502 elbigo2 44510 |
Copyright terms: Public domain | W3C validator |