# Metamath Proof Explorer

## Theorem restopnb

Description: If B is an open subset of the subspace base set A , then any subset of B is open iff it is open in A . (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Assertion restopnb ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {A}\in {V}\right)\wedge \left({B}\in {J}\wedge {B}\subseteq {A}\wedge {C}\subseteq {B}\right)\right)\to \left({C}\in {J}↔{C}\in \left({J}{↾}_{𝑡}{A}\right)\right)$

### Proof

Step Hyp Ref Expression
1 simpr3 ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {A}\in {V}\right)\wedge \left({B}\in {J}\wedge {B}\subseteq {A}\wedge {C}\subseteq {B}\right)\right)\to {C}\subseteq {B}$
2 simpr2 ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {A}\in {V}\right)\wedge \left({B}\in {J}\wedge {B}\subseteq {A}\wedge {C}\subseteq {B}\right)\right)\to {B}\subseteq {A}$
3 1 2 sstrd ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {A}\in {V}\right)\wedge \left({B}\in {J}\wedge {B}\subseteq {A}\wedge {C}\subseteq {B}\right)\right)\to {C}\subseteq {A}$
4 df-ss ${⊢}{C}\subseteq {A}↔{C}\cap {A}={C}$
5 3 4 sylib ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {A}\in {V}\right)\wedge \left({B}\in {J}\wedge {B}\subseteq {A}\wedge {C}\subseteq {B}\right)\right)\to {C}\cap {A}={C}$
6 5 eqcomd ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {A}\in {V}\right)\wedge \left({B}\in {J}\wedge {B}\subseteq {A}\wedge {C}\subseteq {B}\right)\right)\to {C}={C}\cap {A}$
7 ineq1 ${⊢}{v}={C}\to {v}\cap {A}={C}\cap {A}$
8 7 rspceeqv ${⊢}\left({C}\in {J}\wedge {C}={C}\cap {A}\right)\to \exists {v}\in {J}\phantom{\rule{.4em}{0ex}}{C}={v}\cap {A}$
9 8 expcom ${⊢}{C}={C}\cap {A}\to \left({C}\in {J}\to \exists {v}\in {J}\phantom{\rule{.4em}{0ex}}{C}={v}\cap {A}\right)$
10 6 9 syl ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {A}\in {V}\right)\wedge \left({B}\in {J}\wedge {B}\subseteq {A}\wedge {C}\subseteq {B}\right)\right)\to \left({C}\in {J}\to \exists {v}\in {J}\phantom{\rule{.4em}{0ex}}{C}={v}\cap {A}\right)$
11 inass ${⊢}\left({v}\cap {A}\right)\cap {B}={v}\cap \left({A}\cap {B}\right)$
12 simprr ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {A}\in {V}\right)\wedge \left({B}\in {J}\wedge {B}\subseteq {A}\wedge {C}\subseteq {B}\right)\right)\wedge \left({v}\in {J}\wedge {C}={v}\cap {A}\right)\right)\to {C}={v}\cap {A}$
13 12 ineq1d ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {A}\in {V}\right)\wedge \left({B}\in {J}\wedge {B}\subseteq {A}\wedge {C}\subseteq {B}\right)\right)\wedge \left({v}\in {J}\wedge {C}={v}\cap {A}\right)\right)\to {C}\cap {B}=\left({v}\cap {A}\right)\cap {B}$
14 simplr3 ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {A}\in {V}\right)\wedge \left({B}\in {J}\wedge {B}\subseteq {A}\wedge {C}\subseteq {B}\right)\right)\wedge {v}\in {J}\right)\to {C}\subseteq {B}$
15 df-ss ${⊢}{C}\subseteq {B}↔{C}\cap {B}={C}$
16 14 15 sylib ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {A}\in {V}\right)\wedge \left({B}\in {J}\wedge {B}\subseteq {A}\wedge {C}\subseteq {B}\right)\right)\wedge {v}\in {J}\right)\to {C}\cap {B}={C}$
17 16 adantrr ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {A}\in {V}\right)\wedge \left({B}\in {J}\wedge {B}\subseteq {A}\wedge {C}\subseteq {B}\right)\right)\wedge \left({v}\in {J}\wedge {C}={v}\cap {A}\right)\right)\to {C}\cap {B}={C}$
18 13 17 eqtr3d ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {A}\in {V}\right)\wedge \left({B}\in {J}\wedge {B}\subseteq {A}\wedge {C}\subseteq {B}\right)\right)\wedge \left({v}\in {J}\wedge {C}={v}\cap {A}\right)\right)\to \left({v}\cap {A}\right)\cap {B}={C}$
19 simplr2 ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {A}\in {V}\right)\wedge \left({B}\in {J}\wedge {B}\subseteq {A}\wedge {C}\subseteq {B}\right)\right)\wedge {v}\in {J}\right)\to {B}\subseteq {A}$
20 sseqin2 ${⊢}{B}\subseteq {A}↔{A}\cap {B}={B}$
21 19 20 sylib ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {A}\in {V}\right)\wedge \left({B}\in {J}\wedge {B}\subseteq {A}\wedge {C}\subseteq {B}\right)\right)\wedge {v}\in {J}\right)\to {A}\cap {B}={B}$
22 21 ineq2d ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {A}\in {V}\right)\wedge \left({B}\in {J}\wedge {B}\subseteq {A}\wedge {C}\subseteq {B}\right)\right)\wedge {v}\in {J}\right)\to {v}\cap \left({A}\cap {B}\right)={v}\cap {B}$
23 22 adantrr ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {A}\in {V}\right)\wedge \left({B}\in {J}\wedge {B}\subseteq {A}\wedge {C}\subseteq {B}\right)\right)\wedge \left({v}\in {J}\wedge {C}={v}\cap {A}\right)\right)\to {v}\cap \left({A}\cap {B}\right)={v}\cap {B}$
24 11 18 23 3eqtr3a ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {A}\in {V}\right)\wedge \left({B}\in {J}\wedge {B}\subseteq {A}\wedge {C}\subseteq {B}\right)\right)\wedge \left({v}\in {J}\wedge {C}={v}\cap {A}\right)\right)\to {C}={v}\cap {B}$
25 simplll ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {A}\in {V}\right)\wedge \left({B}\in {J}\wedge {B}\subseteq {A}\wedge {C}\subseteq {B}\right)\right)\wedge \left({v}\in {J}\wedge {C}={v}\cap {A}\right)\right)\to {J}\in \mathrm{Top}$
26 simprl ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {A}\in {V}\right)\wedge \left({B}\in {J}\wedge {B}\subseteq {A}\wedge {C}\subseteq {B}\right)\right)\wedge \left({v}\in {J}\wedge {C}={v}\cap {A}\right)\right)\to {v}\in {J}$
27 simplr1 ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {A}\in {V}\right)\wedge \left({B}\in {J}\wedge {B}\subseteq {A}\wedge {C}\subseteq {B}\right)\right)\wedge \left({v}\in {J}\wedge {C}={v}\cap {A}\right)\right)\to {B}\in {J}$
28 inopn ${⊢}\left({J}\in \mathrm{Top}\wedge {v}\in {J}\wedge {B}\in {J}\right)\to {v}\cap {B}\in {J}$
29 25 26 27 28 syl3anc ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {A}\in {V}\right)\wedge \left({B}\in {J}\wedge {B}\subseteq {A}\wedge {C}\subseteq {B}\right)\right)\wedge \left({v}\in {J}\wedge {C}={v}\cap {A}\right)\right)\to {v}\cap {B}\in {J}$
30 24 29 eqeltrd ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {A}\in {V}\right)\wedge \left({B}\in {J}\wedge {B}\subseteq {A}\wedge {C}\subseteq {B}\right)\right)\wedge \left({v}\in {J}\wedge {C}={v}\cap {A}\right)\right)\to {C}\in {J}$
31 30 rexlimdvaa ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {A}\in {V}\right)\wedge \left({B}\in {J}\wedge {B}\subseteq {A}\wedge {C}\subseteq {B}\right)\right)\to \left(\exists {v}\in {J}\phantom{\rule{.4em}{0ex}}{C}={v}\cap {A}\to {C}\in {J}\right)$
32 10 31 impbid ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {A}\in {V}\right)\wedge \left({B}\in {J}\wedge {B}\subseteq {A}\wedge {C}\subseteq {B}\right)\right)\to \left({C}\in {J}↔\exists {v}\in {J}\phantom{\rule{.4em}{0ex}}{C}={v}\cap {A}\right)$
33 elrest ${⊢}\left({J}\in \mathrm{Top}\wedge {A}\in {V}\right)\to \left({C}\in \left({J}{↾}_{𝑡}{A}\right)↔\exists {v}\in {J}\phantom{\rule{.4em}{0ex}}{C}={v}\cap {A}\right)$
34 33 adantr ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {A}\in {V}\right)\wedge \left({B}\in {J}\wedge {B}\subseteq {A}\wedge {C}\subseteq {B}\right)\right)\to \left({C}\in \left({J}{↾}_{𝑡}{A}\right)↔\exists {v}\in {J}\phantom{\rule{.4em}{0ex}}{C}={v}\cap {A}\right)$
35 32 34 bitr4d ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {A}\in {V}\right)\wedge \left({B}\in {J}\wedge {B}\subseteq {A}\wedge {C}\subseteq {B}\right)\right)\to \left({C}\in {J}↔{C}\in \left({J}{↾}_{𝑡}{A}\right)\right)$