![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elrest | Structured version Visualization version GIF version |
Description: The predicate "is an open set of a subspace topology". (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) |
Ref | Expression |
---|---|
elrest | ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (𝐽 ↾t 𝐵) ↔ ∃𝑥 ∈ 𝐽 𝐴 = (𝑥 ∩ 𝐵))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | restval 16534 | . . 3 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐽 ↾t 𝐵) = ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵))) | |
2 | 1 | eleq2d 2868 | . 2 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (𝐽 ↾t 𝐵) ↔ 𝐴 ∈ ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)))) |
3 | eqid 2795 | . . 3 ⊢ (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)) = (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)) | |
4 | vex 3440 | . . . 4 ⊢ 𝑥 ∈ V | |
5 | 4 | inex1 5117 | . . 3 ⊢ (𝑥 ∩ 𝐵) ∈ V |
6 | 3, 5 | elrnmpti 5719 | . 2 ⊢ (𝐴 ∈ ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)) ↔ ∃𝑥 ∈ 𝐽 𝐴 = (𝑥 ∩ 𝐵)) |
7 | 2, 6 | syl6bb 288 | 1 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (𝐽 ↾t 𝐵) ↔ ∃𝑥 ∈ 𝐽 𝐴 = (𝑥 ∩ 𝐵))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1522 ∈ wcel 2081 ∃wrex 3106 ∩ cin 3862 ↦ cmpt 5045 ran crn 5449 (class class class)co 7021 ↾t crest 16528 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-rep 5086 ax-sep 5099 ax-nul 5106 ax-pr 5226 ax-un 7324 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-ral 3110 df-rex 3111 df-reu 3112 df-rab 3114 df-v 3439 df-sbc 3710 df-csb 3816 df-dif 3866 df-un 3868 df-in 3870 df-ss 3878 df-nul 4216 df-if 4386 df-sn 4477 df-pr 4479 df-op 4483 df-uni 4750 df-iun 4831 df-br 4967 df-opab 5029 df-mpt 5046 df-id 5353 df-xp 5454 df-rel 5455 df-cnv 5456 df-co 5457 df-dm 5458 df-rn 5459 df-res 5460 df-ima 5461 df-iota 6194 df-fun 6232 df-fn 6233 df-f 6234 df-f1 6235 df-fo 6236 df-f1o 6237 df-fv 6238 df-ov 7024 df-oprab 7025 df-mpo 7026 df-rest 16530 |
This theorem is referenced by: elrestr 16536 restsspw 16539 firest 16540 restbas 21455 restsn 21467 restcld 21469 restopnb 21472 ssrest 21473 neitr 21477 restntr 21479 cnrest2 21583 cnpresti 21585 cnprest 21586 cnprest2 21587 lmss 21595 cmpsublem 21696 cmpsub 21697 connsuba 21717 1stcrest 21750 subislly 21778 cldllycmp 21792 txrest 21928 trfbas2 22140 trfbas 22141 trfil2 22184 flimrest 22280 fclsrest 22321 cnextcn 22364 tsmssubm 22439 trust 22526 restutop 22534 restutopopn 22535 trcfilu 22591 metrest 22822 xrtgioo 23102 xrge0tsms 23130 icoopnst 23231 iocopnst 23232 subopnmbl 23893 mbfimaopn2 23946 xrlimcnp 25233 xrge0tsmsd 30508 bj-restsn 33997 bj-rest10 34003 bj-restn0 34005 bj-restpw 34007 bj-rest0 34008 bj-restb 34009 bj-restuni 34012 bj-restreg 34014 ptrest 34447 poimirlem29 34477 elrestd 40939 restuni3 40949 icccncfext 41737 subsaliuncl 42209 subsalsal 42210 sssmf 42583 incsmf 42587 decsmf 42611 smflimlem6 42620 smfco 42645 smfpimcc 42650 |
Copyright terms: Public domain | W3C validator |