![]() |
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 17308 | . . 3 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐽 ↾t 𝐵) = ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵))) | |
2 | 1 | eleq2d 2823 | . 2 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (𝐽 ↾t 𝐵) ↔ 𝐴 ∈ ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)))) |
3 | eqid 2736 | . . 3 ⊢ (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)) = (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)) | |
4 | vex 3449 | . . . 4 ⊢ 𝑥 ∈ V | |
5 | 4 | inex1 5274 | . . 3 ⊢ (𝑥 ∩ 𝐵) ∈ V |
6 | 3, 5 | elrnmpti 5915 | . 2 ⊢ (𝐴 ∈ ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐵)) ↔ ∃𝑥 ∈ 𝐽 𝐴 = (𝑥 ∩ 𝐵)) |
7 | 2, 6 | bitrdi 286 | 1 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (𝐽 ↾t 𝐵) ↔ ∃𝑥 ∈ 𝐽 𝐴 = (𝑥 ∩ 𝐵))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ∃wrex 3073 ∩ cin 3909 ↦ cmpt 5188 ran crn 5634 (class class class)co 7357 ↾t crest 17302 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pr 5384 ax-un 7672 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-ral 3065 df-rex 3074 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-id 5531 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-ov 7360 df-oprab 7361 df-mpo 7362 df-rest 17304 |
This theorem is referenced by: elrestr 17310 restsspw 17313 firest 17314 restbas 22509 restsn 22521 restcld 22523 restopnb 22526 ssrest 22527 neitr 22531 restntr 22533 cnrest2 22637 cnpresti 22639 cnprest 22640 cnprest2 22641 lmss 22649 cmpsublem 22750 cmpsub 22751 connsuba 22771 1stcrest 22804 subislly 22832 cldllycmp 22846 txrest 22982 trfbas2 23194 trfbas 23195 trfil2 23238 flimrest 23334 fclsrest 23375 cnextcn 23418 tsmssubm 23494 trust 23581 restutop 23589 restutopopn 23590 trcfilu 23646 metrest 23880 xrtgioo 24169 xrge0tsms 24197 icoopnst 24302 iocopnst 24303 subopnmbl 24968 mbfimaopn2 25021 xrlimcnp 26318 xrge0tsmsd 31899 rspectopn 32448 bj-restsn 35553 bj-rest10 35559 bj-restn0 35561 bj-restpw 35563 bj-rest0 35564 bj-restb 35565 bj-restuni 35568 bj-restreg 35570 ptrest 36077 poimirlem29 36107 elrestd 43308 restuni3 43318 restsubel 43358 icccncfext 44118 subsaliuncl 44589 subsalsal 44590 salrestss 44592 sssmf 44969 incsmf 44973 decsmf 44998 smflimlem6 45007 smfco 45033 smfpimcc 45039 |
Copyright terms: Public domain | W3C validator |