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