![]() |
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 6495 | . . . . . . 7 ⊢ (𝐹:𝐶⟶𝐴 → dom 𝐹 = 𝐶) | |
2 | 1 | feq2d 6473 | . . . . . 6 ⊢ (𝐹:𝐶⟶𝐴 → (𝐹:dom 𝐹⟶𝐴 ↔ 𝐹:𝐶⟶𝐴)) |
3 | 1 | sseq1d 3946 | . . . . . 6 ⊢ (𝐹:𝐶⟶𝐴 → (dom 𝐹 ⊆ 𝐵 ↔ 𝐶 ⊆ 𝐵)) |
4 | 2, 3 | anbi12d 633 | . . . . 5 ⊢ (𝐹:𝐶⟶𝐴 → ((𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐵) ↔ (𝐹:𝐶⟶𝐴 ∧ 𝐶 ⊆ 𝐵))) |
5 | 4 | adantr 484 | . . . 4 ⊢ ((𝐹:𝐶⟶𝐴 ∧ 𝐶 ⊆ 𝐵) → ((𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐵) ↔ (𝐹:𝐶⟶𝐴 ∧ 𝐶 ⊆ 𝐵))) |
6 | 5 | ibir 271 | . . 3 ⊢ ((𝐹:𝐶⟶𝐴 ∧ 𝐶 ⊆ 𝐵) → (𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐵)) |
7 | elpm2g 8406 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐹 ∈ (𝐴 ↑pm 𝐵) ↔ (𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐵))) | |
8 | 6, 7 | syl5ibr 249 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐹:𝐶⟶𝐴 ∧ 𝐶 ⊆ 𝐵) → 𝐹 ∈ (𝐴 ↑pm 𝐵))) |
9 | 8 | imp 410 | 1 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐹:𝐶⟶𝐴 ∧ 𝐶 ⊆ 𝐵)) → 𝐹 ∈ (𝐴 ↑pm 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∈ wcel 2111 ⊆ wss 3881 dom cdm 5519 ⟶wf 6320 (class class class)co 7135 ↑pm cpm 8390 |
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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-ral 3111 df-rex 3112 df-rab 3115 df-v 3443 df-sbc 3721 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-fv 6332 df-ov 7138 df-oprab 7139 df-mpo 7140 df-pm 8392 |
This theorem is referenced by: fpmg 8415 pmresg 8417 rlim 14844 ello12 14865 elo12 14876 sscpwex 17077 catcfuccl 17361 catcxpccl 17449 lmbrf 21865 cnextfval 22667 lmmbrf 23866 iscauf 23884 caucfil 23887 cmetcaulem 23892 lmclimf 23908 ismbf 24232 ismbfcn 24233 mbfconst 24237 cncombf 24262 cnmbf 24263 limcfval 24475 dvfval 24500 dvnff 24526 dvn2bss 24533 dvnfre 24555 taylfvallem1 24952 taylfval 24954 tayl0 24957 taylplem1 24958 taylply2 24963 taylply 24964 dvtaylp 24965 dvntaylp 24966 dvntaylp0 24967 taylthlem1 24968 taylthlem2 24969 ulmval 24975 ulmpm 24978 iscgrgd 26307 esumcvg 31455 mrsubfval 32868 elmrsubrn 32880 msubfval 32884 fwddifval 33736 fwddifnval 33737 fpmd 41903 xlimmnfvlem2 42475 xlimpnfvlem2 42479 dvnmptdivc 42580 dvnxpaek 42584 etransclem46 42922 issmflem 43361 fdivpm 44957 refdivpm 44958 elbigo2 44966 |
Copyright terms: Public domain | W3C validator |