Metamath Proof Explorer

Theorem restin

Description: When the subspace region is not a subset of the base of the topology, the resulting set is the same as the subspace restricted to the base. (Contributed by Mario Carneiro, 15-Dec-2013)

		Ref	Expression
	Hypothesis	restin.1	$⊢ X = ⋃ J$
	Assertion	restin	$⊢ (J \in V \land A \in W) \to J ↾_{𝑡} A = J ↾_{𝑡} (A \cap X)$

Proof

Step	Hyp	Ref	Expression
1		restin.1	$⊢ X = ⋃ J$
2		uniexg	$⊢ J \in V \to ⋃ J \in V$
3	1 2	eqeltrid	$⊢ J \in V \to X \in V$
4	3	adantr	$⊢ (J \in V \land A \in W) \to X \in V$
5		restco	$⊢ (J \in V \land X \in V \land A \in W) \to (J ↾_{𝑡} X) ↾_{𝑡} A = J ↾_{𝑡} (X \cap A)$
6	5	3com23	$⊢ (J \in V \land A \in W \land X \in V) \to (J ↾_{𝑡} X) ↾_{𝑡} A = J ↾_{𝑡} (X \cap A)$
7	4 6	mpd3an3	$⊢ (J \in V \land A \in W) \to (J ↾_{𝑡} X) ↾_{𝑡} A = J ↾_{𝑡} (X \cap A)$
8	1	restid	$⊢ J \in V \to J ↾_{𝑡} X = J$
9	8	adantr	$⊢ (J \in V \land A \in W) \to J ↾_{𝑡} X = J$
10	9	oveq1d	$⊢ (J \in V \land A \in W) \to (J ↾_{𝑡} X) ↾_{𝑡} A = J ↾_{𝑡} A$
11		incom	$⊢ X \cap A = A \cap X$
12	11	oveq2i	$⊢ J ↾_{𝑡} (X \cap A) = J ↾_{𝑡} (A \cap X)$
13	12	a1i	$⊢ (J \in V \land A \in W) \to J ↾_{𝑡} (X \cap A) = J ↾_{𝑡} (A \cap X)$
14	7 10 13	3eqtr3d	$⊢ (J \in V \land A \in W) \to J ↾_{𝑡} A = J ↾_{𝑡} (A \cap X)$