restbas

Description: A subspace topology basis is a basis. (Contributed by Mario Carneiro, 19-Mar-2015)

		Ref	Expression
	Assertion	restbas	$⊢ B \in TopBases \to B ↾_{𝑡} A \in TopBases$

Proof

Step	Hyp	Ref	Expression
1		elrest	$⊢ (B \in TopBases \land A \in V) \to (a \in (B ↾_{𝑡} A) \leftrightarrow \exists u \in B a = u \cap A)$
2		elrest	$⊢ (B \in TopBases \land A \in V) \to (b \in (B ↾_{𝑡} A) \leftrightarrow \exists v \in B b = v \cap A)$
3	1 2	anbi12d	$⊢ (B \in TopBases \land A \in V) \to ((a \in (B ↾_{𝑡} A) \land b \in (B ↾_{𝑡} A)) \leftrightarrow (\exists u \in B a = u \cap A \land \exists v \in B b = v \cap A))$
4		reeanv	$⊢ \exists u \in B \exists v \in B (a = u \cap A \land b = v \cap A) \leftrightarrow (\exists u \in B a = u \cap A \land \exists v \in B b = v \cap A)$
5	3 4	syl6bbr	$⊢ (B \in TopBases \land A \in V) \to ((a \in (B ↾_{𝑡} A) \land b \in (B ↾_{𝑡} A)) \leftrightarrow \exists u \in B \exists v \in B (a = u \cap A \land b = v \cap A))$
6		simplll	$⊢ (((B \in TopBases \land A \in V) \land (u \in B \land v \in B)) \land c \in ((u \cap v) \cap A)) \to B \in TopBases$
7		simplrl	$⊢ (((B \in TopBases \land A \in V) \land (u \in B \land v \in B)) \land c \in ((u \cap v) \cap A)) \to u \in B$
8		simplrr	$⊢ (((B \in TopBases \land A \in V) \land (u \in B \land v \in B)) \land c \in ((u \cap v) \cap A)) \to v \in B$
9		simpr	$⊢ (((B \in TopBases \land A \in V) \land (u \in B \land v \in B)) \land c \in ((u \cap v) \cap A)) \to c \in ((u \cap v) \cap A)$
10	9	elin1d	$⊢ (((B \in TopBases \land A \in V) \land (u \in B \land v \in B)) \land c \in ((u \cap v) \cap A)) \to c \in (u \cap v)$
11		basis2	$⊢ ((B \in TopBases \land u \in B) \land (v \in B \land c \in (u \cap v))) \to \exists z \in B (c \in z \land z \subseteq u \cap v)$
12	6 7 8 10 11	syl22anc	$⊢ (((B \in TopBases \land A \in V) \land (u \in B \land v \in B)) \land c \in ((u \cap v) \cap A)) \to \exists z \in B (c \in z \land z \subseteq u \cap v)$
13		simplll	$⊢ ((((B \in TopBases \land A \in V) \land (u \in B \land v \in B)) \land c \in ((u \cap v) \cap A)) \land (z \in B \land (c \in z \land z \subseteq u \cap v))) \to (B \in TopBases \land A \in V)$
14	13	simpld	$⊢ ((((B \in TopBases \land A \in V) \land (u \in B \land v \in B)) \land c \in ((u \cap v) \cap A)) \land (z \in B \land (c \in z \land z \subseteq u \cap v))) \to B \in TopBases$
15	13	simprd	$⊢ ((((B \in TopBases \land A \in V) \land (u \in B \land v \in B)) \land c \in ((u \cap v) \cap A)) \land (z \in B \land (c \in z \land z \subseteq u \cap v))) \to A \in V$
16		simprl	$⊢ ((((B \in TopBases \land A \in V) \land (u \in B \land v \in B)) \land c \in ((u \cap v) \cap A)) \land (z \in B \land (c \in z \land z \subseteq u \cap v))) \to z \in B$
17		elrestr	$⊢ (B \in TopBases \land A \in V \land z \in B) \to z \cap A \in (B ↾_{𝑡} A)$
18	14 15 16 17	syl3anc	$⊢ ((((B \in TopBases \land A \in V) \land (u \in B \land v \in B)) \land c \in ((u \cap v) \cap A)) \land (z \in B \land (c \in z \land z \subseteq u \cap v))) \to z \cap A \in (B ↾_{𝑡} A)$
19		simprrl	$⊢ ((((B \in TopBases \land A \in V) \land (u \in B \land v \in B)) \land c \in ((u \cap v) \cap A)) \land (z \in B \land (c \in z \land z \subseteq u \cap v))) \to c \in z$
20		simplr	$⊢ ((((B \in TopBases \land A \in V) \land (u \in B \land v \in B)) \land c \in ((u \cap v) \cap A)) \land (z \in B \land (c \in z \land z \subseteq u \cap v))) \to c \in ((u \cap v) \cap A)$
21	20	elin2d	$⊢ ((((B \in TopBases \land A \in V) \land (u \in B \land v \in B)) \land c \in ((u \cap v) \cap A)) \land (z \in B \land (c \in z \land z \subseteq u \cap v))) \to c \in A$
22	19 21	elind	$⊢ ((((B \in TopBases \land A \in V) \land (u \in B \land v \in B)) \land c \in ((u \cap v) \cap A)) \land (z \in B \land (c \in z \land z \subseteq u \cap v))) \to c \in (z \cap A)$
23		simprrr	$⊢ ((((B \in TopBases \land A \in V) \land (u \in B \land v \in B)) \land c \in ((u \cap v) \cap A)) \land (z \in B \land (c \in z \land z \subseteq u \cap v))) \to z \subseteq u \cap v$
24	23	ssrind	$⊢ ((((B \in TopBases \land A \in V) \land (u \in B \land v \in B)) \land c \in ((u \cap v) \cap A)) \land (z \in B \land (c \in z \land z \subseteq u \cap v))) \to z \cap A \subseteq (u \cap v) \cap A$
25		eleq2	$⊢ w = z \cap A \to (c \in w \leftrightarrow c \in (z \cap A))$
26		sseq1	$⊢ w = z \cap A \to (w \subseteq (u \cap v) \cap A \leftrightarrow z \cap A \subseteq (u \cap v) \cap A)$
27	25 26	anbi12d	$⊢ w = z \cap A \to ((c \in w \land w \subseteq (u \cap v) \cap A) \leftrightarrow (c \in (z \cap A) \land z \cap A \subseteq (u \cap v) \cap A))$
28	27	rspcev	$⊢ (z \cap A \in (B ↾_{𝑡} A) \land (c \in (z \cap A) \land z \cap A \subseteq (u \cap v) \cap A)) \to \exists w \in (B ↾_{𝑡} A) (c \in w \land w \subseteq (u \cap v) \cap A)$
29	18 22 24 28	syl12anc	$⊢ ((((B \in TopBases \land A \in V) \land (u \in B \land v \in B)) \land c \in ((u \cap v) \cap A)) \land (z \in B \land (c \in z \land z \subseteq u \cap v))) \to \exists w \in (B ↾_{𝑡} A) (c \in w \land w \subseteq (u \cap v) \cap A)$
30	12 29	rexlimddv	$⊢ (((B \in TopBases \land A \in V) \land (u \in B \land v \in B)) \land c \in ((u \cap v) \cap A)) \to \exists w \in (B ↾_{𝑡} A) (c \in w \land w \subseteq (u \cap v) \cap A)$
31	30	ralrimiva	$⊢ ((B \in TopBases \land A \in V) \land (u \in B \land v \in B)) \to \forall c \in ((u \cap v) \cap A) \exists w \in (B ↾_{𝑡} A) (c \in w \land w \subseteq (u \cap v) \cap A)$
32		ineq12	$⊢ (a = u \cap A \land b = v \cap A) \to a \cap b = (u \cap A) \cap (v \cap A)$
33		inindir	$⊢ (u \cap v) \cap A = (u \cap A) \cap (v \cap A)$
34	32 33	syl6eqr	$⊢ (a = u \cap A \land b = v \cap A) \to a \cap b = (u \cap v) \cap A$
35	34	sseq2d	$⊢ (a = u \cap A \land b = v \cap A) \to (w \subseteq a \cap b \leftrightarrow w \subseteq (u \cap v) \cap A)$
36	35	anbi2d	$⊢ (a = u \cap A \land b = v \cap A) \to ((c \in w \land w \subseteq a \cap b) \leftrightarrow (c \in w \land w \subseteq (u \cap v) \cap A))$
37	36	rexbidv	$⊢ (a = u \cap A \land b = v \cap A) \to (\exists w \in (B ↾_{𝑡} A) (c \in w \land w \subseteq a \cap b) \leftrightarrow \exists w \in (B ↾_{𝑡} A) (c \in w \land w \subseteq (u \cap v) \cap A))$
38	34 37	raleqbidv	$⊢ (a = u \cap A \land b = v \cap A) \to (\forall c \in (a \cap b) \exists w \in (B ↾_{𝑡} A) (c \in w \land w \subseteq a \cap b) \leftrightarrow \forall c \in ((u \cap v) \cap A) \exists w \in (B ↾_{𝑡} A) (c \in w \land w \subseteq (u \cap v) \cap A))$
39	31 38	syl5ibrcom	$⊢ ((B \in TopBases \land A \in V) \land (u \in B \land v \in B)) \to ((a = u \cap A \land b = v \cap A) \to \forall c \in (a \cap b) \exists w \in (B ↾_{𝑡} A) (c \in w \land w \subseteq a \cap b))$
40	39	rexlimdvva	$⊢ (B \in TopBases \land A \in V) \to (\exists u \in B \exists v \in B (a = u \cap A \land b = v \cap A) \to \forall c \in (a \cap b) \exists w \in (B ↾_{𝑡} A) (c \in w \land w \subseteq a \cap b))$
41	5 40	sylbid	$⊢ (B \in TopBases \land A \in V) \to ((a \in (B ↾_{𝑡} A) \land b \in (B ↾_{𝑡} A)) \to \forall c \in (a \cap b) \exists w \in (B ↾_{𝑡} A) (c \in w \land w \subseteq a \cap b))$
42	41	ralrimivv	$⊢ (B \in TopBases \land A \in V) \to \forall a \in (B ↾_{𝑡} A) \forall b \in (B ↾_{𝑡} A) \forall c \in (a \cap b) \exists w \in (B ↾_{𝑡} A) (c \in w \land w \subseteq a \cap b)$
43		ovex	$⊢ B ↾_{𝑡} A \in V$
44		isbasis2g	$⊢ B ↾_{𝑡} A \in V \to (B ↾_{𝑡} A \in TopBases \leftrightarrow \forall a \in (B ↾_{𝑡} A) \forall b \in (B ↾_{𝑡} A) \forall c \in (a \cap b) \exists w \in (B ↾_{𝑡} A) (c \in w \land w \subseteq a \cap b))$
45	43 44	ax-mp	$⊢ B ↾_{𝑡} A \in TopBases \leftrightarrow \forall a \in (B ↾_{𝑡} A) \forall b \in (B ↾_{𝑡} A) \forall c \in (a \cap b) \exists w \in (B ↾_{𝑡} A) (c \in w \land w \subseteq a \cap b)$
46	42 45	sylibr	$⊢ (B \in TopBases \land A \in V) \to B ↾_{𝑡} A \in TopBases$
47		relxp	$⊢ Rel (V \times V)$
48		restfn	$⊢ ↾_{𝑡} Fn (V \times V)$
49		fndm	$⊢ ↾_{𝑡} Fn (V \times V) \to dom ↾_{𝑡} = V \times V$
50	48 49	ax-mp	$⊢ dom ↾_{𝑡} = V \times V$
51	50	releqi	$⊢ Rel dom ↾_{𝑡} \leftrightarrow Rel (V \times V)$
52	47 51	mpbir	$⊢ Rel dom ↾_{𝑡}$
53	52	ovprc2	$⊢ \neg A \in V \to B ↾_{𝑡} A = \emptyset$
54	53	adantl	$⊢ (B \in TopBases \land \neg A \in V) \to B ↾_{𝑡} A = \emptyset$
55		fi0	$⊢ fi (\emptyset) = \emptyset$
56		fibas	$⊢ fi (\emptyset) \in TopBases$
57	55 56	eqeltrri	$⊢ \emptyset \in TopBases$
58	54 57	eqeltrdi	$⊢ (B \in TopBases \land \neg A \in V) \to B ↾_{𝑡} A \in TopBases$
59	46 58	pm2.61dan	$⊢ B \in TopBases \to B ↾_{𝑡} A \in TopBases$

Metamath Proof Explorer

Theorem restbas

Proof