Metamath Proof Explorer

Theorem elrestr

Description: Sufficient condition for being an open set in a subspace. (Contributed by Jeff Hankins, 11-Jul-2009) (Revised by Mario Carneiro, 15-Dec-2013)

		Ref	Expression
	Assertion	elrestr	$⊢ (J \in V \land S \in W \land A \in J) \to A \cap S \in (J ↾_{𝑡} S)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ A \cap S = A \cap S$
2		ineq1	$⊢ x = A \to x \cap S = A \cap S$
3	2	rspceeqv	$⊢ (A \in J \land A \cap S = A \cap S) \to \exists x \in J A \cap S = x \cap S$
4	1 3	mpan2	$⊢ A \in J \to \exists x \in J A \cap S = x \cap S$
5		elrest	$⊢ (J \in V \land S \in W) \to (A \cap S \in (J ↾_{𝑡} S) \leftrightarrow \exists x \in J A \cap S = x \cap S)$
6	4 5	syl5ibr	$⊢ (J \in V \land S \in W) \to (A \in J \to A \cap S \in (J ↾_{𝑡} S))$
7	6	3impia	$⊢ (J \in V \land S \in W \land A \in J) \to A \cap S \in (J ↾_{𝑡} S)$