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 ⊢J∈Top∧A∈V∧B∈J∧B⊆A∧C⊆B→C∈J↔C∈J↾𝑡A

Proof

Step Hyp Ref Expression
1 simpr3 ⊢J∈Top∧A∈V∧B∈J∧B⊆A∧C⊆B→C⊆B
2 simpr2 ⊢J∈Top∧A∈V∧B∈J∧B⊆A∧C⊆B→B⊆A
3 1 2 sstrd ⊢J∈Top∧A∈V∧B∈J∧B⊆A∧C⊆B→C⊆A
4 df-ss ⊢C⊆A↔C∩A=C
5 3 4 sylib ⊢J∈Top∧A∈V∧B∈J∧B⊆A∧C⊆B→C∩A=C
6 5 eqcomd ⊢J∈Top∧A∈V∧B∈J∧B⊆A∧C⊆B→C=C∩A
7 ineq1 ⊢v=C→v∩A=C∩A
8 7 rspceeqv ⊢C∈J∧C=C∩A→∃v∈JC=v∩A
9 8 expcom ⊢C=C∩A→C∈J→∃v∈JC=v∩A
10 6 9 syl ⊢J∈Top∧A∈V∧B∈J∧B⊆A∧C⊆B→C∈J→∃v∈JC=v∩A
11 inass ⊢v∩A∩B=v∩A∩B
12 simprr ⊢J∈Top∧A∈V∧B∈J∧B⊆A∧C⊆B∧v∈J∧C=v∩A→C=v∩A
13 12 ineq1d ⊢J∈Top∧A∈V∧B∈J∧B⊆A∧C⊆B∧v∈J∧C=v∩A→C∩B=v∩A∩B
14 simplr3 ⊢J∈Top∧A∈V∧B∈J∧B⊆A∧C⊆B∧v∈J→C⊆B
15 df-ss ⊢C⊆B↔C∩B=C
16 14 15 sylib ⊢J∈Top∧A∈V∧B∈J∧B⊆A∧C⊆B∧v∈J→C∩B=C
17 16 adantrr ⊢J∈Top∧A∈V∧B∈J∧B⊆A∧C⊆B∧v∈J∧C=v∩A→C∩B=C
18 13 17 eqtr3d ⊢J∈Top∧A∈V∧B∈J∧B⊆A∧C⊆B∧v∈J∧C=v∩A→v∩A∩B=C
19 simplr2 ⊢J∈Top∧A∈V∧B∈J∧B⊆A∧C⊆B∧v∈J→B⊆A
20 sseqin2 ⊢B⊆A↔A∩B=B
21 19 20 sylib ⊢J∈Top∧A∈V∧B∈J∧B⊆A∧C⊆B∧v∈J→A∩B=B
22 21 ineq2d ⊢J∈Top∧A∈V∧B∈J∧B⊆A∧C⊆B∧v∈J→v∩A∩B=v∩B
23 22 adantrr ⊢J∈Top∧A∈V∧B∈J∧B⊆A∧C⊆B∧v∈J∧C=v∩A→v∩A∩B=v∩B
24 11 18 23 3eqtr3a ⊢J∈Top∧A∈V∧B∈J∧B⊆A∧C⊆B∧v∈J∧C=v∩A→C=v∩B
25 simplll ⊢J∈Top∧A∈V∧B∈J∧B⊆A∧C⊆B∧v∈J∧C=v∩A→J∈Top
26 simprl ⊢J∈Top∧A∈V∧B∈J∧B⊆A∧C⊆B∧v∈J∧C=v∩A→v∈J
27 simplr1 ⊢J∈Top∧A∈V∧B∈J∧B⊆A∧C⊆B∧v∈J∧C=v∩A→B∈J
28 inopn ⊢J∈Top∧v∈J∧B∈J→v∩B∈J
29 25 26 27 28 syl3anc ⊢J∈Top∧A∈V∧B∈J∧B⊆A∧C⊆B∧v∈J∧C=v∩A→v∩B∈J
30 24 29 eqeltrd ⊢J∈Top∧A∈V∧B∈J∧B⊆A∧C⊆B∧v∈J∧C=v∩A→C∈J
31 30 rexlimdvaa ⊢J∈Top∧A∈V∧B∈J∧B⊆A∧C⊆B→∃v∈JC=v∩A→C∈J
32 10 31 impbid ⊢J∈Top∧A∈V∧B∈J∧B⊆A∧C⊆B→C∈J↔∃v∈JC=v∩A
33 elrest ⊢J∈Top∧A∈V→C∈J↾𝑡A↔∃v∈JC=v∩A
34 33 adantr ⊢J∈Top∧A∈V∧B∈J∧B⊆A∧C⊆B→C∈J↾𝑡A↔∃v∈JC=v∩A
35 32 34 bitr4d ⊢J∈Top∧A∈V∧B∈J∧B⊆A∧C⊆B→C∈J↔C∈J↾𝑡A