elrest

Description: The predicate "is an open set of a subspace topology". (Contributed by FL, 5-Jan-2009) (Revised by Mario Carneiro, 15-Dec-2013)

		Ref	Expression
	Assertion	elrest	$⊢ (J \in V \land B \in W) \to (A \in (J ↾_{𝑡} B) \leftrightarrow \exists x \in J A = x \cap B)$

Step	Hyp	Ref	Expression
1		restval	$⊢ (J \in V \land B \in W) \to J ↾_{𝑡} B = ran (x \in J ⟼ x \cap B)$
2	1	eleq2d	$⊢ (J \in V \land B \in W) \to (A \in (J ↾_{𝑡} B) \leftrightarrow A \in ran (x \in J ⟼ x \cap B))$
3		eqid	$⊢ (x \in J ⟼ x \cap B) = (x \in J ⟼ x \cap B)$
4		vex	$⊢ x \in V$
5	4	inex1	$⊢ x \cap B \in V$
6	3 5	elrnmpti	$⊢ A \in ran (x \in J ⟼ x \cap B) \leftrightarrow \exists x \in J A = x \cap B$
7	2 6	bitrdi	$⊢ (J \in V \land B \in W) \to (A \in (J ↾_{𝑡} B) \leftrightarrow \exists x \in J A = x \cap B)$

Metamath Proof Explorer