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	25	sspwd	$⊢ (((φ \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$
27		sslin	$⊢ 𝒫 y \subseteq 𝒫 N \to F (P) \cap 𝒫 y \subseteq F (P) \cap 𝒫 N$
28	26 27	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$
29		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$
30		snssg	$⊢ P \in X \to (P \in y \leftrightarrow \{P\} \subseteq y)$
31	30	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)$
32	29 31	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$
33		fveq2	$⊢ x = P \to F (x) = F (P)$
34	33	ineq1d	$⊢ x = P \to F (x) \cap 𝒫 y = F (P) \cap 𝒫 y$
35	34	neeq1d	$⊢ x = P \to (F (x) \cap 𝒫 y \neq \emptyset \leftrightarrow F (P) \cap 𝒫 y \neq \emptyset)$
36	35	rspcv	$⊢ P \in y \to (\forall x \in y F (x) \cap 𝒫 y \neq \emptyset \to F (P) \cap 𝒫 y \neq \emptyset)$
37	32 36	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)$
38		ssn0	$⊢ (F (P) \cap 𝒫 y \subseteq F (P) \cap 𝒫 N \land F (P) \cap 𝒫 y \neq \emptyset) \to F (P) \cap 𝒫 N \neq \emptyset$
39	28 37 38	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)$
40	39	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))$
41	40	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))$
42	41	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))$
43	24 42	biimtrid	$⊢ ((φ \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))$
44	43	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)$
45	19 44	mpd	$⊢ ((φ \land P \in X) \land N \in nei (J) (\{P\})) \to F (P) \cap 𝒫 N \neq \emptyset$
46	17 45	jca	$⊢ ((φ \land P \in X) \land N \in nei (J) (\{P\})) \to (N \subseteq X \land F (P) \cap 𝒫 N \neq \emptyset)$
47	46	ex	$⊢ (φ \land P \in X) \to (N \in nei (J) (\{P\}) \to (N \subseteq X \land F (P) \cap 𝒫 N \neq \emptyset))$
48		n0	$⊢ F (P) \cap 𝒫 N \neq \emptyset \leftrightarrow \exists s s \in (F (P) \cap 𝒫 N)$
49		elin	$⊢ s \in (F (P) \cap 𝒫 N) \leftrightarrow (s \in F (P) \land s \in 𝒫 N)$
50		simprl	$⊢ ((φ \land P \in X) \land (N \subseteq X \land (s \in F (P) \land s \in 𝒫 N))) \to N \subseteq X$
51	15	ad2antrr	$⊢ ((φ \land P \in X) \land (N \subseteq X \land (s \in F (P) \land s \in 𝒫 N))) \to X = ⋃ J$
52	50 51	sseqtrd	$⊢ ((φ \land P \in X) \land (N \subseteq X \land (s \in F (P) \land s \in 𝒫 N))) \to N \subseteq ⋃ J$
53	1	ad2antrr	$⊢ ((φ \land P \in X) \land (N \subseteq X \land (s \in F (P) \land s \in 𝒫 N))) \to X \in V$
54	2	ad2antrr	$⊢ ((φ \land P \in X) \land (N \subseteq X \land (s \in F (P) \land s \in 𝒫 N))) \to F : X ⟶ 𝒫 𝒫 X ∖ \{\emptyset\}$
55		simpll	$⊢ ((φ \land P \in X) \land (N \subseteq X \land (s \in F (P) \land s \in 𝒫 N))) \to φ$
56	55 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$
57	55 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$
58	55 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$
59		simplr	$⊢ ((φ \land P \in X) \land (N \subseteq X \land (s \in F (P) \land s \in 𝒫 N))) \to P \in X$
60		simprrl	$⊢ ((φ \land P \in X) \land (N \subseteq X \land (s \in F (P) \land s \in 𝒫 N))) \to s \in F (P)$
61		simprrr	$⊢ ((φ \land P \in X) \land (N \subseteq X \land (s \in F (P) \land s \in 𝒫 N))) \to s \in 𝒫 N$
62	61	elpwid	$⊢ ((φ \land P \in X) \land (N \subseteq X \land (s \in F (P) \land s \in 𝒫 N))) \to s \subseteq N$
63		fveq2	$⊢ n = x \to F (n) = F (x)$
64	63	ineq1d	$⊢ n = x \to F (n) \cap 𝒫 b = F (x) \cap 𝒫 b$
65	64	cbviunv	$⊢ ⋃_{n \in X} (F (n) \cap 𝒫 b) = ⋃_{x \in X} (F (x) \cap 𝒫 b)$
66		pweq	$⊢ b = z \to 𝒫 b = 𝒫 z$
67	66	ineq2d	$⊢ b = z \to F (x) \cap 𝒫 b = F (x) \cap 𝒫 z$
68	67	iuneq2d	$⊢ b = z \to ⋃_{x \in X} (F (x) \cap 𝒫 b) = ⋃_{x \in X} (F (x) \cap 𝒫 z)$
69	65 68	eqtrid	$⊢ b = z \to ⋃_{n \in X} (F (n) \cap 𝒫 b) = ⋃_{x \in X} (F (x) \cap 𝒫 z)$
70	69	cbviunv	$⊢ ⋃_{b \in a} ⋃_{n \in X} (F (n) \cap 𝒫 b) = ⋃_{z \in a} ⋃_{x \in X} (F (x) \cap 𝒫 z)$
71	70	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))$
72		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\})$
73	71 72	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\})$
74	73	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\}) ↾}_{ω}$
75		pweq	$⊢ g = f \to 𝒫 g = 𝒫 f$
76	75	ineq2d	$⊢ g = f \to F (w) \cap 𝒫 g = F (w) \cap 𝒫 f$
77	76	neeq1d	$⊢ g = f \to (F (w) \cap 𝒫 g \neq \emptyset \leftrightarrow F (w) \cap 𝒫 f \neq \emptyset)$
78	77	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$
79		fveq2	$⊢ w = y \to F (w) = F (y)$
80	79	ineq1d	$⊢ w = y \to F (w) \cap 𝒫 f = F (y) \cap 𝒫 f$
81	80	neeq1d	$⊢ w = y \to (F (w) \cap 𝒫 f \neq \emptyset \leftrightarrow F (y) \cap 𝒫 f \neq \emptyset)$
82	81	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)$
83	78 82	bitrid	$⊢ 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)$
84	83	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\}$
85	53 54 56 4 57 58 59 50 60 62 74 84	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)$
86	9	ad2antrr	$⊢ ((φ \land P \in X) \land (N \subseteq X \land (s \in F (P) \land s \in 𝒫 N))) \to J \in Top$
87	59 51	eleqtrd	$⊢ ((φ \land P \in X) \land (N \subseteq X \land (s \in F (P) \land s \in 𝒫 N))) \to P \in ⋃ J$
88	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)))$
89	86 87 88	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)))$
90	52 85 89	mpbir2and	$⊢ ((φ \land P \in X) \land (N \subseteq X \land (s \in F (P) \land s \in 𝒫 N))) \to N \in nei (J) (\{P\})$
91	90	expr	$⊢ ((φ \land P \in X) \land N \subseteq X) \to ((s \in F (P) \land s \in 𝒫 N) \to N \in nei (J) (\{P\}))$
92	49 91	biimtrid	$⊢ ((φ \land P \in X) \land N \subseteq X) \to (s \in (F (P) \cap 𝒫 N) \to N \in nei (J) (\{P\}))$
93	92	exlimdv	$⊢ ((φ \land P \in X) \land N \subseteq X) \to (\exists s s \in (F (P) \cap 𝒫 N) \to N \in nei (J) (\{P\}))$
94	48 93	biimtrid	$⊢ ((φ \land P \in X) \land N \subseteq X) \to (F (P) \cap 𝒫 N \neq \emptyset \to N \in nei (J) (\{P\}))$
95	94	expimpd	$⊢ (φ \land P \in X) \to ((N \subseteq X \land F (P) \cap 𝒫 N \neq \emptyset) \to N \in nei (J) (\{P\}))$
96	47 95	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