restopnb

Description: If B is an open subset of the subspace base set A , then any subset of B is open iff it is open in A . (Contributed by Mario Carneiro, 2-Mar-2015)

		Ref	Expression
	Assertion	restopnb	$⊢ ((J \in Top \land A \in V) \land (B \in J \land B \subseteq A \land C \subseteq B)) \to (C \in J \leftrightarrow C \in (J ↾_{𝑡} A))$

Proof

Step	Hyp	Ref	Expression
1		simpr3	$⊢ ((J \in Top \land A \in V) \land (B \in J \land B \subseteq A \land C \subseteq B)) \to C \subseteq B$
2		simpr2	$⊢ ((J \in Top \land A \in V) \land (B \in J \land B \subseteq A \land C \subseteq B)) \to B \subseteq A$
3	1 2	sstrd	$⊢ ((J \in Top \land A \in V) \land (B \in J \land B \subseteq A \land C \subseteq B)) \to C \subseteq A$
4		dfss2	$⊢ C \subseteq A \leftrightarrow C \cap A = C$
5	3 4	sylib	$⊢ ((J \in Top \land A \in V) \land (B \in J \land B \subseteq A \land C \subseteq B)) \to C \cap A = C$
6	5	eqcomd	$⊢ ((J \in Top \land A \in V) \land (B \in J \land B \subseteq A \land C \subseteq B)) \to C = C \cap A$
7		ineq1	$⊢ v = C \to v \cap A = C \cap A$
8	7	rspceeqv	$⊢ (C \in J \land C = C \cap A) \to \exists v \in J C = v \cap A$
9	8	expcom	$⊢ C = C \cap A \to (C \in J \to \exists v \in J C = v \cap A)$
10	6 9	syl	$⊢ ((J \in Top \land A \in V) \land (B \in J \land B \subseteq A \land C \subseteq B)) \to (C \in J \to \exists v \in J C = v \cap A)$
11		inass	$⊢ (v \cap A) \cap B = v \cap (A \cap B)$
12		simprr	$⊢ (((J \in Top \land A \in V) \land (B \in J \land B \subseteq A \land C \subseteq B)) \land (v \in J \land C = v \cap A)) \to C = v \cap A$
13	12	ineq1d	$⊢ (((J \in Top \land A \in V) \land (B \in J \land B \subseteq A \land C \subseteq B)) \land (v \in J \land C = v \cap A)) \to C \cap B = (v \cap A) \cap B$
14		simplr3	$⊢ (((J \in Top \land A \in V) \land (B \in J \land B \subseteq A \land C \subseteq B)) \land v \in J) \to C \subseteq B$
15		dfss2	$⊢ C \subseteq B \leftrightarrow C \cap B = C$
16	14 15	sylib	$⊢ (((J \in Top \land A \in V) \land (B \in J \land B \subseteq A \land C \subseteq B)) \land v \in J) \to C \cap B = C$
17	16	adantrr	$⊢ (((J \in Top \land A \in V) \land (B \in J \land B \subseteq A \land C \subseteq B)) \land (v \in J \land C = v \cap A)) \to C \cap B = C$
18	13 17	eqtr3d	$⊢ (((J \in Top \land A \in V) \land (B \in J \land B \subseteq A \land C \subseteq B)) \land (v \in J \land C = v \cap A)) \to (v \cap A) \cap B = C$
19		simplr2	$⊢ (((J \in Top \land A \in V) \land (B \in J \land B \subseteq A \land C \subseteq B)) \land v \in J) \to B \subseteq A$
20		sseqin2	$⊢ B \subseteq A \leftrightarrow A \cap B = B$
21	19 20	sylib	$⊢ (((J \in Top \land A \in V) \land (B \in J \land B \subseteq A \land C \subseteq B)) \land v \in J) \to A \cap B = B$
22	21	ineq2d	$⊢ (((J \in Top \land A \in V) \land (B \in J \land B \subseteq A \land C \subseteq B)) \land v \in J) \to v \cap (A \cap B) = v \cap B$
23	22	adantrr	$⊢ (((J \in Top \land A \in V) \land (B \in J \land B \subseteq A \land C \subseteq B)) \land (v \in J \land C = v \cap A)) \to v \cap (A \cap B) = v \cap B$
24	11 18 23	3eqtr3a	$⊢ (((J \in Top \land A \in V) \land (B \in J \land B \subseteq A \land C \subseteq B)) \land (v \in J \land C = v \cap A)) \to C = v \cap B$
25		simplll	$⊢ (((J \in Top \land A \in V) \land (B \in J \land B \subseteq A \land C \subseteq B)) \land (v \in J \land C = v \cap A)) \to J \in Top$
26		simprl	$⊢ (((J \in Top \land A \in V) \land (B \in J \land B \subseteq A \land C \subseteq B)) \land (v \in J \land C = v \cap A)) \to v \in J$
27		simplr1	$⊢ (((J \in Top \land A \in V) \land (B \in J \land B \subseteq A \land C \subseteq B)) \land (v \in J \land C = v \cap A)) \to B \in J$
28		inopn	$⊢ (J \in Top \land v \in J \land B \in J) \to v \cap B \in J$
29	25 26 27 28	syl3anc	$⊢ (((J \in Top \land A \in V) \land (B \in J \land B \subseteq A \land C \subseteq B)) \land (v \in J \land C = v \cap A)) \to v \cap B \in J$
30	24 29	eqeltrd	$⊢ (((J \in Top \land A \in V) \land (B \in J \land B \subseteq A \land C \subseteq B)) \land (v \in J \land C = v \cap A)) \to C \in J$
31	30	rexlimdvaa	$⊢ ((J \in Top \land A \in V) \land (B \in J \land B \subseteq A \land C \subseteq B)) \to (\exists v \in J C = v \cap A \to C \in J)$
32	10 31	impbid	$⊢ ((J \in Top \land A \in V) \land (B \in J \land B \subseteq A \land C \subseteq B)) \to (C \in J \leftrightarrow \exists v \in J C = v \cap A)$
33		elrest	$⊢ (J \in Top \land A \in V) \to (C \in (J ↾_{𝑡} A) \leftrightarrow \exists v \in J C = v \cap A)$
34	33	adantr	$⊢ ((J \in Top \land A \in V) \land (B \in J \land B \subseteq A \land C \subseteq B)) \to (C \in (J ↾_{𝑡} A) \leftrightarrow \exists v \in J C = v \cap A)$
35	32 34	bitr4d	$⊢ ((J \in Top \land A \in V) \land (B \in J \land B \subseteq A \land C \subseteq B)) \to (C \in J \leftrightarrow C \in (J ↾_{𝑡} A))$

Metamath Proof Explorer

Theorem restopnb

Proof