resttopon

Description: A subspace topology is a topology on the base set. (Contributed by Mario Carneiro, 13-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		topontop	$⊢ J \in TopOn (X) \to J \in Top$
2		id	$⊢ A \subseteq X \to A \subseteq X$
3		toponmax	$⊢ J \in TopOn (X) \to X \in J$
4		ssexg	$⊢ (A \subseteq X \land X \in J) \to A \in V$
5	2 3 4	syl2anr	$⊢ (J \in TopOn (X) \land A \subseteq X) \to A \in V$
6		resttop	$⊢ (J \in Top \land A \in V) \to J ↾_{𝑡} A \in Top$
7	1 5 6	syl2an2r	$⊢ (J \in TopOn (X) \land A \subseteq X) \to J ↾_{𝑡} A \in Top$
8		simpr	$⊢ (J \in TopOn (X) \land A \subseteq X) \to A \subseteq X$
9		sseqin2	$⊢ A \subseteq X \leftrightarrow X \cap A = A$
10	8 9	sylib	$⊢ (J \in TopOn (X) \land A \subseteq X) \to X \cap A = A$
11		simpl	$⊢ (J \in TopOn (X) \land A \subseteq X) \to J \in TopOn (X)$
12	3	adantr	$⊢ (J \in TopOn (X) \land A \subseteq X) \to X \in J$
13		elrestr	$⊢ (J \in TopOn (X) \land A \in V \land X \in J) \to X \cap A \in (J ↾_{𝑡} A)$
14	11 5 12 13	syl3anc	$⊢ (J \in TopOn (X) \land A \subseteq X) \to X \cap A \in (J ↾_{𝑡} A)$
15	10 14	eqeltrrd	$⊢ (J \in TopOn (X) \land A \subseteq X) \to A \in (J ↾_{𝑡} A)$
16		elssuni	$⊢ A \in (J ↾_{𝑡} A) \to A \subseteq ⋃ (J ↾_{𝑡} A)$
17	15 16	syl	$⊢ (J \in TopOn (X) \land A \subseteq X) \to A \subseteq ⋃ (J ↾_{𝑡} A)$
18		restval	$⊢ (J \in TopOn (X) \land A \in V) \to J ↾_{𝑡} A = ran (x \in J ⟼ x \cap A)$
19	5 18	syldan	$⊢ (J \in TopOn (X) \land A \subseteq X) \to J ↾_{𝑡} A = ran (x \in J ⟼ x \cap A)$
20		inss2	$⊢ x \cap A \subseteq A$
21		vex	$⊢ x \in V$
22	21	inex1	$⊢ x \cap A \in V$
23	22	elpw	$⊢ x \cap A \in 𝒫 A \leftrightarrow x \cap A \subseteq A$
24	20 23	mpbir	$⊢ x \cap A \in 𝒫 A$
25	24	a1i	$⊢ ((J \in TopOn (X) \land A \subseteq X) \land x \in J) \to x \cap A \in 𝒫 A$
26	25	fmpttd	$⊢ (J \in TopOn (X) \land A \subseteq X) \to (x \in J ⟼ x \cap A) : J ⟶ 𝒫 A$
27	26	frnd	$⊢ (J \in TopOn (X) \land A \subseteq X) \to ran (x \in J ⟼ x \cap A) \subseteq 𝒫 A$
28	19 27	eqsstrd	$⊢ (J \in TopOn (X) \land A \subseteq X) \to J ↾_{𝑡} A \subseteq 𝒫 A$
29		sspwuni	$⊢ J ↾_{𝑡} A \subseteq 𝒫 A \leftrightarrow ⋃ (J ↾_{𝑡} A) \subseteq A$
30	28 29	sylib	$⊢ (J \in TopOn (X) \land A \subseteq X) \to ⋃ (J ↾_{𝑡} A) \subseteq A$
31	17 30	eqssd	$⊢ (J \in TopOn (X) \land A \subseteq X) \to A = ⋃ (J ↾_{𝑡} A)$
32		istopon	$⊢ J ↾_{𝑡} A \in TopOn (A) \leftrightarrow (J ↾_{𝑡} A \in Top \land A = ⋃ (J ↾_{𝑡} A))$
33	7 31 32	sylanbrc	$⊢ (J \in TopOn (X) \land A \subseteq X) \to J ↾_{𝑡} A \in TopOn (A)$

Metamath Proof Explorer

Theorem resttopon

Proof