resttopon2

Description: The underlying set of a subspace topology. (Contributed by Mario Carneiro, 13-Aug-2015)

		Ref	Expression
	Assertion	resttopon2	$⊢ (J \in TopOn (X) \land A \in V) \to J ↾_{𝑡} A \in TopOn (A \cap X)$

Step	Hyp	Ref	Expression
1		topontop	$⊢ J \in TopOn (X) \to J \in Top$
2		resttop	$⊢ (J \in Top \land A \in V) \to J ↾_{𝑡} A \in Top$
3	1 2	sylan	$⊢ (J \in TopOn (X) \land A \in V) \to J ↾_{𝑡} A \in Top$
4		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
5	4	ineq2d	$⊢ J \in TopOn (X) \to A \cap X = A \cap ⋃ J$
6	5	adantr	$⊢ (J \in TopOn (X) \land A \in V) \to A \cap X = A \cap ⋃ J$
7		eqid	$⊢ ⋃ J = ⋃ J$
8	7	restuni2	$⊢ (J \in Top \land A \in V) \to A \cap ⋃ J = ⋃ (J ↾_{𝑡} A)$
9	1 8	sylan	$⊢ (J \in TopOn (X) \land A \in V) \to A \cap ⋃ J = ⋃ (J ↾_{𝑡} A)$
10	6 9	eqtrd	$⊢ (J \in TopOn (X) \land A \in V) \to A \cap X = ⋃ (J ↾_{𝑡} A)$
11		istopon	$⊢ J ↾_{𝑡} A \in TopOn (A \cap X) \leftrightarrow (J ↾_{𝑡} A \in Top \land A \cap X = ⋃ (J ↾_{𝑡} A))$
12	3 10 11	sylanbrc	$⊢ (J \in TopOn (X) \land A \in V) \to J ↾_{𝑡} A \in TopOn (A \cap X)$

Metamath Proof Explorer