restntr

Description: An interior in a subspace topology. Willard inGeneral Topology says that there is no analogue of restcls for interiors. In some sense, that is true. (Contributed by Jeff Hankins, 23-Jan-2010) (Revised by Mario Carneiro, 15-Dec-2013)

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

Proof

Step	Hyp	Ref	Expression
1		restcls.1	$⊢ X = ⋃ J$
2		restcls.2	$⊢ K = J ↾_{𝑡} Y$
3	2	fveq2i	$⊢ int (K) = int (J ↾_{𝑡} Y)$
4	3	fveq1i	$⊢ int (K) (S) = int (J ↾_{𝑡} Y) (S)$
5	1	topopn	$⊢ J \in Top \to X \in J$
6		ssexg	$⊢ (Y \subseteq X \land X \in J) \to Y \in V$
7	6	ancoms	$⊢ (X \in J \land Y \subseteq X) \to Y \in V$
8	5 7	sylan	$⊢ (J \in Top \land Y \subseteq X) \to Y \in V$
9		resttop	$⊢ (J \in Top \land Y \in V) \to J ↾_{𝑡} Y \in Top$
10	8 9	syldan	$⊢ (J \in Top \land Y \subseteq X) \to J ↾_{𝑡} Y \in Top$
11	10	3adant3	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to J ↾_{𝑡} Y \in Top$
12	1	restuni	$⊢ (J \in Top \land Y \subseteq X) \to Y = ⋃ (J ↾_{𝑡} Y)$
13	12	sseq2d	$⊢ (J \in Top \land Y \subseteq X) \to (S \subseteq Y \leftrightarrow S \subseteq ⋃ (J ↾_{𝑡} Y))$
14	13	biimp3a	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to S \subseteq ⋃ (J ↾_{𝑡} Y)$
15		eqid	$⊢ ⋃ (J ↾_{𝑡} Y) = ⋃ (J ↾_{𝑡} Y)$
16	15	ntropn	$⊢ (J ↾_{𝑡} Y \in Top \land S \subseteq ⋃ (J ↾_{𝑡} Y)) \to int (J ↾_{𝑡} Y) (S) \in (J ↾_{𝑡} Y)$
17	11 14 16	syl2anc	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to int (J ↾_{𝑡} Y) (S) \in (J ↾_{𝑡} Y)$
18	4 17	eqeltrid	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to int (K) (S) \in (J ↾_{𝑡} Y)$
19		simp1	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to J \in Top$
20		uniexg	$⊢ J \in Top \to ⋃ J \in V$
21	1 20	eqeltrid	$⊢ J \in Top \to X \in V$
22		ssexg	$⊢ (Y \subseteq X \land X \in V) \to Y \in V$
23	21 22	sylan2	$⊢ (Y \subseteq X \land J \in Top) \to Y \in V$
24	23	ancoms	$⊢ (J \in Top \land Y \subseteq X) \to Y \in V$
25	24	3adant3	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to Y \in V$
26		elrest	$⊢ (J \in Top \land Y \in V) \to (int (K) (S) \in (J ↾_{𝑡} Y) \leftrightarrow \exists o \in J int (K) (S) = o \cap Y)$
27	19 25 26	syl2anc	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to (int (K) (S) \in (J ↾_{𝑡} Y) \leftrightarrow \exists o \in J int (K) (S) = o \cap Y)$
28	18 27	mpbid	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to \exists o \in J int (K) (S) = o \cap Y$
29	1	eltopss	$⊢ (J \in Top \land o \in J) \to o \subseteq X$
30	29	sseld	$⊢ (J \in Top \land o \in J) \to (x \in o \to x \in X)$
31	30	adantrr	$⊢ (J \in Top \land (o \in J \land int (K) (S) = o \cap Y)) \to (x \in o \to x \in X)$
32	31	3ad2antl1	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (o \in J \land int (K) (S) = o \cap Y)) \to (x \in o \to x \in X)$
33		eldif	$⊢ x \in (X ∖ Y) \leftrightarrow (x \in X \land \neg x \in Y)$
34	33	simplbi2	$⊢ x \in X \to (\neg x \in Y \to x \in (X ∖ Y))$
35	34	orrd	$⊢ x \in X \to (x \in Y \lor x \in (X ∖ Y))$
36	32 35	syl6	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (o \in J \land int (K) (S) = o \cap Y)) \to (x \in o \to (x \in Y \lor x \in (X ∖ Y)))$
37		elin	$⊢ x \in (o \cap Y) \leftrightarrow (x \in o \land x \in Y)$
38		eleq2	$⊢ int (K) (S) = o \cap Y \to (x \in int (K) (S) \leftrightarrow x \in (o \cap Y))$
39		elun1	$⊢ x \in int (K) (S) \to x \in (int (K) (S) \cup (X ∖ Y))$
40	38 39	syl6bir	$⊢ int (K) (S) = o \cap Y \to (x \in (o \cap Y) \to x \in (int (K) (S) \cup (X ∖ Y)))$
41	40	ad2antll	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (o \in J \land int (K) (S) = o \cap Y)) \to (x \in (o \cap Y) \to x \in (int (K) (S) \cup (X ∖ Y)))$
42	37 41	biimtrrid	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (o \in J \land int (K) (S) = o \cap Y)) \to ((x \in o \land x \in Y) \to x \in (int (K) (S) \cup (X ∖ Y)))$
43	42	expdimp	$⊢ (((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (o \in J \land int (K) (S) = o \cap Y)) \land x \in o) \to (x \in Y \to x \in (int (K) (S) \cup (X ∖ Y)))$
44		elun2	$⊢ x \in (X ∖ Y) \to x \in (int (K) (S) \cup (X ∖ Y))$
45	44	a1i	$⊢ (((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (o \in J \land int (K) (S) = o \cap Y)) \land x \in o) \to (x \in (X ∖ Y) \to x \in (int (K) (S) \cup (X ∖ Y)))$
46	43 45	jaod	$⊢ (((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (o \in J \land int (K) (S) = o \cap Y)) \land x \in o) \to ((x \in Y \lor x \in (X ∖ Y)) \to x \in (int (K) (S) \cup (X ∖ Y)))$
47	46	ex	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (o \in J \land int (K) (S) = o \cap Y)) \to (x \in o \to ((x \in Y \lor x \in (X ∖ Y)) \to x \in (int (K) (S) \cup (X ∖ Y))))$
48	36 47	mpdd	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (o \in J \land int (K) (S) = o \cap Y)) \to (x \in o \to x \in (int (K) (S) \cup (X ∖ Y)))$
49	48	ssrdv	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (o \in J \land int (K) (S) = o \cap Y)) \to o \subseteq int (K) (S) \cup (X ∖ Y)$
50	11	adantr	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (o \in J \land int (K) (S) = o \cap Y)) \to J ↾_{𝑡} Y \in Top$
51	2 50	eqeltrid	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (o \in J \land int (K) (S) = o \cap Y)) \to K \in Top$
52	14	adantr	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (o \in J \land int (K) (S) = o \cap Y)) \to S \subseteq ⋃ (J ↾_{𝑡} Y)$
53	2	unieqi	$⊢ ⋃ K = ⋃ (J ↾_{𝑡} Y)$
54	53	eqcomi	$⊢ ⋃ (J ↾_{𝑡} Y) = ⋃ K$
55	54	ntrss2	$⊢ (K \in Top \land S \subseteq ⋃ (J ↾_{𝑡} Y)) \to int (K) (S) \subseteq S$
56	51 52 55	syl2anc	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (o \in J \land int (K) (S) = o \cap Y)) \to int (K) (S) \subseteq S$
57		unss1	$⊢ int (K) (S) \subseteq S \to int (K) (S) \cup (X ∖ Y) \subseteq S \cup (X ∖ Y)$
58	56 57	syl	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (o \in J \land int (K) (S) = o \cap Y)) \to int (K) (S) \cup (X ∖ Y) \subseteq S \cup (X ∖ Y)$
59	49 58	sstrd	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (o \in J \land int (K) (S) = o \cap Y)) \to o \subseteq S \cup (X ∖ Y)$
60		simpl1	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (o \in J \land o \subseteq S \cup (X ∖ Y))) \to J \in Top$
61		sstr	$⊢ (S \subseteq Y \land Y \subseteq X) \to S \subseteq X$
62	61	ancoms	$⊢ (Y \subseteq X \land S \subseteq Y) \to S \subseteq X$
63	62	3adant1	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to S \subseteq X$
64	63	adantr	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (o \in J \land o \subseteq S \cup (X ∖ Y))) \to S \subseteq X$
65		difss	$⊢ X ∖ Y \subseteq X$
66		unss	$⊢ (S \subseteq X \land X ∖ Y \subseteq X) \leftrightarrow S \cup (X ∖ Y) \subseteq X$
67	64 65 66	sylanblc	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (o \in J \land o \subseteq S \cup (X ∖ Y))) \to S \cup (X ∖ Y) \subseteq X$
68		simprl	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (o \in J \land o \subseteq S \cup (X ∖ Y))) \to o \in J$
69		simprr	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (o \in J \land o \subseteq S \cup (X ∖ Y))) \to o \subseteq S \cup (X ∖ Y)$
70	1	ssntr	$⊢ ((J \in Top \land S \cup (X ∖ Y) \subseteq X) \land (o \in J \land o \subseteq S \cup (X ∖ Y))) \to o \subseteq int (J) (S \cup (X ∖ Y))$
71	60 67 68 69 70	syl22anc	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (o \in J \land o \subseteq S \cup (X ∖ Y))) \to o \subseteq int (J) (S \cup (X ∖ Y))$
72	71	ssrind	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (o \in J \land o \subseteq S \cup (X ∖ Y))) \to o \cap Y \subseteq int (J) (S \cup (X ∖ Y)) \cap Y$
73		sseq1	$⊢ int (K) (S) = o \cap Y \to (int (K) (S) \subseteq int (J) (S \cup (X ∖ Y)) \cap Y \leftrightarrow o \cap Y \subseteq int (J) (S \cup (X ∖ Y)) \cap Y)$
74	72 73	syl5ibrcom	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (o \in J \land o \subseteq S \cup (X ∖ Y))) \to (int (K) (S) = o \cap Y \to int (K) (S) \subseteq int (J) (S \cup (X ∖ Y)) \cap Y)$
75	74	expr	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land o \in J) \to (o \subseteq S \cup (X ∖ Y) \to (int (K) (S) = o \cap Y \to int (K) (S) \subseteq int (J) (S \cup (X ∖ Y)) \cap Y))$
76	75	com23	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land o \in J) \to (int (K) (S) = o \cap Y \to (o \subseteq S \cup (X ∖ Y) \to int (K) (S) \subseteq int (J) (S \cup (X ∖ Y)) \cap Y))$
77	76	impr	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (o \in J \land int (K) (S) = o \cap Y)) \to (o \subseteq S \cup (X ∖ Y) \to int (K) (S) \subseteq int (J) (S \cup (X ∖ Y)) \cap Y)$
78	59 77	mpd	$⊢ ((J \in Top \land Y \subseteq X \land S \subseteq Y) \land (o \in J \land int (K) (S) = o \cap Y)) \to int (K) (S) \subseteq int (J) (S \cup (X ∖ Y)) \cap Y$
79	28 78	rexlimddv	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to int (K) (S) \subseteq int (J) (S \cup (X ∖ Y)) \cap Y$
80	2 11	eqeltrid	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to K \in Top$
81	8	3adant3	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to Y \in V$
82	63 65 66	sylanblc	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to S \cup (X ∖ Y) \subseteq X$
83	1	ntropn	$⊢ (J \in Top \land S \cup (X ∖ Y) \subseteq X) \to int (J) (S \cup (X ∖ Y)) \in J$
84	19 82 83	syl2anc	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to int (J) (S \cup (X ∖ Y)) \in J$
85		elrestr	$⊢ (J \in Top \land Y \in V \land int (J) (S \cup (X ∖ Y)) \in J) \to int (J) (S \cup (X ∖ Y)) \cap Y \in (J ↾_{𝑡} Y)$
86	19 81 84 85	syl3anc	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to int (J) (S \cup (X ∖ Y)) \cap Y \in (J ↾_{𝑡} Y)$
87	86 2	eleqtrrdi	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to int (J) (S \cup (X ∖ Y)) \cap Y \in K$
88	1	ntrss2	$⊢ (J \in Top \land S \cup (X ∖ Y) \subseteq X) \to int (J) (S \cup (X ∖ Y)) \subseteq S \cup (X ∖ Y)$
89	19 82 88	syl2anc	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to int (J) (S \cup (X ∖ Y)) \subseteq S \cup (X ∖ Y)$
90	89	ssrind	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to int (J) (S \cup (X ∖ Y)) \cap Y \subseteq (S \cup (X ∖ Y)) \cap Y$
91		elin	$⊢ x \in ((S \cup (X ∖ Y)) \cap Y) \leftrightarrow (x \in (S \cup (X ∖ Y)) \land x \in Y)$
92		elun	$⊢ x \in (S \cup (X ∖ Y)) \leftrightarrow (x \in S \lor x \in (X ∖ Y))$
93		orcom	$⊢ (x \in S \lor x \in (X ∖ Y)) \leftrightarrow (x \in (X ∖ Y) \lor x \in S)$
94		df-or	$⊢ (x \in (X ∖ Y) \lor x \in S) \leftrightarrow (\neg x \in (X ∖ Y) \to x \in S)$
95	93 94	bitri	$⊢ (x \in S \lor x \in (X ∖ Y)) \leftrightarrow (\neg x \in (X ∖ Y) \to x \in S)$
96	92 95	bitri	$⊢ x \in (S \cup (X ∖ Y)) \leftrightarrow (\neg x \in (X ∖ Y) \to x \in S)$
97	96	anbi1i	$⊢ (x \in (S \cup (X ∖ Y)) \land x \in Y) \leftrightarrow ((\neg x \in (X ∖ Y) \to x \in S) \land x \in Y)$
98	91 97	bitri	$⊢ x \in ((S \cup (X ∖ Y)) \cap Y) \leftrightarrow ((\neg x \in (X ∖ Y) \to x \in S) \land x \in Y)$
99		elndif	$⊢ x \in Y \to \neg x \in (X ∖ Y)$
100		pm2.27	$⊢ \neg x \in (X ∖ Y) \to ((\neg x \in (X ∖ Y) \to x \in S) \to x \in S)$
101	99 100	syl	$⊢ x \in Y \to ((\neg x \in (X ∖ Y) \to x \in S) \to x \in S)$
102	101	impcom	$⊢ ((\neg x \in (X ∖ Y) \to x \in S) \land x \in Y) \to x \in S$
103	102	a1i	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to (((\neg x \in (X ∖ Y) \to x \in S) \land x \in Y) \to x \in S)$
104	98 103	biimtrid	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to (x \in ((S \cup (X ∖ Y)) \cap Y) \to x \in S)$
105	104	ssrdv	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to (S \cup (X ∖ Y)) \cap Y \subseteq S$
106	90 105	sstrd	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to int (J) (S \cup (X ∖ Y)) \cap Y \subseteq S$
107	54	ssntr	$⊢ ((K \in Top \land S \subseteq ⋃ (J ↾_{𝑡} Y)) \land (int (J) (S \cup (X ∖ Y)) \cap Y \in K \land int (J) (S \cup (X ∖ Y)) \cap Y \subseteq S)) \to int (J) (S \cup (X ∖ Y)) \cap Y \subseteq int (K) (S)$
108	80 14 87 106 107	syl22anc	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to int (J) (S \cup (X ∖ Y)) \cap Y \subseteq int (K) (S)$
109	79 108	eqssd	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to int (K) (S) = int (J) (S \cup (X ∖ Y)) \cap Y$

Metamath Proof Explorer

Theorem restntr

Proof