restcld

Description: A closed set of a subspace topology is a closed set of the original topology intersected with the subset. (Contributed by FL, 11-Jul-2009) (Proof shortened by Mario Carneiro, 15-Dec-2013)

		Ref	Expression
	Hypothesis	restcld.1	$⊢ X = ⋃ J$
	Assertion	restcld	$⊢ (J \in Top \land S \subseteq X) \to (A \in Clsd (J ↾_{𝑡} S) \leftrightarrow \exists x \in Clsd (J) A = x \cap S)$

Proof

Step	Hyp	Ref	Expression
1		restcld.1	$⊢ X = ⋃ J$
2		id	$⊢ S \subseteq X \to S \subseteq X$
3	1	topopn	$⊢ J \in Top \to X \in J$
4		ssexg	$⊢ (S \subseteq X \land X \in J) \to S \in V$
5	2 3 4	syl2anr	$⊢ (J \in Top \land S \subseteq X) \to S \in V$
6		resttop	$⊢ (J \in Top \land S \in V) \to J ↾_{𝑡} S \in Top$
7	5 6	syldan	$⊢ (J \in Top \land S \subseteq X) \to J ↾_{𝑡} S \in Top$
8		eqid	$⊢ ⋃ (J ↾_{𝑡} S) = ⋃ (J ↾_{𝑡} S)$
9	8	iscld	$⊢ J ↾_{𝑡} S \in Top \to (A \in Clsd (J ↾_{𝑡} S) \leftrightarrow (A \subseteq ⋃ (J ↾_{𝑡} S) \land ⋃ (J ↾_{𝑡} S) ∖ A \in (J ↾_{𝑡} S)))$
10	7 9	syl	$⊢ (J \in Top \land S \subseteq X) \to (A \in Clsd (J ↾_{𝑡} S) \leftrightarrow (A \subseteq ⋃ (J ↾_{𝑡} S) \land ⋃ (J ↾_{𝑡} S) ∖ A \in (J ↾_{𝑡} S)))$
11	1	restuni	$⊢ (J \in Top \land S \subseteq X) \to S = ⋃ (J ↾_{𝑡} S)$
12	11	sseq2d	$⊢ (J \in Top \land S \subseteq X) \to (A \subseteq S \leftrightarrow A \subseteq ⋃ (J ↾_{𝑡} S))$
13	11	difeq1d	$⊢ (J \in Top \land S \subseteq X) \to S ∖ A = ⋃ (J ↾_{𝑡} S) ∖ A$
14	13	eleq1d	$⊢ (J \in Top \land S \subseteq X) \to (S ∖ A \in (J ↾_{𝑡} S) \leftrightarrow ⋃ (J ↾_{𝑡} S) ∖ A \in (J ↾_{𝑡} S))$
15	12 14	anbi12d	$⊢ (J \in Top \land S \subseteq X) \to ((A \subseteq S \land S ∖ A \in (J ↾_{𝑡} S)) \leftrightarrow (A \subseteq ⋃ (J ↾_{𝑡} S) \land ⋃ (J ↾_{𝑡} S) ∖ A \in (J ↾_{𝑡} S)))$
16		elrest	$⊢ (J \in Top \land S \in V) \to (S ∖ A \in (J ↾_{𝑡} S) \leftrightarrow \exists o \in J S ∖ A = o \cap S)$
17	5 16	syldan	$⊢ (J \in Top \land S \subseteq X) \to (S ∖ A \in (J ↾_{𝑡} S) \leftrightarrow \exists o \in J S ∖ A = o \cap S)$
18	17	anbi2d	$⊢ (J \in Top \land S \subseteq X) \to ((A \subseteq S \land S ∖ A \in (J ↾_{𝑡} S)) \leftrightarrow (A \subseteq S \land \exists o \in J S ∖ A = o \cap S))$
19	1	opncld	$⊢ (J \in Top \land o \in J) \to X ∖ o \in Clsd (J)$
20	19	ad5ant14	$⊢ ((((J \in Top \land S \subseteq X) \land A \subseteq S) \land o \in J) \land S ∖ A = o \cap S) \to X ∖ o \in Clsd (J)$
21		incom	$⊢ X \cap S = S \cap X$
22		df-ss	$⊢ S \subseteq X \leftrightarrow S \cap X = S$
23	22	biimpi	$⊢ S \subseteq X \to S \cap X = S$
24	21 23	syl5eq	$⊢ S \subseteq X \to X \cap S = S$
25	24	ad4antlr	$⊢ ((((J \in Top \land S \subseteq X) \land A \subseteq S) \land o \in J) \land S ∖ A = o \cap S) \to X \cap S = S$
26	25	difeq1d	$⊢ ((((J \in Top \land S \subseteq X) \land A \subseteq S) \land o \in J) \land S ∖ A = o \cap S) \to (X \cap S) ∖ o = S ∖ o$
27		difeq2	$⊢ S ∖ A = o \cap S \to S ∖ (S ∖ A) = S ∖ (o \cap S)$
28		difindi	$⊢ S ∖ (o \cap S) = (S ∖ o) \cup (S ∖ S)$
29		difid	$⊢ S ∖ S = \emptyset$
30	29	uneq2i	$⊢ (S ∖ o) \cup (S ∖ S) = (S ∖ o) \cup \emptyset$
31		un0	$⊢ (S ∖ o) \cup \emptyset = S ∖ o$
32	28 30 31	3eqtri	$⊢ S ∖ (o \cap S) = S ∖ o$
33	27 32	syl6eq	$⊢ S ∖ A = o \cap S \to S ∖ (S ∖ A) = S ∖ o$
34	33	adantl	$⊢ ((((J \in Top \land S \subseteq X) \land A \subseteq S) \land o \in J) \land S ∖ A = o \cap S) \to S ∖ (S ∖ A) = S ∖ o$
35		dfss4	$⊢ A \subseteq S \leftrightarrow S ∖ (S ∖ A) = A$
36	35	biimpi	$⊢ A \subseteq S \to S ∖ (S ∖ A) = A$
37	36	ad3antlr	$⊢ ((((J \in Top \land S \subseteq X) \land A \subseteq S) \land o \in J) \land S ∖ A = o \cap S) \to S ∖ (S ∖ A) = A$
38	26 34 37	3eqtr2rd	$⊢ ((((J \in Top \land S \subseteq X) \land A \subseteq S) \land o \in J) \land S ∖ A = o \cap S) \to A = (X \cap S) ∖ o$
39	21	difeq1i	$⊢ (X \cap S) ∖ o = (S \cap X) ∖ o$
40		indif2	$⊢ S \cap (X ∖ o) = (S \cap X) ∖ o$
41		incom	$⊢ S \cap (X ∖ o) = (X ∖ o) \cap S$
42	39 40 41	3eqtr2i	$⊢ (X \cap S) ∖ o = (X ∖ o) \cap S$
43	38 42	syl6eq	$⊢ ((((J \in Top \land S \subseteq X) \land A \subseteq S) \land o \in J) \land S ∖ A = o \cap S) \to A = (X ∖ o) \cap S$
44		ineq1	$⊢ x = X ∖ o \to x \cap S = (X ∖ o) \cap S$
45	44	rspceeqv	$⊢ (X ∖ o \in Clsd (J) \land A = (X ∖ o) \cap S) \to \exists x \in Clsd (J) A = x \cap S$
46	20 43 45	syl2anc	$⊢ ((((J \in Top \land S \subseteq X) \land A \subseteq S) \land o \in J) \land S ∖ A = o \cap S) \to \exists x \in Clsd (J) A = x \cap S$
47	46	rexlimdva2	$⊢ ((J \in Top \land S \subseteq X) \land A \subseteq S) \to (\exists o \in J S ∖ A = o \cap S \to \exists x \in Clsd (J) A = x \cap S)$
48	47	expimpd	$⊢ (J \in Top \land S \subseteq X) \to ((A \subseteq S \land \exists o \in J S ∖ A = o \cap S) \to \exists x \in Clsd (J) A = x \cap S)$
49	18 48	sylbid	$⊢ (J \in Top \land S \subseteq X) \to ((A \subseteq S \land S ∖ A \in (J ↾_{𝑡} S)) \to \exists x \in Clsd (J) A = x \cap S)$
50		difindi	$⊢ S ∖ (x \cap S) = (S ∖ x) \cup (S ∖ S)$
51	29	uneq2i	$⊢ (S ∖ x) \cup (S ∖ S) = (S ∖ x) \cup \emptyset$
52		un0	$⊢ (S ∖ x) \cup \emptyset = S ∖ x$
53	50 51 52	3eqtri	$⊢ S ∖ (x \cap S) = S ∖ x$
54		difin2	$⊢ S \subseteq X \to S ∖ x = (X ∖ x) \cap S$
55	54	adantl	$⊢ (J \in Top \land S \subseteq X) \to S ∖ x = (X ∖ x) \cap S$
56	53 55	syl5eq	$⊢ (J \in Top \land S \subseteq X) \to S ∖ (x \cap S) = (X ∖ x) \cap S$
57	56	adantr	$⊢ ((J \in Top \land S \subseteq X) \land x \in Clsd (J)) \to S ∖ (x \cap S) = (X ∖ x) \cap S$
58		simpll	$⊢ ((J \in Top \land S \subseteq X) \land x \in Clsd (J)) \to J \in Top$
59	5	adantr	$⊢ ((J \in Top \land S \subseteq X) \land x \in Clsd (J)) \to S \in V$
60	1	cldopn	$⊢ x \in Clsd (J) \to X ∖ x \in J$
61	60	adantl	$⊢ ((J \in Top \land S \subseteq X) \land x \in Clsd (J)) \to X ∖ x \in J$
62		elrestr	$⊢ (J \in Top \land S \in V \land X ∖ x \in J) \to (X ∖ x) \cap S \in (J ↾_{𝑡} S)$
63	58 59 61 62	syl3anc	$⊢ ((J \in Top \land S \subseteq X) \land x \in Clsd (J)) \to (X ∖ x) \cap S \in (J ↾_{𝑡} S)$
64	57 63	eqeltrd	$⊢ ((J \in Top \land S \subseteq X) \land x \in Clsd (J)) \to S ∖ (x \cap S) \in (J ↾_{𝑡} S)$
65		inss2	$⊢ x \cap S \subseteq S$
66	64 65	jctil	$⊢ ((J \in Top \land S \subseteq X) \land x \in Clsd (J)) \to (x \cap S \subseteq S \land S ∖ (x \cap S) \in (J ↾_{𝑡} S))$
67		sseq1	$⊢ A = x \cap S \to (A \subseteq S \leftrightarrow x \cap S \subseteq S)$
68		difeq2	$⊢ A = x \cap S \to S ∖ A = S ∖ (x \cap S)$
69	68	eleq1d	$⊢ A = x \cap S \to (S ∖ A \in (J ↾_{𝑡} S) \leftrightarrow S ∖ (x \cap S) \in (J ↾_{𝑡} S))$
70	67 69	anbi12d	$⊢ A = x \cap S \to ((A \subseteq S \land S ∖ A \in (J ↾_{𝑡} S)) \leftrightarrow (x \cap S \subseteq S \land S ∖ (x \cap S) \in (J ↾_{𝑡} S)))$
71	66 70	syl5ibrcom	$⊢ ((J \in Top \land S \subseteq X) \land x \in Clsd (J)) \to (A = x \cap S \to (A \subseteq S \land S ∖ A \in (J ↾_{𝑡} S)))$
72	71	rexlimdva	$⊢ (J \in Top \land S \subseteq X) \to (\exists x \in Clsd (J) A = x \cap S \to (A \subseteq S \land S ∖ A \in (J ↾_{𝑡} S)))$
73	49 72	impbid	$⊢ (J \in Top \land S \subseteq X) \to ((A \subseteq S \land S ∖ A \in (J ↾_{𝑡} S)) \leftrightarrow \exists x \in Clsd (J) A = x \cap S)$
74	10 15 73	3bitr2d	$⊢ (J \in Top \land S \subseteq X) \to (A \in Clsd (J ↾_{𝑡} S) \leftrightarrow \exists x \in Clsd (J) A = x \cap S)$

Metamath Proof Explorer

Theorem restcld

Proof