# Metamath Proof Explorer

## Theorem restopn2

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

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

### Proof

Step Hyp Ref Expression
1 elssuni ${⊢}{B}\in \left({J}{↾}_{𝑡}{A}\right)\to {B}\subseteq \bigcup \left({J}{↾}_{𝑡}{A}\right)$
2 elssuni ${⊢}{A}\in {J}\to {A}\subseteq \bigcup {J}$
3 eqid ${⊢}\bigcup {J}=\bigcup {J}$
4 3 restuni ${⊢}\left({J}\in \mathrm{Top}\wedge {A}\subseteq \bigcup {J}\right)\to {A}=\bigcup \left({J}{↾}_{𝑡}{A}\right)$
5 2 4 sylan2 ${⊢}\left({J}\in \mathrm{Top}\wedge {A}\in {J}\right)\to {A}=\bigcup \left({J}{↾}_{𝑡}{A}\right)$
6 5 sseq2d ${⊢}\left({J}\in \mathrm{Top}\wedge {A}\in {J}\right)\to \left({B}\subseteq {A}↔{B}\subseteq \bigcup \left({J}{↾}_{𝑡}{A}\right)\right)$
7 1 6 syl5ibr ${⊢}\left({J}\in \mathrm{Top}\wedge {A}\in {J}\right)\to \left({B}\in \left({J}{↾}_{𝑡}{A}\right)\to {B}\subseteq {A}\right)$
8 7 pm4.71rd ${⊢}\left({J}\in \mathrm{Top}\wedge {A}\in {J}\right)\to \left({B}\in \left({J}{↾}_{𝑡}{A}\right)↔\left({B}\subseteq {A}\wedge {B}\in \left({J}{↾}_{𝑡}{A}\right)\right)\right)$
9 simpll ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {A}\in {J}\right)\wedge {B}\subseteq {A}\right)\to {J}\in \mathrm{Top}$
10 simplr ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {A}\in {J}\right)\wedge {B}\subseteq {A}\right)\to {A}\in {J}$
11 ssidd ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {A}\in {J}\right)\wedge {B}\subseteq {A}\right)\to {A}\subseteq {A}$
12 simpr ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {A}\in {J}\right)\wedge {B}\subseteq {A}\right)\to {B}\subseteq {A}$
13 restopnb ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {A}\in {J}\right)\wedge \left({A}\in {J}\wedge {A}\subseteq {A}\wedge {B}\subseteq {A}\right)\right)\to \left({B}\in {J}↔{B}\in \left({J}{↾}_{𝑡}{A}\right)\right)$
14 9 10 10 11 12 13 syl23anc ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {A}\in {J}\right)\wedge {B}\subseteq {A}\right)\to \left({B}\in {J}↔{B}\in \left({J}{↾}_{𝑡}{A}\right)\right)$
15 14 pm5.32da ${⊢}\left({J}\in \mathrm{Top}\wedge {A}\in {J}\right)\to \left(\left({B}\subseteq {A}\wedge {B}\in {J}\right)↔\left({B}\subseteq {A}\wedge {B}\in \left({J}{↾}_{𝑡}{A}\right)\right)\right)$
16 8 15 bitr4d ${⊢}\left({J}\in \mathrm{Top}\wedge {A}\in {J}\right)\to \left({B}\in \left({J}{↾}_{𝑡}{A}\right)↔\left({B}\subseteq {A}\wedge {B}\in {J}\right)\right)$
17 16 biancomd ${⊢}\left({J}\in \mathrm{Top}\wedge {A}\in {J}\right)\to \left({B}\in \left({J}{↾}_{𝑡}{A}\right)↔\left({B}\in {J}\wedge {B}\subseteq {A}\right)\right)$