neibastop2

Description: In the topology generated by a neighborhood base, a set is a neighborhood of a point iff it contains a subset in the base. (Contributed by Jeff Hankins, 9-Sep-2009) (Proof shortened by Mario Carneiro, 11-Sep-2015)

	Ref	Expression
Hypotheses	neibastop1.1	$⊢ φ \to X \in V$
	neibastop1.2	$⊢ φ \to F : X ⟶ 𝒫 𝒫 X ∖ \{\emptyset\}$
	neibastop1.3	$⊢ (φ \land (x \in X \land v \in F (x) \land w \in F (x))) \to F (x) \cap 𝒫 (v \cap w) \neq \emptyset$
	neibastop1.4	$⊢ J = \{o \in 𝒫 X \| \forall x \in o F (x) \cap 𝒫 o \neq \emptyset\}$
	neibastop1.5	$⊢ (φ \land (x \in X \land v \in F (x))) \to x \in v$
	neibastop1.6	$⊢ (φ \land (x \in X \land v \in F (x))) \to \exists t \in F (x) \forall y \in t F (y) \cap 𝒫 v \neq \emptyset$
Assertion	neibastop2	$⊢ (φ \land P \in X) \to (N \in nei (J) (\{P\}) \leftrightarrow (N \subseteq X \land F (P) \cap 𝒫 N \neq \emptyset))$

Proof

