restid2

Description: The subspace topology over a subset of the base set is the original topology. (Contributed by Mario Carneiro, 13-Aug-2015)

		Ref	Expression
	Assertion	restid2	$⊢ (A \in V \land J \subseteq 𝒫 A) \to J ↾_{𝑡} A = J$

Step	Hyp	Ref	Expression
1		pwexg	$⊢ A \in V \to 𝒫 A \in V$
2	1	adantr	$⊢ (A \in V \land J \subseteq 𝒫 A) \to 𝒫 A \in V$
3		simpr	$⊢ (A \in V \land J \subseteq 𝒫 A) \to J \subseteq 𝒫 A$
4	2 3	ssexd	$⊢ (A \in V \land J \subseteq 𝒫 A) \to J \in V$
5		simpl	$⊢ (A \in V \land J \subseteq 𝒫 A) \to A \in V$
6		restval	$⊢ (J \in V \land A \in V) \to J ↾_{𝑡} A = ran (x \in J ⟼ x \cap A)$
7	4 5 6	syl2anc	$⊢ (A \in V \land J \subseteq 𝒫 A) \to J ↾_{𝑡} A = ran (x \in J ⟼ x \cap A)$
8	3	sselda	$⊢ ((A \in V \land J \subseteq 𝒫 A) \land x \in J) \to x \in 𝒫 A$
9	8	elpwid	$⊢ ((A \in V \land J \subseteq 𝒫 A) \land x \in J) \to x \subseteq A$
10		dfss2	$⊢ x \subseteq A \leftrightarrow x \cap A = x$
11	9 10	sylib	$⊢ ((A \in V \land J \subseteq 𝒫 A) \land x \in J) \to x \cap A = x$
12	11	mpteq2dva	$⊢ (A \in V \land J \subseteq 𝒫 A) \to (x \in J ⟼ x \cap A) = (x \in J ⟼ x)$
13		mptresid	$⊢ {I ↾}_{J} = (x \in J ⟼ x)$
14	12 13	eqtr4di	$⊢ (A \in V \land J \subseteq 𝒫 A) \to (x \in J ⟼ x \cap A) = {I ↾}_{J}$
15	14	rneqd	$⊢ (A \in V \land J \subseteq 𝒫 A) \to ran (x \in J ⟼ x \cap A) = ran ({I ↾}_{J})$
16		rnresi	$⊢ ran ({I ↾}_{J}) = J$
17	15 16	eqtrdi	$⊢ (A \in V \land J \subseteq 𝒫 A) \to ran (x \in J ⟼ x \cap A) = J$
18	7 17	eqtrd	$⊢ (A \in V \land J \subseteq 𝒫 A) \to J ↾_{𝑡} A = J$

Metamath Proof Explorer