Theorem subspopn

Description: An open set is open in the subspace topology. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 15-Dec-2013)

	Ref	Expression
Assertion	subspopn	|- ( ( ( J e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A ) ) -> B e. ( J |`t A ) )

Proof

Step	Hyp	Ref	Expression
1		elrestr	|- ( ( J e. Top /\ A e. V /\ B e. J ) -> ( B i^i A ) e. ( J |`t A ) )
2		df-ss	|- ( B C_ A <-> ( B i^i A ) = B )
3		eleq1	|- ( ( B i^i A ) = B -> ( ( B i^i A ) e. ( J |`t A ) <-> B e. ( J |`t A ) ) )
4	2 3	sylbi	|- ( B C_ A -> ( ( B i^i A ) e. ( J |`t A ) <-> B e. ( J |`t A ) ) )
5	1 4	syl5ibcom	|- ( ( J e. Top /\ A e. V /\ B e. J ) -> ( B C_ A -> B e. ( J |`t A ) ) )
6	5	3expa	|- ( ( ( J e. Top /\ A e. V ) /\ B e. J ) -> ( B C_ A -> B e. ( J |`t A ) ) )
7	6	impr	|- ( ( ( J e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A ) ) -> B e. ( J |`t A ) )