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 16885 | . . 3 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐽 ↾t 𝐵) = ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵))) | |
2 | 1 | eleq2d 2816 | . 2 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (𝐽 ↾t 𝐵) ↔ 𝐴 ∈ ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)))) |
3 | eqid 2736 | . . 3 ⊢ (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)) = (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)) | |
4 | vex 3402 | . . . 4 ⊢ 𝑥 ∈ V | |
5 | 4 | inex1 5195 | . . 3 ⊢ (𝑥 ∩ 𝐵) ∈ V |
6 | 3, 5 | elrnmpti 5814 | . 2 ⊢ (𝐴 ∈ ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)) ↔ ∃𝑥 ∈ 𝐽 𝐴 = (𝑥 ∩ 𝐵)) |
7 | 2, 6 | bitrdi 290 | 1 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (𝐽 ↾t 𝐵) ↔ ∃𝑥 ∈ 𝐽 𝐴 = (𝑥 ∩ 𝐵))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1543 ∈ wcel 2112 ∃wrex 3052 ∩ cin 3852 ↦ cmpt 5120 ran crn 5537 (class class class)co 7191 ↾t crest 16879 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2708 ax-rep 5164 ax-sep 5177 ax-nul 5184 ax-pr 5307 ax-un 7501 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2728 df-clel 2809 df-nfc 2879 df-ne 2933 df-ral 3056 df-rex 3057 df-reu 3058 df-rab 3060 df-v 3400 df-sbc 3684 df-csb 3799 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-nul 4224 df-if 4426 df-sn 4528 df-pr 4530 df-op 4534 df-uni 4806 df-iun 4892 df-br 5040 df-opab 5102 df-mpt 5121 df-id 5440 df-xp 5542 df-rel 5543 df-cnv 5544 df-co 5545 df-dm 5546 df-rn 5547 df-res 5548 df-ima 5549 df-iota 6316 df-fun 6360 df-fn 6361 df-f 6362 df-f1 6363 df-fo 6364 df-f1o 6365 df-fv 6366 df-ov 7194 df-oprab 7195 df-mpo 7196 df-rest 16881 |
This theorem is referenced by: elrestr 16887 restsspw 16890 firest 16891 restbas 22009 restsn 22021 restcld 22023 restopnb 22026 ssrest 22027 neitr 22031 restntr 22033 cnrest2 22137 cnpresti 22139 cnprest 22140 cnprest2 22141 lmss 22149 cmpsublem 22250 cmpsub 22251 connsuba 22271 1stcrest 22304 subislly 22332 cldllycmp 22346 txrest 22482 trfbas2 22694 trfbas 22695 trfil2 22738 flimrest 22834 fclsrest 22875 cnextcn 22918 tsmssubm 22994 trust 23081 restutop 23089 restutopopn 23090 trcfilu 23145 metrest 23376 xrtgioo 23657 xrge0tsms 23685 icoopnst 23790 iocopnst 23791 subopnmbl 24455 mbfimaopn2 24508 xrlimcnp 25805 xrge0tsmsd 30990 rspectopn 31485 bj-restsn 34937 bj-rest10 34943 bj-restn0 34945 bj-restpw 34947 bj-rest0 34948 bj-restb 34949 bj-restuni 34952 bj-restreg 34954 ptrest 35462 poimirlem29 35492 elrestd 42272 restuni3 42281 icccncfext 43046 subsaliuncl 43515 subsalsal 43516 sssmf 43889 incsmf 43893 decsmf 43917 smflimlem6 43926 smfco 43951 smfpimcc 43956 |
Copyright terms: Public domain | W3C validator |