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 \in Top \land A \in V) \land (B \in J \land B \subseteq A)) \to B \in (J ↾_{𝑡} A)$

Step	Hyp	Ref	Expression
1		elrestr	$⊢ (J \in Top \land A \in V \land B \in J) \to B \cap A \in (J ↾_{𝑡} A)$
2		df-ss	$⊢ B \subseteq A \leftrightarrow B \cap A = B$
3		eleq1	$⊢ B \cap A = B \to (B \cap A \in (J ↾_{𝑡} A) \leftrightarrow B \in (J ↾_{𝑡} A))$
4	2 3	sylbi	$⊢ B \subseteq A \to (B \cap A \in (J ↾_{𝑡} A) \leftrightarrow B \in (J ↾_{𝑡} A))$
5	1 4	syl5ibcom	$⊢ (J \in Top \land A \in V \land B \in J) \to (B \subseteq A \to B \in (J ↾_{𝑡} A))$
6	5	3expa	$⊢ ((J \in Top \land A \in V) \land B \in J) \to (B \subseteq A \to B \in (J ↾_{𝑡} A))$
7	6	impr	$⊢ ((J \in Top \land A \in V) \land (B \in J \land B \subseteq A)) \to B \in (J ↾_{𝑡} A)$

Metamath Proof Explorer