opnfbas

Description: The collection of open supersets of a nonempty set in a topology is a neighborhoods of the set, one of the motivations for the filter concept. (Contributed by Jeff Hankins, 2-Sep-2009) (Revised by Mario Carneiro, 7-Aug-2015)

		Ref	Expression
	Hypothesis	opnfbas.1	$⊢ X = ⋃ J$
	Assertion	opnfbas	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to \{x \in J \| S \subseteq x\} \in fBas (X)$

Proof

Step	Hyp	Ref	Expression
1		opnfbas.1	$⊢ X = ⋃ J$
2		ssrab2	$⊢ \{x \in J \| S \subseteq x\} \subseteq J$
3	1	eqimss2i	$⊢ ⋃ J \subseteq X$
4		sspwuni	$⊢ J \subseteq 𝒫 X \leftrightarrow ⋃ J \subseteq X$
5	3 4	mpbir	$⊢ J \subseteq 𝒫 X$
6	2 5	sstri	$⊢ \{x \in J \| S \subseteq x\} \subseteq 𝒫 X$
7	6	a1i	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to \{x \in J \| S \subseteq x\} \subseteq 𝒫 X$
8	1	topopn	$⊢ J \in Top \to X \in J$
9	8	anim1i	$⊢ (J \in Top \land S \subseteq X) \to (X \in J \land S \subseteq X)$
10	9	3adant3	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to (X \in J \land S \subseteq X)$
11		sseq2	$⊢ x = X \to (S \subseteq x \leftrightarrow S \subseteq X)$
12	11	elrab	$⊢ X \in \{x \in J \| S \subseteq x\} \leftrightarrow (X \in J \land S \subseteq X)$
13	10 12	sylibr	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to X \in \{x \in J \| S \subseteq x\}$
14	13	ne0d	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to \{x \in J \| S \subseteq x\} \neq \emptyset$
15		ss0	$⊢ S \subseteq \emptyset \to S = \emptyset$
16	15	necon3ai	$⊢ S \neq \emptyset \to \neg S \subseteq \emptyset$
17	16	3ad2ant3	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to \neg S \subseteq \emptyset$
18	17	intnand	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to \neg (\emptyset \in J \land S \subseteq \emptyset)$
19		df-nel	$⊢ \emptyset \notin \{x \in J \| S \subseteq x\} \leftrightarrow \neg \emptyset \in \{x \in J \| S \subseteq x\}$
20		sseq2	$⊢ x = \emptyset \to (S \subseteq x \leftrightarrow S \subseteq \emptyset)$
21	20	elrab	$⊢ \emptyset \in \{x \in J \| S \subseteq x\} \leftrightarrow (\emptyset \in J \land S \subseteq \emptyset)$
22	21	notbii	$⊢ \neg \emptyset \in \{x \in J \| S \subseteq x\} \leftrightarrow \neg (\emptyset \in J \land S \subseteq \emptyset)$
23	19 22	bitr2i	$⊢ \neg (\emptyset \in J \land S \subseteq \emptyset) \leftrightarrow \emptyset \notin \{x \in J \| S \subseteq x\}$
24	18 23	sylib	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to \emptyset \notin \{x \in J \| S \subseteq x\}$
25		sseq2	$⊢ x = r \to (S \subseteq x \leftrightarrow S \subseteq r)$
26	25	elrab	$⊢ r \in \{x \in J \| S \subseteq x\} \leftrightarrow (r \in J \land S \subseteq r)$
27		sseq2	$⊢ x = s \to (S \subseteq x \leftrightarrow S \subseteq s)$
28	27	elrab	$⊢ s \in \{x \in J \| S \subseteq x\} \leftrightarrow (s \in J \land S \subseteq s)$
29	26 28	anbi12i	$⊢ (r \in \{x \in J \| S \subseteq x\} \land s \in \{x \in J \| S \subseteq x\}) \leftrightarrow ((r \in J \land S \subseteq r) \land (s \in J \land S \subseteq s))$
30		simpl	$⊢ (J \in Top \land ((r \in J \land S \subseteq r) \land (s \in J \land S \subseteq s))) \to J \in Top$
31		simprll	$⊢ (J \in Top \land ((r \in J \land S \subseteq r) \land (s \in J \land S \subseteq s))) \to r \in J$
32		simprrl	$⊢ (J \in Top \land ((r \in J \land S \subseteq r) \land (s \in J \land S \subseteq s))) \to s \in J$
33		inopn	$⊢ (J \in Top \land r \in J \land s \in J) \to r \cap s \in J$
34	30 31 32 33	syl3anc	$⊢ (J \in Top \land ((r \in J \land S \subseteq r) \land (s \in J \land S \subseteq s))) \to r \cap s \in J$
35		ssin	$⊢ (S \subseteq r \land S \subseteq s) \leftrightarrow S \subseteq r \cap s$
36	35	biimpi	$⊢ (S \subseteq r \land S \subseteq s) \to S \subseteq r \cap s$
37	36	ad2ant2l	$⊢ ((r \in J \land S \subseteq r) \land (s \in J \land S \subseteq s)) \to S \subseteq r \cap s$
38	37	adantl	$⊢ (J \in Top \land ((r \in J \land S \subseteq r) \land (s \in J \land S \subseteq s))) \to S \subseteq r \cap s$
39	34 38	jca	$⊢ (J \in Top \land ((r \in J \land S \subseteq r) \land (s \in J \land S \subseteq s))) \to (r \cap s \in J \land S \subseteq r \cap s)$
40	39	3ad2antl1	$⊢ ((J \in Top \land S \subseteq X \land S \neq \emptyset) \land ((r \in J \land S \subseteq r) \land (s \in J \land S \subseteq s))) \to (r \cap s \in J \land S \subseteq r \cap s)$
41		sseq2	$⊢ x = r \cap s \to (S \subseteq x \leftrightarrow S \subseteq r \cap s)$
42	41	elrab	$⊢ r \cap s \in \{x \in J \| S \subseteq x\} \leftrightarrow (r \cap s \in J \land S \subseteq r \cap s)$
43	40 42	sylibr	$⊢ ((J \in Top \land S \subseteq X \land S \neq \emptyset) \land ((r \in J \land S \subseteq r) \land (s \in J \land S \subseteq s))) \to r \cap s \in \{x \in J \| S \subseteq x\}$
44		ssid	$⊢ r \cap s \subseteq r \cap s$
45		sseq1	$⊢ t = r \cap s \to (t \subseteq r \cap s \leftrightarrow r \cap s \subseteq r \cap s)$
46	45	rspcev	$⊢ (r \cap s \in \{x \in J \| S \subseteq x\} \land r \cap s \subseteq r \cap s) \to \exists t \in \{x \in J \| S \subseteq x\} t \subseteq r \cap s$
47	43 44 46	sylancl	$⊢ ((J \in Top \land S \subseteq X \land S \neq \emptyset) \land ((r \in J \land S \subseteq r) \land (s \in J \land S \subseteq s))) \to \exists t \in \{x \in J \| S \subseteq x\} t \subseteq r \cap s$
48	47	ex	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to (((r \in J \land S \subseteq r) \land (s \in J \land S \subseteq s)) \to \exists t \in \{x \in J \| S \subseteq x\} t \subseteq r \cap s)$
49	29 48	biimtrid	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to ((r \in \{x \in J \| S \subseteq x\} \land s \in \{x \in J \| S \subseteq x\}) \to \exists t \in \{x \in J \| S \subseteq x\} t \subseteq r \cap s)$
50	49	ralrimivv	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to \forall r \in \{x \in J \| S \subseteq x\} \forall s \in \{x \in J \| S \subseteq x\} \exists t \in \{x \in J \| S \subseteq x\} t \subseteq r \cap s$
51	14 24 50	3jca	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to (\{x \in J \| S \subseteq x\} \neq \emptyset \land \emptyset \notin \{x \in J \| S \subseteq x\} \land \forall r \in \{x \in J \| S \subseteq x\} \forall s \in \{x \in J \| S \subseteq x\} \exists t \in \{x \in J \| S \subseteq x\} t \subseteq r \cap s)$
52		isfbas2	$⊢ X \in J \to (\{x \in J \| S \subseteq x\} \in fBas (X) \leftrightarrow (\{x \in J \| S \subseteq x\} \subseteq 𝒫 X \land (\{x \in J \| S \subseteq x\} \neq \emptyset \land \emptyset \notin \{x \in J \| S \subseteq x\} \land \forall r \in \{x \in J \| S \subseteq x\} \forall s \in \{x \in J \| S \subseteq x\} \exists t \in \{x \in J \| S \subseteq x\} t \subseteq r \cap s)))$
53	8 52	syl	$⊢ J \in Top \to (\{x \in J \| S \subseteq x\} \in fBas (X) \leftrightarrow (\{x \in J \| S \subseteq x\} \subseteq 𝒫 X \land (\{x \in J \| S \subseteq x\} \neq \emptyset \land \emptyset \notin \{x \in J \| S \subseteq x\} \land \forall r \in \{x \in J \| S \subseteq x\} \forall s \in \{x \in J \| S \subseteq x\} \exists t \in \{x \in J \| S \subseteq x\} t \subseteq r \cap s)))$
54	53	3ad2ant1	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to (\{x \in J \| S \subseteq x\} \in fBas (X) \leftrightarrow (\{x \in J \| S \subseteq x\} \subseteq 𝒫 X \land (\{x \in J \| S \subseteq x\} \neq \emptyset \land \emptyset \notin \{x \in J \| S \subseteq x\} \land \forall r \in \{x \in J \| S \subseteq x\} \forall s \in \{x \in J \| S \subseteq x\} \exists t \in \{x \in J \| S \subseteq x\} t \subseteq r \cap s)))$
55	7 51 54	mpbir2and	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to \{x \in J \| S \subseteq x\} \in fBas (X)$

Metamath Proof Explorer

Theorem opnfbas

Proof