Metamath Proof Explorer

Theorem restval

Description: The subspace topology induced by the topology J on the set A . (Contributed by FL, 20-Sep-2010) (Revised by Mario Carneiro, 1-May-2015)

		Ref	Expression
	Assertion	restval	$⊢ (J \in V \land A \in W) \to J ↾_{𝑡} A = ran (x \in J ⟼ x \cap A)$

Proof

Step	Hyp	Ref	Expression
1		elex	$⊢ J \in V \to J \in V$
2		elex	$⊢ A \in W \to A \in V$
3		mptexg	$⊢ J \in V \to (x \in J ⟼ x \cap A) \in V$
4		rnexg	$⊢ (x \in J ⟼ x \cap A) \in V \to ran (x \in J ⟼ x \cap A) \in V$
5	3 4	syl	$⊢ J \in V \to ran (x \in J ⟼ x \cap A) \in V$
6	5	adantr	$⊢ (J \in V \land A \in V) \to ran (x \in J ⟼ x \cap A) \in V$
7		simpl	$⊢ (j = J \land y = A) \to j = J$
8		simpr	$⊢ (j = J \land y = A) \to y = A$
9	8	ineq2d	$⊢ (j = J \land y = A) \to x \cap y = x \cap A$
10	7 9	mpteq12dv	$⊢ (j = J \land y = A) \to (x \in j ⟼ x \cap y) = (x \in J ⟼ x \cap A)$
11	10	rneqd	$⊢ (j = J \land y = A) \to ran (x \in j ⟼ x \cap y) = ran (x \in J ⟼ x \cap A)$
12		df-rest	$⊢ ↾_{𝑡} = (j \in V, y \in V ⟼ ran (x \in j ⟼ x \cap y))$
13	11 12	ovmpoga	$⊢ (J \in V \land A \in V \land ran (x \in J ⟼ x \cap A) \in V) \to J ↾_{𝑡} A = ran (x \in J ⟼ x \cap A)$
14	6 13	mpd3an3	$⊢ (J \in V \land A \in V) \to J ↾_{𝑡} A = ran (x \in J ⟼ x \cap A)$
15	1 2 14	syl2an	$⊢ (J \in V \land A \in W) \to J ↾_{𝑡} A = ran (x \in J ⟼ x \cap A)$