restcls

Description: A closure in a subspace topology. (Contributed by Jeff Hankins, 22-Jan-2010) (Revised by Mario Carneiro, 15-Dec-2013)

	Ref	Expression
Hypotheses	restcls.1	$⊢ X = ⋃ J$
	restcls.2	$⊢ K = J ↾_{𝑡} Y$
Assertion	restcls	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to cls (K) (S) = cls (J) (S) \cap Y$

Proof

Step	Hyp	Ref	Expression
1		restcls.1	$⊢ X = ⋃ J$
2		restcls.2	$⊢ K = J ↾_{𝑡} Y$
3		simp1	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to J \in Top$
4		sstr	$⊢ (S \subseteq Y \land Y \subseteq X) \to S \subseteq X$
5	4	ancoms	$⊢ (Y \subseteq X \land S \subseteq Y) \to S \subseteq X$
6	5	3adant1	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to S \subseteq X$
7	1	clscld	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) \in Clsd (J)$
8	3 6 7	syl2anc	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to cls (J) (S) \in Clsd (J)$
9		eqid	$⊢ cls (J) (S) \cap Y = cls (J) (S) \cap Y$
10		ineq1	$⊢ x = cls (J) (S) \to x \cap Y = cls (J) (S) \cap Y$
11	10	rspceeqv	$⊢ (cls (J) (S) \in Clsd (J) \land cls (J) (S) \cap Y = cls (J) (S) \cap Y) \to \exists x \in Clsd (J) cls (J) (S) \cap Y = x \cap Y$
12	8 9 11	sylancl	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to \exists x \in Clsd (J) cls (J) (S) \cap Y = x \cap Y$
13	2	fveq2i	$⊢ Clsd (K) = Clsd (J ↾_{𝑡} Y)$
14	13	eleq2i	$⊢ cls (J) (S) \cap Y \in Clsd (K) \leftrightarrow cls (J) (S) \cap Y \in Clsd (J ↾_{𝑡} Y)$
15	1	restcld	$⊢ (J \in Top \land Y \subseteq X) \to (cls (J) (S) \cap Y \in Clsd (J ↾_{𝑡} Y) \leftrightarrow \exists x \in Clsd (J) cls (J) (S) \cap Y = x \cap Y)$
16	15	3adant3	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to (cls (J) (S) \cap Y \in Clsd (J ↾_{𝑡} Y) \leftrightarrow \exists x \in Clsd (J) cls (J) (S) \cap Y = x \cap Y)$
17	14 16	bitrid	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to (cls (J) (S) \cap Y \in Clsd (K) \leftrightarrow \exists x \in Clsd (J) cls (J) (S) \cap Y = x \cap Y)$
18	12 17	mpbird	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to cls (J) (S) \cap Y \in Clsd (K)$
19	1	sscls	$⊢ (J \in Top \land S \subseteq X) \to S \subseteq cls (J) (S)$
20	3 6 19	syl2anc	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to S \subseteq cls (J) (S)$
21		simp3	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to S \subseteq Y$
22	20 21	ssind	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to S \subseteq cls (J) (S) \cap Y$
23		eqid	$⊢ ⋃ K = ⋃ K$
24	23	clsss2	$⊢ (cls (J) (S) \cap Y \in Clsd (K) \land S \subseteq cls (J) (S) \cap Y) \to cls (K) (S) \subseteq cls (J) (S) \cap Y$
25	18 22 24	syl2anc	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to cls (K) (S) \subseteq cls (J) (S) \cap Y$
26	2	fveq2i	$⊢ cls (K) = cls (J ↾_{𝑡} Y)$
27	26	fveq1i	$⊢ cls (K) (S) = cls (J ↾_{𝑡} Y) (S)$
28		id	$⊢ Y \subseteq X \to Y \subseteq X$
29	1	topopn	$⊢ J \in Top \to X \in J$
30		ssexg	$⊢ (Y \subseteq X \land X \in J) \to Y \in V$
31	28 29 30	syl2anr	$⊢ (J \in Top \land Y \subseteq X) \to Y \in V$
32		resttop	$⊢ (J \in Top \land Y \in V) \to J ↾_{𝑡} Y \in Top$
33	31 32	syldan	$⊢ (J \in Top \land Y \subseteq X) \to J ↾_{𝑡} Y \in Top$
34	33	3adant3	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to J ↾_{𝑡} Y \in Top$
35	1	restuni	$⊢ (J \in Top \land Y \subseteq X) \to Y = ⋃ (J ↾_{𝑡} Y)$
36	35	3adant3	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to Y = ⋃ (J ↾_{𝑡} Y)$
37	21 36	sseqtrd	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to S \subseteq ⋃ (J ↾_{𝑡} Y)$
38		eqid	$⊢ ⋃ (J ↾_{𝑡} Y) = ⋃ (J ↾_{𝑡} Y)$
39	38	clscld	$⊢ (J ↾_{𝑡} Y \in Top \land S \subseteq ⋃ (J ↾_{𝑡} Y)) \to cls (J ↾_{𝑡} Y) (S) \in Clsd (J ↾_{𝑡} Y)$
40	34 37 39	syl2anc	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to cls (J ↾_{𝑡} Y) (S) \in Clsd (J ↾_{𝑡} Y)$
41	27 40	eqeltrid	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to cls (K) (S) \in Clsd (J ↾_{𝑡} Y)$
42	1	restcld	$⊢ (J \in Top \land Y \subseteq X) \to (cls (K) (S) \in Clsd (J ↾_{𝑡} Y) \leftrightarrow \exists x \in Clsd (J) cls (K) (S) = x \cap Y)$
43	42	3adant3	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to (cls (K) (S) \in Clsd (J ↾_{𝑡} Y) \leftrightarrow \exists x \in Clsd (J) cls (K) (S) = x \cap Y)$
44	41 43	mpbid	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to \exists x \in Clsd (J) cls (K) (S) = x \cap Y$
45	2 33	eqeltrid	$⊢ (J \in Top \land Y \subseteq X) \to K \in Top$
46	45	3adant3	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to K \in Top$
47	2	unieqi	$⊢ ⋃ K = ⋃ (J ↾_{𝑡} Y)$
48	47	eqcomi	$⊢ ⋃ (J ↾_{𝑡} Y) = ⋃ K$
49	48	sscls	$⊢ (K \in Top \land S \subseteq ⋃ (J ↾_{𝑡} Y)) \to S \subseteq cls (K) (S)$
50	46 37 49	syl2anc	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to S \subseteq cls (K) (S)$
51	50	adantr	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (x \in Clsd (J) \land cls (K) (S) = x \cap Y)) \to S \subseteq cls (K) (S)$
52		inss1	$⊢ x \cap Y \subseteq x$
53		sseq1	$⊢ cls (K) (S) = x \cap Y \to (cls (K) (S) \subseteq x \leftrightarrow x \cap Y \subseteq x)$
54	52 53	mpbiri	$⊢ cls (K) (S) = x \cap Y \to cls (K) (S) \subseteq x$
55	54	ad2antll	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (x \in Clsd (J) \land cls (K) (S) = x \cap Y)) \to cls (K) (S) \subseteq x$
56	51 55	sstrd	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (x \in Clsd (J) \land cls (K) (S) = x \cap Y)) \to S \subseteq x$
57	1	clsss2	$⊢ (x \in Clsd (J) \land S \subseteq x) \to cls (J) (S) \subseteq x$
58	57	adantl	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (x \in Clsd (J) \land S \subseteq x)) \to cls (J) (S) \subseteq x$
59	58	ssrind	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (x \in Clsd (J) \land S \subseteq x)) \to cls (J) (S) \cap Y \subseteq x \cap Y$
60		sseq2	$⊢ cls (K) (S) = x \cap Y \to (cls (J) (S) \cap Y \subseteq cls (K) (S) \leftrightarrow cls (J) (S) \cap Y \subseteq x \cap Y)$
61	59 60	syl5ibrcom	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (x \in Clsd (J) \land S \subseteq x)) \to (cls (K) (S) = x \cap Y \to cls (J) (S) \cap Y \subseteq cls (K) (S))$
62	61	expr	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land x \in Clsd (J)) \to (S \subseteq x \to (cls (K) (S) = x \cap Y \to cls (J) (S) \cap Y \subseteq cls (K) (S)))$
63	62	com23	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land x \in Clsd (J)) \to (cls (K) (S) = x \cap Y \to (S \subseteq x \to cls (J) (S) \cap Y \subseteq cls (K) (S)))$
64	63	impr	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (x \in Clsd (J) \land cls (K) (S) = x \cap Y)) \to (S \subseteq x \to cls (J) (S) \cap Y \subseteq cls (K) (S))$
65	56 64	mpd	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (x \in Clsd (J) \land cls (K) (S) = x \cap Y)) \to cls (J) (S) \cap Y \subseteq cls (K) (S)$
66	44 65	rexlimddv	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to cls (J) (S) \cap Y \subseteq cls (K) (S)$
67	25 66	eqssd	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to cls (K) (S) = cls (J) (S) \cap Y$

Metamath Proof Explorer

Theorem restcls

Proof