This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrrid 
 |-  ( ( 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 ) ) )