![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elrestr | Structured version Visualization version GIF version |
Description: Sufficient condition for being an open set in a subspace. (Contributed by Jeff Hankins, 11-Jul-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) |
Ref | Expression |
---|---|
elrestr | ⊢ ((𝐽 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐴 ∈ 𝐽) → (𝐴 ∩ 𝑆) ∈ (𝐽 ↾t 𝑆)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2798 | . . . 4 ⊢ (𝐴 ∩ 𝑆) = (𝐴 ∩ 𝑆) | |
2 | ineq1 4131 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝑆) = (𝐴 ∩ 𝑆)) | |
3 | 2 | rspceeqv 3586 | . . . 4 ⊢ ((𝐴 ∈ 𝐽 ∧ (𝐴 ∩ 𝑆) = (𝐴 ∩ 𝑆)) → ∃𝑥 ∈ 𝐽 (𝐴 ∩ 𝑆) = (𝑥 ∩ 𝑆)) |
4 | 1, 3 | mpan2 690 | . . 3 ⊢ (𝐴 ∈ 𝐽 → ∃𝑥 ∈ 𝐽 (𝐴 ∩ 𝑆) = (𝑥 ∩ 𝑆)) |
5 | elrest 16693 | . . 3 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → ((𝐴 ∩ 𝑆) ∈ (𝐽 ↾t 𝑆) ↔ ∃𝑥 ∈ 𝐽 (𝐴 ∩ 𝑆) = (𝑥 ∩ 𝑆))) | |
6 | 4, 5 | syl5ibr 249 | . 2 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (𝐴 ∈ 𝐽 → (𝐴 ∩ 𝑆) ∈ (𝐽 ↾t 𝑆))) |
7 | 6 | 3impia 1114 | 1 ⊢ ((𝐽 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐴 ∈ 𝐽) → (𝐴 ∩ 𝑆) ∈ (𝐽 ↾t 𝑆)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1084 = wceq 1538 ∈ wcel 2111 ∃wrex 3107 ∩ cin 3880 (class class class)co 7135 ↾t crest 16686 |
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-rep 5154 ax-sep 5167 ax-nul 5174 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-reu 3113 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-ov 7138 df-oprab 7139 df-mpo 7140 df-rest 16688 |
This theorem is referenced by: firest 16698 restbas 21763 tgrest 21764 resttopon 21766 restcld 21777 restfpw 21784 neitr 21785 restntr 21787 ordtrest 21807 cnrest 21890 lmss 21903 connsubclo 22029 restnlly 22087 islly2 22089 cldllycmp 22100 lly1stc 22101 kgenss 22148 xkococnlem 22264 xkoinjcn 22292 qtoprest 22322 trfbas2 22448 trfil1 22491 trfil2 22492 fgtr 22495 trfg 22496 uzrest 22502 trufil 22515 flimrest 22588 cnextcn 22672 trust 22835 restutop 22843 trcfilu 22900 cfiluweak 22901 xrsmopn 23417 zdis 23421 xrge0tsms 23439 cnheibor 23560 cfilres 23900 lhop2 24618 psercn 25021 xrlimcnp 25554 xrge0tsmsd 30742 ordtrestNEW 31274 pnfneige0 31304 lmxrge0 31305 rrhre 31372 cvmscld 32633 cvmopnlem 32638 cvmliftmolem1 32641 poimirlem30 35087 subspopn 35190 iocopn 42157 icoopn 42162 limcresiooub 42284 limcresioolb 42285 fourierdlem32 42781 fourierdlem33 42782 fourierdlem48 42796 fourierdlem49 42797 |
Copyright terms: Public domain | W3C validator |