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 6522 | . . . . . . 7 ⊢ (𝐹:𝐶⟶𝐴 → dom 𝐹 = 𝐶) | |
2 | 1 | feq2d 6500 | . . . . . 6 ⊢ (𝐹:𝐶⟶𝐴 → (𝐹:dom 𝐹⟶𝐴 ↔ 𝐹:𝐶⟶𝐴)) |
3 | 1 | sseq1d 3998 | . . . . . 6 ⊢ (𝐹:𝐶⟶𝐴 → (dom 𝐹 ⊆ 𝐵 ↔ 𝐶 ⊆ 𝐵)) |
4 | 2, 3 | anbi12d 632 | . . . . 5 ⊢ (𝐹:𝐶⟶𝐴 → ((𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐵) ↔ (𝐹:𝐶⟶𝐴 ∧ 𝐶 ⊆ 𝐵))) |
5 | 4 | adantr 483 | . . . 4 ⊢ ((𝐹:𝐶⟶𝐴 ∧ 𝐶 ⊆ 𝐵) → ((𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐵) ↔ (𝐹:𝐶⟶𝐴 ∧ 𝐶 ⊆ 𝐵))) |
6 | 5 | ibir 270 | . . 3 ⊢ ((𝐹:𝐶⟶𝐴 ∧ 𝐶 ⊆ 𝐵) → (𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐵)) |
7 | elpm2g 8423 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐹 ∈ (𝐴 ↑pm 𝐵) ↔ (𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐵))) | |
8 | 6, 7 | syl5ibr 248 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐹:𝐶⟶𝐴 ∧ 𝐶 ⊆ 𝐵) → 𝐹 ∈ (𝐴 ↑pm 𝐵))) |
9 | 8 | imp 409 | 1 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐹:𝐶⟶𝐴 ∧ 𝐶 ⊆ 𝐵)) → 𝐹 ∈ (𝐴 ↑pm 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∈ wcel 2114 ⊆ wss 3936 dom cdm 5555 ⟶wf 6351 (class class class)co 7156 ↑pm cpm 8407 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 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 3496 df-sbc 3773 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4839 df-br 5067 df-opab 5129 df-id 5460 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-fv 6363 df-ov 7159 df-oprab 7160 df-mpo 7161 df-pm 8409 |
This theorem is referenced by: fpmg 8432 pmresg 8434 rlim 14852 ello12 14873 elo12 14884 sscpwex 17085 catcfuccl 17369 catcxpccl 17457 lmbrf 21868 cnextfval 22670 lmmbrf 23865 iscauf 23883 caucfil 23886 cmetcaulem 23891 lmclimf 23907 ismbf 24229 ismbfcn 24230 mbfconst 24234 cncombf 24259 cnmbf 24260 limcfval 24470 dvfval 24495 dvnff 24520 dvn2bss 24527 dvnfre 24549 taylfvallem1 24945 taylfval 24947 tayl0 24950 taylplem1 24951 taylply2 24956 taylply 24957 dvtaylp 24958 dvntaylp 24959 dvntaylp0 24960 taylthlem1 24961 taylthlem2 24962 ulmval 24968 ulmpm 24971 iscgrgd 26299 esumcvg 31345 mrsubfval 32755 elmrsubrn 32767 msubfval 32771 fwddifval 33623 fwddifnval 33624 fpmd 41558 xlimmnfvlem2 42134 xlimpnfvlem2 42138 dvnmptdivc 42243 dvnxpaek 42247 etransclem46 42585 issmflem 43024 fdivpm 44623 refdivpm 44624 elbigo2 44632 |
Copyright terms: Public domain | W3C validator |