# 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
`|- ( ( J e. Top /\ A e. J ) -> ( B e. ( J |`t A ) <-> ( B e. J /\ B C_ A ) ) )`

### Proof

Step Hyp Ref Expression
1 elssuni
` |-  ( B e. ( J |`t A ) -> B C_ U. ( J |`t A ) )`
2 elssuni
` |-  ( A e. J -> A C_ U. J )`
3 eqid
` |-  U. J = U. J`
4 3 restuni
` |-  ( ( J e. Top /\ A C_ U. J ) -> A = U. ( J |`t A ) )`
5 2 4 sylan2
` |-  ( ( J e. Top /\ A e. J ) -> A = U. ( J |`t A ) )`
6 5 sseq2d
` |-  ( ( J e. Top /\ A e. J ) -> ( B C_ A <-> B C_ U. ( J |`t A ) ) )`
7 1 6 syl5ibr
` |-  ( ( J e. Top /\ A e. J ) -> ( B e. ( J |`t A ) -> B C_ A ) )`
8 7 pm4.71rd
` |-  ( ( J e. Top /\ A e. J ) -> ( B e. ( J |`t A ) <-> ( B C_ A /\ B e. ( J |`t A ) ) ) )`
9 simpll
` |-  ( ( ( J e. Top /\ A e. J ) /\ B C_ A ) -> J e. Top )`
10 simplr
` |-  ( ( ( J e. Top /\ A e. J ) /\ B C_ A ) -> A e. J )`
11 ssidd
` |-  ( ( ( J e. Top /\ A e. J ) /\ B C_ A ) -> A C_ A )`
12 simpr
` |-  ( ( ( J e. Top /\ A e. J ) /\ B C_ A ) -> B C_ A )`
13 restopnb
` |-  ( ( ( J e. Top /\ A e. J ) /\ ( A e. J /\ A C_ A /\ B C_ A ) ) -> ( B e. J <-> B e. ( J |`t A ) ) )`
14 9 10 10 11 12 13 syl23anc
` |-  ( ( ( J e. Top /\ A e. J ) /\ B C_ A ) -> ( B e. J <-> B e. ( J |`t A ) ) )`
15 14 pm5.32da
` |-  ( ( J e. Top /\ A e. J ) -> ( ( B C_ A /\ B e. J ) <-> ( B C_ A /\ B e. ( J |`t A ) ) ) )`
16 8 15 bitr4d
` |-  ( ( J e. Top /\ A e. J ) -> ( B e. ( J |`t A ) <-> ( B C_ A /\ B e. J ) ) )`
17 16 biancomd
` |-  ( ( J e. Top /\ A e. J ) -> ( B e. ( J |`t A ) <-> ( B e. J /\ B C_ A ) ) )`