Step	Hyp	Ref	Expression
1		neibastop1.1	$⊢ φ \to X \in V$
2		neibastop1.2	$⊢ φ \to F : X ⟶ 𝒫 𝒫 X ∖ \{\emptyset\}$
3		neibastop1.3	$⊢ (φ \land (x \in X \land v \in F (x) \land w \in F (x))) \to F (x) \cap 𝒫 (v \cap w) \neq \emptyset$
4		neibastop1.4	$⊢ J = \{o \in 𝒫 X \| \forall x \in o F (x) \cap 𝒫 o \neq \emptyset\}$
5		neibastop1.5	$⊢ (φ \land (x \in X \land v \in F (x))) \to x \in v$
6		neibastop1.6	$⊢ (φ \land (x \in X \land v \in F (x))) \to \exists t \in F (x) \forall y \in t F (y) \cap 𝒫 v \neq \emptyset$
7	1 2 3 4	neibastop1	$⊢ φ \to J \in TopOn (X)$
8		topontop	$⊢ J \in TopOn (X) \to J \in Top$
9	7 8	syl	$⊢ φ \to J \in Top$
10	9	adantr	$⊢ (φ \land P \in X) \to J \in Top$
11		eqid	$⊢ ⋃ J = ⋃ J$
12	11	neii1	$⊢ (J \in Top \land N \in nei (J) (\{P\})) \to N \subseteq ⋃ J$
13	10 12	sylan	$⊢ ((φ \land P \in X) \land N \in nei (J) (\{P\})) \to N \subseteq ⋃ J$
14		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
15	7 14	syl	$⊢ φ \to X = ⋃ J$
16	15	ad2antrr	$⊢ ((φ \land P \in X) \land N \in nei (J) (\{P\})) \to X = ⋃ J$
17	13 16	sseqtrrd	$⊢ ((φ \land P \in X) \land N \in nei (J) (\{P\})) \to N \subseteq X$
18		neii2	$⊢ (J \in Top \land N \in nei (J) (\{P\})) \to \exists y \in J (\{P\} \subseteq y \land y \subseteq N)$
19	10 18	sylan	$⊢ ((φ \land P \in X) \land N \in nei (J) (\{P\})) \to \exists y \in J (\{P\} \subseteq y \land y \subseteq N)$
20		pweq	$⊢ o = y \to 𝒫 o = 𝒫 y$
21	20	ineq2d	$⊢ o = y \to F (x) \cap 𝒫 o = F (x) \cap 𝒫 y$
22	21	neeq1d	$⊢ o = y \to (F (x) \cap 𝒫 o \neq \emptyset \leftrightarrow F (x) \cap 𝒫 y \neq \emptyset)$
23	22	raleqbi1dv	$⊢ o = y \to (\forall x \in o F (x) \cap 𝒫 o \neq \emptyset \leftrightarrow \forall x \in y F (x) \cap 𝒫 y \neq \emptyset)$
24	23 4	elrab2	$⊢ y \in J \leftrightarrow (y \in 𝒫 X \land \forall x \in y F (x) \cap 𝒫 y \neq \emptyset)$
25		simprrr	$⊢ (((φ \land P \in X) \land N \in nei (J) (\{P\})) \land (y \in 𝒫 X \land (\{P\} \subseteq y \land y \subseteq N))) \to y \subseteq N$
26		sspwb	$⊢ y \subseteq N \leftrightarrow 𝒫 y \subseteq 𝒫 N$
27	25 26	sylib	$⊢ (((φ \land P \in X) \land N \in nei (J) (\{P\})) \land (y \in 𝒫 X \land (\{P\} \subseteq y \land y \subseteq N))) \to 𝒫 y \subseteq 𝒫 N$
28		sslin	$⊢ 𝒫 y \subseteq 𝒫 N \to F (P) \cap 𝒫 y \subseteq F (P) \cap 𝒫 N$
29	27 28	syl	$⊢ (((φ \land P \in X) \land N \in nei (J) (\{P\})) \land (y \in 𝒫 X \land (\{P\} \subseteq y \land y \subseteq N))) \to F (P) \cap 𝒫 y \subseteq F (P) \cap 𝒫 N$
30		simprrl	$⊢ (((φ \land P \in X) \land N \in nei (J) (\{P\})) \land (y \in 𝒫 X \land (\{P\} \subseteq y \land y \subseteq N))) \to \{P\} \subseteq y$
31		snssg	$⊢ P \in X \to (P \in y \leftrightarrow \{P\} \subseteq y)$
32	31	ad3antlr	$⊢ (((φ \land P \in X) \land N \in nei (J) (\{P\})) \land (y \in 𝒫 X \land (\{P\} \subseteq y \land y \subseteq N))) \to (P \in y \leftrightarrow \{P\} \subseteq y)$
33	30 32	mpbird	$⊢ (((φ \land P \in X) \land N \in nei (J) (\{P\})) \land (y \in 𝒫 X \land (\{P\} \subseteq y \land y \subseteq N))) \to P \in y$
34		fveq2	$⊢ x = P \to F (x) = F (P)$
35	34	ineq1d	$⊢ x = P \to F (x) \cap 𝒫 y = F (P) \cap 𝒫 y$
36	35	neeq1d	$⊢ x = P \to (F (x) \cap 𝒫 y \neq \emptyset \leftrightarrow F (P) \cap 𝒫 y \neq \emptyset)$
37	36	rspcv	$⊢ P \in y \to (\forall x \in y F (x) \cap 𝒫 y \neq \emptyset \to F (P) \cap 𝒫 y \neq \emptyset)$
38	33 37	syl	$⊢ (((φ \land P \in X) \land N \in nei (J) (\{P\})) \land (y \in 𝒫 X \land (\{P\} \subseteq y \land y \subseteq N))) \to (\forall x \in y F (x) \cap 𝒫 y \neq \emptyset \to F (P) \cap 𝒫 y \neq \emptyset)$
39		ssn0	$⊢ (F (P) \cap 𝒫 y \subseteq F (P) \cap 𝒫 N \land F (P) \cap 𝒫 y \neq \emptyset) \to F (P) \cap 𝒫 N \neq \emptyset$
40	29 38 39	syl6an	$⊢ (((φ \land P \in X) \land N \in nei (J) (\{P\})) \land (y \in 𝒫 X \land (\{P\} \subseteq y \land y \subseteq N))) \to (\forall x \in y F (x) \cap 𝒫 y \neq \emptyset \to F (P) \cap 𝒫 N \neq \emptyset)$
41	40	expr	$⊢ (((φ \land P \in X) \land N \in nei (J) (\{P\})) \land y \in 𝒫 X) \to ((\{P\} \subseteq y \land y \subseteq N) \to (\forall x \in y F (x) \cap 𝒫 y \neq \emptyset \to F (P) \cap 𝒫 N \neq \emptyset))$
42	41	com23	$⊢ (((φ \land P \in X) \land N \in nei (J) (\{P\})) \land y \in 𝒫 X) \to (\forall x \in y F (x) \cap 𝒫 y \neq \emptyset \to ((\{P\} \subseteq y \land y \subseteq N) \to F (P) \cap 𝒫 N \neq \emptyset))$
43	42	expimpd	$⊢ ((φ \land P \in X) \land N \in nei (J) (\{P\})) \to ((y \in 𝒫 X \land \forall x \in y F (x) \cap 𝒫 y \neq \emptyset) \to ((\{P\} \subseteq y \land y \subseteq N) \to F (P) \cap 𝒫 N \neq \emptyset))$
44	24 43	syl5bi	$⊢ ((φ \land P \in X) \land N \in nei (J) (\{P\})) \to (y \in J \to ((\{P\} \subseteq y \land y \subseteq N) \to F (P) \cap 𝒫 N \neq \emptyset))$
45	44	rexlimdv	$⊢ ((φ \land P \in X) \land N \in nei (J) (\{P\})) \to (\exists y \in J (\{P\} \subseteq y \land y \subseteq N) \to F (P) \cap 𝒫 N \neq \emptyset)$
46	19 45	mpd	$⊢ ((φ \land P \in X) \land N \in nei (J) (\{P\})) \to F (P) \cap 𝒫 N \neq \emptyset$
47	17 46	jca	$⊢ ((φ \land P \in X) \land N \in nei (J) (\{P\})) \to (N \subseteq X \land F (P) \cap 𝒫 N \neq \emptyset)$
48	47	ex	$⊢ (φ \land P \in X) \to (N \in nei (J) (\{P\}) \to (N \subseteq X \land F (P) \cap 𝒫 N \neq \emptyset))$
49		n0	$⊢ F (P) \cap 𝒫 N \neq \emptyset \leftrightarrow \exists s s \in (F (P) \cap 𝒫 N)$
50		elin	$⊢ s \in (F (P) \cap 𝒫 N) \leftrightarrow (s \in F (P) \land s \in 𝒫 N)$
51		simprl	$⊢ ((φ \land P \in X) \land (N \subseteq X \land (s \in F (P) \land s \in 𝒫 N))) \to N \subseteq X$
52	15	ad2antrr	$⊢ ((φ \land P \in X) \land (N \subseteq X \land (s \in F (P) \land s \in 𝒫 N))) \to X = ⋃ J$
53	51 52	sseqtrd	$⊢ ((φ \land P \in X) \land (N \subseteq X \land (s \in F (P) \land s \in 𝒫 N))) \to N \subseteq ⋃ J$
54	1	ad2antrr	$⊢ ((φ \land P \in X) \land (N \subseteq X \land (s \in F (P) \land s \in 𝒫 N))) \to X \in V$
55	2	ad2antrr	$⊢ ((φ \land P \in X) \land (N \subseteq X \land (s \in F (P) \land s \in 𝒫 N))) \to F : X ⟶ 𝒫 𝒫 X ∖ \{\emptyset\}$
56		simpll	$⊢ ((φ \land P \in X) \land (N \subseteq X \land (s \in F (P) \land s \in 𝒫 N))) \to φ$
57	56 3	sylan	$⊢ (((φ \land P \in X) \land (N \subseteq X \land (s \in F (P) \land s \in 𝒫 N))) \land (x \in X \land v \in F (x) \land w \in F (x))) \to F (x) \cap 𝒫 (v \cap w) \neq \emptyset$
58	56 5	sylan	$⊢ (((φ \land P \in X) \land (N \subseteq X \land (s \in F (P) \land s \in 𝒫 N))) \land (x \in X \land v \in F (x))) \to x \in v$
59	56 6	sylan	$⊢ (((φ \land P \in X) \land (N \subseteq X \land (s \in F (P) \land s \in 𝒫 N))) \land (x \in X \land v \in F (x))) \to \exists t \in F (x) \forall y \in t F (y) \cap 𝒫 v \neq \emptyset$
60		simplr	$⊢ ((φ \land P \in X) \land (N \subseteq X \land (s \in F (P) \land s \in 𝒫 N))) \to P \in X$
61		simprrl	$⊢ ((φ \land P \in X) \land (N \subseteq X \land (s \in F (P) \land s \in 𝒫 N))) \to s \in F (P)$
62		simprrr	$⊢ ((φ \land P \in X) \land (N \subseteq X \land (s \in F (P) \land s \in 𝒫 N))) \to s \in 𝒫 N$
63	62	elpwid	$⊢ ((φ \land P \in X) \land (N \subseteq X \land (s \in F (P) \land s \in 𝒫 N))) \to s \subseteq N$
64		fveq2	$⊢ n = x \to F (n) = F (x)$
65	64	ineq1d	$⊢ n = x \to F (n) \cap 𝒫 b = F (x) \cap 𝒫 b$
66	65	cbviunv	$⊢ ⋃_{n \in X} (F (n) \cap 𝒫 b) = ⋃_{x \in X} (F (x) \cap 𝒫 b)$
67		pweq	$⊢ b = z \to 𝒫 b = 𝒫 z$
68	67	ineq2d	$⊢ b = z \to F (x) \cap 𝒫 b = F (x) \cap 𝒫 z$
69	68	iuneq2d	$⊢ b = z \to ⋃_{x \in X} (F (x) \cap 𝒫 b) = ⋃_{x \in X} (F (x) \cap 𝒫 z)$
70	66 69	syl5eq	$⊢ b = z \to ⋃_{n \in X} (F (n) \cap 𝒫 b) = ⋃_{x \in X} (F (x) \cap 𝒫 z)$
71	70	cbviunv	$⊢ ⋃_{b \in a} ⋃_{n \in X} (F (n) \cap 𝒫 b) = ⋃_{z \in a} ⋃_{x \in X} (F (x) \cap 𝒫 z)$
72	71	mpteq2i	$⊢ (a \in V ⟼ ⋃_{b \in a} ⋃_{n \in X} (F (n) \cap 𝒫 b)) = (a \in V ⟼ ⋃_{z \in a} ⋃_{x \in X} (F (x) \cap 𝒫 z))$
73		rdgeq1	$⊢ (a \in V ⟼ ⋃_{b \in a} ⋃_{n \in X} (F (n) \cap 𝒫 b)) = (a \in V ⟼ ⋃_{z \in a} ⋃_{x \in X} (F (x) \cap 𝒫 z)) \to rec ((a \in V ⟼ ⋃_{b \in a} ⋃_{n \in X} (F (n) \cap 𝒫 b)), \{s\}) = rec ((a \in V ⟼ ⋃_{z \in a} ⋃_{x \in X} (F (x) \cap 𝒫 z)), \{s\})$
74	72 73	ax-mp	$⊢ rec ((a \in V ⟼ ⋃_{b \in a} ⋃_{n \in X} (F (n) \cap 𝒫 b)), \{s\}) = rec ((a \in V ⟼ ⋃_{z \in a} ⋃_{x \in X} (F (x) \cap 𝒫 z)), \{s\})$
75	74	reseq1i	$⊢ {rec ((a \in V ⟼ ⋃_{b \in a} ⋃_{n \in X} (F (n) \cap 𝒫 b)), \{s\}) ↾}_{ω} = {rec ((a \in V ⟼ ⋃_{z \in a} ⋃_{x \in X} (F (x) \cap 𝒫 z)), \{s\}) ↾}_{ω}$
76		pweq	$⊢ g = f \to 𝒫 g = 𝒫 f$
77	76	ineq2d	$⊢ g = f \to F (w) \cap 𝒫 g = F (w) \cap 𝒫 f$
78	77	neeq1d	$⊢ g = f \to (F (w) \cap 𝒫 g \neq \emptyset \leftrightarrow F (w) \cap 𝒫 f \neq \emptyset)$
79	78	cbvrexvw	$⊢ \exists g \in ⋃ ran ({rec ((a \in V ⟼ ⋃_{b \in a} ⋃_{n \in X} (F (n) \cap 𝒫 b)), \{s\}) ↾}_{ω}) F (w) \cap 𝒫 g \neq \emptyset \leftrightarrow \exists f \in ⋃ ran ({rec ((a \in V ⟼ ⋃_{b \in a} ⋃_{n \in X} (F (n) \cap 𝒫 b)), \{s\}) ↾}_{ω}) F (w) \cap 𝒫 f \neq \emptyset$
80		fveq2	$⊢ w = y \to F (w) = F (y)$
81	80	ineq1d	$⊢ w = y \to F (w) \cap 𝒫 f = F (y) \cap 𝒫 f$
82	81	neeq1d	$⊢ w = y \to (F (w) \cap 𝒫 f \neq \emptyset \leftrightarrow F (y) \cap 𝒫 f \neq \emptyset)$
83	82	rexbidv	$⊢ w = y \to (\exists f \in ⋃ ran ({rec ((a \in V ⟼ ⋃_{b \in a} ⋃_{n \in X} (F (n) \cap 𝒫 b)), \{s\}) ↾}_{ω}) F (w) \cap 𝒫 f \neq \emptyset \leftrightarrow \exists f \in ⋃ ran ({rec ((a \in V ⟼ ⋃_{b \in a} ⋃_{n \in X} (F (n) \cap 𝒫 b)), \{s\}) ↾}_{ω}) F (y) \cap 𝒫 f \neq \emptyset)$
84	79 83	syl5bb	$⊢ w = y \to (\exists g \in ⋃ ran ({rec ((a \in V ⟼ ⋃_{b \in a} ⋃_{n \in X} (F (n) \cap 𝒫 b)), \{s\}) ↾}_{ω}) F (w) \cap 𝒫 g \neq \emptyset \leftrightarrow \exists f \in ⋃ ran ({rec ((a \in V ⟼ ⋃_{b \in a} ⋃_{n \in X} (F (n) \cap 𝒫 b)), \{s\}) ↾}_{ω}) F (y) \cap 𝒫 f \neq \emptyset)$
85	84	cbvrabv	$⊢ \{w \in X \| \exists g \in ⋃ ran ({rec ((a \in V ⟼ ⋃_{b \in a} ⋃_{n \in X} (F (n) \cap 𝒫 b)), \{s\}) ↾}_{ω}) F (w) \cap 𝒫 g \neq \emptyset\} = \{y \in X \| \exists f \in ⋃ ran ({rec ((a \in V ⟼ ⋃_{b \in a} ⋃_{n \in X} (F (n) \cap 𝒫 b)), \{s\}) ↾}_{ω}) F (y) \cap 𝒫 f \neq \emptyset\}$
86	54 55 57 4 58 59 60 51 61 63 75 85	neibastop2lem	$⊢ ((φ \land P \in X) \land (N \subseteq X \land (s \in F (P) \land s \in 𝒫 N))) \to \exists u \in J (P \in u \land u \subseteq N)$
87	9	ad2antrr	$⊢ ((φ \land P \in X) \land (N \subseteq X \land (s \in F (P) \land s \in 𝒫 N))) \to J \in Top$
88	60 52	eleqtrd	$⊢ ((φ \land P \in X) \land (N \subseteq X \land (s \in F (P) \land s \in 𝒫 N))) \to P \in ⋃ J$
89	11	isneip	$⊢ (J \in Top \land P \in ⋃ J) \to (N \in nei (J) (\{P\}) \leftrightarrow (N \subseteq ⋃ J \land \exists u \in J (P \in u \land u \subseteq N)))$
90	87 88 89	syl2anc	$⊢ ((φ \land P \in X) \land (N \subseteq X \land (s \in F (P) \land s \in 𝒫 N))) \to (N \in nei (J) (\{P\}) \leftrightarrow (N \subseteq ⋃ J \land \exists u \in J (P \in u \land u \subseteq N)))$
91	53 86 90	mpbir2and	$⊢ ((φ \land P \in X) \land (N \subseteq X \land (s \in F (P) \land s \in 𝒫 N))) \to N \in nei (J) (\{P\})$
92	91	expr	$⊢ ((φ \land P \in X) \land N \subseteq X) \to ((s \in F (P) \land s \in 𝒫 N) \to N \in nei (J) (\{P\}))$
93	50 92	syl5bi	$⊢ ((φ \land P \in X) \land N \subseteq X) \to (s \in (F (P) \cap 𝒫 N) \to N \in nei (J) (\{P\}))$
94	93	exlimdv	$⊢ ((φ \land P \in X) \land N \subseteq X) \to (\exists s s \in (F (P) \cap 𝒫 N) \to N \in nei (J) (\{P\}))$
95	49 94	syl5bi	$⊢ ((φ \land P \in X) \land N \subseteq X) \to (F (P) \cap 𝒫 N \neq \emptyset \to N \in nei (J) (\{P\}))$
96	95	expimpd	$⊢ (φ \land P \in X) \to ((N \subseteq X \land F (P) \cap 𝒫 N \neq \emptyset) \to N \in nei (J) (\{P\}))$
97	48 96	impbid	$⊢ (φ \land P \in X) \to (N \in nei (J) (\{P\}) \leftrightarrow (N \subseteq X \land F (P) \cap 𝒫 N \neq \emptyset))$

Metamath Proof Explorer

Theorem neibastop2

Proof