![]() |
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 17313 | . . 3 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐽 ↾t 𝐵) = ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵))) | |
2 | 1 | eleq2d 2820 | . 2 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (𝐽 ↾t 𝐵) ↔ 𝐴 ∈ ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)))) |
3 | eqid 2733 | . . 3 ⊢ (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)) = (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)) | |
4 | vex 3448 | . . . 4 ⊢ 𝑥 ∈ V | |
5 | 4 | inex1 5275 | . . 3 ⊢ (𝑥 ∩ 𝐵) ∈ V |
6 | 3, 5 | elrnmpti 5916 | . 2 ⊢ (𝐴 ∈ ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)) ↔ ∃𝑥 ∈ 𝐽 𝐴 = (𝑥 ∩ 𝐵)) |
7 | 2, 6 | bitrdi 287 | 1 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (𝐽 ↾t 𝐵) ↔ ∃𝑥 ∈ 𝐽 𝐴 = (𝑥 ∩ 𝐵))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 ∈ wcel 2107 ∃wrex 3070 ∩ cin 3910 ↦ cmpt 5189 ran crn 5635 (class class class)co 7358 ↾t crest 17307 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5243 ax-sep 5257 ax-nul 5264 ax-pr 5385 ax-un 7673 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2941 df-ral 3062 df-rex 3071 df-reu 3353 df-rab 3407 df-v 3446 df-sbc 3741 df-csb 3857 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4284 df-if 4488 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4867 df-iun 4957 df-br 5107 df-opab 5169 df-mpt 5190 df-id 5532 df-xp 5640 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-rn 5645 df-res 5646 df-ima 5647 df-iota 6449 df-fun 6499 df-fn 6500 df-f 6501 df-f1 6502 df-fo 6503 df-f1o 6504 df-fv 6505 df-ov 7361 df-oprab 7362 df-mpo 7363 df-rest 17309 |
This theorem is referenced by: elrestr 17315 restsspw 17318 firest 17319 restbas 22525 restsn 22537 restcld 22539 restopnb 22542 ssrest 22543 neitr 22547 restntr 22549 cnrest2 22653 cnpresti 22655 cnprest 22656 cnprest2 22657 lmss 22665 cmpsublem 22766 cmpsub 22767 connsuba 22787 1stcrest 22820 subislly 22848 cldllycmp 22862 txrest 22998 trfbas2 23210 trfbas 23211 trfil2 23254 flimrest 23350 fclsrest 23391 cnextcn 23434 tsmssubm 23510 trust 23597 restutop 23605 restutopopn 23606 trcfilu 23662 metrest 23896 xrtgioo 24185 xrge0tsms 24213 icoopnst 24318 iocopnst 24319 subopnmbl 24984 mbfimaopn2 25037 xrlimcnp 26334 xrge0tsmsd 31948 rspectopn 32505 bj-restsn 35599 bj-rest10 35605 bj-restn0 35607 bj-restpw 35609 bj-rest0 35610 bj-restb 35611 bj-restuni 35614 bj-restreg 35616 ptrest 36123 poimirlem29 36153 elrestd 43406 restuni3 43416 restsubel 43456 icccncfext 44214 subsaliuncl 44685 subsalsal 44686 salrestss 44688 sssmf 45065 incsmf 45069 decsmf 45094 smflimlem6 45103 smfco 45129 smfpimcc 45135 |
Copyright terms: Public domain | W3C validator |