elcls3

Description: Membership in a closure in terms of the members of a basis. Theorem 6.5(b) of Munkres p. 95. (Contributed by NM, 26-Feb-2007) (Revised by Mario Carneiro, 3-Sep-2015)

	Ref	Expression
Hypotheses	elcls3.1	$⊢ φ \to J = topGen (B)$
	elcls3.2	$⊢ φ \to X = ⋃ J$
	elcls3.3	$⊢ φ \to B \in TopBases$
	elcls3.4	$⊢ φ \to S \subseteq X$
	elcls3.5	$⊢ φ \to P \in X$
Assertion	elcls3	$⊢ φ \to (P \in cls (J) (S) \leftrightarrow \forall x \in B (P \in x \to x \cap S \neq \emptyset))$

Proof

Step	Hyp	Ref	Expression
1		elcls3.1	$⊢ φ \to J = topGen (B)$
2		elcls3.2	$⊢ φ \to X = ⋃ J$
3		elcls3.3	$⊢ φ \to B \in TopBases$
4		elcls3.4	$⊢ φ \to S \subseteq X$
5		elcls3.5	$⊢ φ \to P \in X$
6		tgcl	$⊢ B \in TopBases \to topGen (B) \in Top$
7	3 6	syl	$⊢ φ \to topGen (B) \in Top$
8	1 7	eqeltrd	$⊢ φ \to J \in Top$
9	4 2	sseqtrd	$⊢ φ \to S \subseteq ⋃ J$
10	5 2	eleqtrd	$⊢ φ \to P \in ⋃ J$
11		eqid	$⊢ ⋃ J = ⋃ J$
12	11	elcls	$⊢ (J \in Top \land S \subseteq ⋃ J \land P \in ⋃ J) \to (P \in cls (J) (S) \leftrightarrow \forall y \in J (P \in y \to y \cap S \neq \emptyset))$
13	8 9 10 12	syl3anc	$⊢ φ \to (P \in cls (J) (S) \leftrightarrow \forall y \in J (P \in y \to y \cap S \neq \emptyset))$
14		bastg	$⊢ B \in TopBases \to B \subseteq topGen (B)$
15	3 14	syl	$⊢ φ \to B \subseteq topGen (B)$
16	15 1	sseqtrrd	$⊢ φ \to B \subseteq J$
17	16	sseld	$⊢ φ \to (y \in B \to y \in J)$
18	17	imim1d	$⊢ φ \to ((y \in J \to (P \in y \to y \cap S \neq \emptyset)) \to (y \in B \to (P \in y \to y \cap S \neq \emptyset)))$
19	18	ralimdv2	$⊢ φ \to (\forall y \in J (P \in y \to y \cap S \neq \emptyset) \to \forall y \in B (P \in y \to y \cap S \neq \emptyset))$
20		eleq2w	$⊢ y = x \to (P \in y \leftrightarrow P \in x)$
21		ineq1	$⊢ y = x \to y \cap S = x \cap S$
22	21	neeq1d	$⊢ y = x \to (y \cap S \neq \emptyset \leftrightarrow x \cap S \neq \emptyset)$
23	20 22	imbi12d	$⊢ y = x \to ((P \in y \to y \cap S \neq \emptyset) \leftrightarrow (P \in x \to x \cap S \neq \emptyset))$
24	23	cbvralvw	$⊢ \forall y \in B (P \in y \to y \cap S \neq \emptyset) \leftrightarrow \forall x \in B (P \in x \to x \cap S \neq \emptyset)$
25	19 24	imbitrdi	$⊢ φ \to (\forall y \in J (P \in y \to y \cap S \neq \emptyset) \to \forall x \in B (P \in x \to x \cap S \neq \emptyset))$
26		simprl	$⊢ ((φ \land \forall x \in B (P \in x \to x \cap S \neq \emptyset)) \land (y \in J \land P \in y)) \to y \in J$
27	1	ad2antrr	$⊢ ((φ \land \forall x \in B (P \in x \to x \cap S \neq \emptyset)) \land (y \in J \land P \in y)) \to J = topGen (B)$
28	26 27	eleqtrd	$⊢ ((φ \land \forall x \in B (P \in x \to x \cap S \neq \emptyset)) \land (y \in J \land P \in y)) \to y \in topGen (B)$
29		simprr	$⊢ ((φ \land \forall x \in B (P \in x \to x \cap S \neq \emptyset)) \land (y \in J \land P \in y)) \to P \in y$
30		tg2	$⊢ (y \in topGen (B) \land P \in y) \to \exists z \in B (P \in z \land z \subseteq y)$
31	28 29 30	syl2anc	$⊢ ((φ \land \forall x \in B (P \in x \to x \cap S \neq \emptyset)) \land (y \in J \land P \in y)) \to \exists z \in B (P \in z \land z \subseteq y)$
32		eleq2w	$⊢ x = z \to (P \in x \leftrightarrow P \in z)$
33		ineq1	$⊢ x = z \to x \cap S = z \cap S$
34	33	neeq1d	$⊢ x = z \to (x \cap S \neq \emptyset \leftrightarrow z \cap S \neq \emptyset)$
35	32 34	imbi12d	$⊢ x = z \to ((P \in x \to x \cap S \neq \emptyset) \leftrightarrow (P \in z \to z \cap S \neq \emptyset))$
36	35	rspccva	$⊢ (\forall x \in B (P \in x \to x \cap S \neq \emptyset) \land z \in B) \to (P \in z \to z \cap S \neq \emptyset)$
37	36	imp	$⊢ ((\forall x \in B (P \in x \to x \cap S \neq \emptyset) \land z \in B) \land P \in z) \to z \cap S \neq \emptyset$
38		ssdisj	$⊢ (z \subseteq y \land y \cap S = \emptyset) \to z \cap S = \emptyset$
39	38	ex	$⊢ z \subseteq y \to (y \cap S = \emptyset \to z \cap S = \emptyset)$
40	39	necon3d	$⊢ z \subseteq y \to (z \cap S \neq \emptyset \to y \cap S \neq \emptyset)$
41	37 40	syl5com	$⊢ ((\forall x \in B (P \in x \to x \cap S \neq \emptyset) \land z \in B) \land P \in z) \to (z \subseteq y \to y \cap S \neq \emptyset)$
42	41	exp31	$⊢ \forall x \in B (P \in x \to x \cap S \neq \emptyset) \to (z \in B \to (P \in z \to (z \subseteq y \to y \cap S \neq \emptyset)))$
43	42	imp4a	$⊢ \forall x \in B (P \in x \to x \cap S \neq \emptyset) \to (z \in B \to ((P \in z \land z \subseteq y) \to y \cap S \neq \emptyset))$
44	43	rexlimdv	$⊢ \forall x \in B (P \in x \to x \cap S \neq \emptyset) \to (\exists z \in B (P \in z \land z \subseteq y) \to y \cap S \neq \emptyset)$
45	44	ad2antlr	$⊢ ((φ \land \forall x \in B (P \in x \to x \cap S \neq \emptyset)) \land (y \in J \land P \in y)) \to (\exists z \in B (P \in z \land z \subseteq y) \to y \cap S \neq \emptyset)$
46	31 45	mpd	$⊢ ((φ \land \forall x \in B (P \in x \to x \cap S \neq \emptyset)) \land (y \in J \land P \in y)) \to y \cap S \neq \emptyset$
47	46	exp43	$⊢ φ \to (\forall x \in B (P \in x \to x \cap S \neq \emptyset) \to (y \in J \to (P \in y \to y \cap S \neq \emptyset)))$
48	47	ralrimdv	$⊢ φ \to (\forall x \in B (P \in x \to x \cap S \neq \emptyset) \to \forall y \in J (P \in y \to y \cap S \neq \emptyset))$
49	25 48	impbid	$⊢ φ \to (\forall y \in J (P \in y \to y \cap S \neq \emptyset) \leftrightarrow \forall x \in B (P \in x \to x \cap S \neq \emptyset))$
50	13 49	bitrd	$⊢ φ \to (P \in cls (J) (S) \leftrightarrow \forall x \in B (P \in x \to x \cap S \neq \emptyset))$

Metamath Proof Explorer

Theorem elcls3

Proof