neibastop3

Description: The topology generated by a neighborhood base is unique. (Contributed by Jeff Hankins, 16-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	neibastop3	$⊢ φ \to \exists! j \in TopOn (X) \forall x \in X nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \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	1 2 3 4 5 6	neibastop2	$⊢ (φ \land z \in X) \to (n \in nei (J) (\{z\}) \leftrightarrow (n \subseteq X \land F (z) \cap 𝒫 n \neq \emptyset))$
9		velpw	$⊢ n \in 𝒫 X \leftrightarrow n \subseteq X$
10	9	anbi1i	$⊢ (n \in 𝒫 X \land F (z) \cap 𝒫 n \neq \emptyset) \leftrightarrow (n \subseteq X \land F (z) \cap 𝒫 n \neq \emptyset)$
11	8 10	bitr4di	$⊢ (φ \land z \in X) \to (n \in nei (J) (\{z\}) \leftrightarrow (n \in 𝒫 X \land F (z) \cap 𝒫 n \neq \emptyset))$
12	11	eqabdv	$⊢ (φ \land z \in X) \to nei (J) (\{z\}) = \{n \| (n \in 𝒫 X \land F (z) \cap 𝒫 n \neq \emptyset)\}$
13		df-rab	$⊢ \{n \in 𝒫 X \| F (z) \cap 𝒫 n \neq \emptyset\} = \{n \| (n \in 𝒫 X \land F (z) \cap 𝒫 n \neq \emptyset)\}$
14	12 13	eqtr4di	$⊢ (φ \land z \in X) \to nei (J) (\{z\}) = \{n \in 𝒫 X \| F (z) \cap 𝒫 n \neq \emptyset\}$
15	14	ralrimiva	$⊢ φ \to \forall z \in X nei (J) (\{z\}) = \{n \in 𝒫 X \| F (z) \cap 𝒫 n \neq \emptyset\}$
16		sneq	$⊢ x = z \to \{x\} = \{z\}$
17	16	fveq2d	$⊢ x = z \to nei (J) (\{x\}) = nei (J) (\{z\})$
18		fveq2	$⊢ x = z \to F (x) = F (z)$
19	18	ineq1d	$⊢ x = z \to F (x) \cap 𝒫 n = F (z) \cap 𝒫 n$
20	19	neeq1d	$⊢ x = z \to (F (x) \cap 𝒫 n \neq \emptyset \leftrightarrow F (z) \cap 𝒫 n \neq \emptyset)$
21	20	rabbidv	$⊢ x = z \to \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\} = \{n \in 𝒫 X \| F (z) \cap 𝒫 n \neq \emptyset\}$
22	17 21	eqeq12d	$⊢ x = z \to (nei (J) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\} \leftrightarrow nei (J) (\{z\}) = \{n \in 𝒫 X \| F (z) \cap 𝒫 n \neq \emptyset\})$
23	22	cbvralvw	$⊢ \forall x \in X nei (J) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\} \leftrightarrow \forall z \in X nei (J) (\{z\}) = \{n \in 𝒫 X \| F (z) \cap 𝒫 n \neq \emptyset\}$
24	15 23	sylibr	$⊢ φ \to \forall x \in X nei (J) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\}$
25		toponuni	$⊢ j \in TopOn (X) \to X = ⋃ j$
26		eqimss2	$⊢ X = ⋃ j \to ⋃ j \subseteq X$
27	25 26	syl	$⊢ j \in TopOn (X) \to ⋃ j \subseteq X$
28		sspwuni	$⊢ j \subseteq 𝒫 X \leftrightarrow ⋃ j \subseteq X$
29	27 28	sylibr	$⊢ j \in TopOn (X) \to j \subseteq 𝒫 X$
30	29	ad2antlr	$⊢ ((φ \land j \in TopOn (X)) \land \forall x \in X nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\}) \to j \subseteq 𝒫 X$
31		sseqin2	$⊢ j \subseteq 𝒫 X \leftrightarrow 𝒫 X \cap j = j$
32	30 31	sylib	$⊢ ((φ \land j \in TopOn (X)) \land \forall x \in X nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\}) \to 𝒫 X \cap j = j$
33		topontop	$⊢ j \in TopOn (X) \to j \in Top$
34	33	ad3antlr	$⊢ (((φ \land j \in TopOn (X)) \land \forall x \in X nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\}) \land o \in 𝒫 X) \to j \in Top$
35		eltop2	$⊢ j \in Top \to (o \in j \leftrightarrow \forall x \in o \exists z \in j (x \in z \land z \subseteq o))$
36	34 35	syl	$⊢ (((φ \land j \in TopOn (X)) \land \forall x \in X nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\}) \land o \in 𝒫 X) \to (o \in j \leftrightarrow \forall x \in o \exists z \in j (x \in z \land z \subseteq o))$
37		elpwi	$⊢ o \in 𝒫 X \to o \subseteq X$
38		ssralv	$⊢ o \subseteq X \to (\forall x \in X nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\} \to \forall x \in o nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\})$
39	37 38	syl	$⊢ o \in 𝒫 X \to (\forall x \in X nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\} \to \forall x \in o nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\})$
40	39	adantl	$⊢ ((φ \land j \in TopOn (X)) \land o \in 𝒫 X) \to (\forall x \in X nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\} \to \forall x \in o nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\})$
41		simprr	$⊢ (((φ \land j \in TopOn (X)) \land o \in 𝒫 X) \land (x \in o \land nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\})) \to nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\}$
42	41	eleq2d	$⊢ (((φ \land j \in TopOn (X)) \land o \in 𝒫 X) \land (x \in o \land nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\})) \to (o \in nei (j) (\{x\}) \leftrightarrow o \in \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\})$
43	33	ad3antlr	$⊢ (((φ \land j \in TopOn (X)) \land o \in 𝒫 X) \land (x \in o \land nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\})) \to j \in Top$
44	25	adantl	$⊢ (φ \land j \in TopOn (X)) \to X = ⋃ j$
45	44	sseq2d	$⊢ (φ \land j \in TopOn (X)) \to (o \subseteq X \leftrightarrow o \subseteq ⋃ j)$
46	45	biimpa	$⊢ ((φ \land j \in TopOn (X)) \land o \subseteq X) \to o \subseteq ⋃ j$
47	37 46	sylan2	$⊢ ((φ \land j \in TopOn (X)) \land o \in 𝒫 X) \to o \subseteq ⋃ j$
48	47	sselda	$⊢ (((φ \land j \in TopOn (X)) \land o \in 𝒫 X) \land x \in o) \to x \in ⋃ j$
49	48	adantrr	$⊢ (((φ \land j \in TopOn (X)) \land o \in 𝒫 X) \land (x \in o \land nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\})) \to x \in ⋃ j$
50	47	adantr	$⊢ (((φ \land j \in TopOn (X)) \land o \in 𝒫 X) \land (x \in o \land nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\})) \to o \subseteq ⋃ j$
51		eqid	$⊢ ⋃ j = ⋃ j$
52	51	isneip	$⊢ (j \in Top \land x \in ⋃ j) \to (o \in nei (j) (\{x\}) \leftrightarrow (o \subseteq ⋃ j \land \exists z \in j (x \in z \land z \subseteq o)))$
53	52	baibd	$⊢ ((j \in Top \land x \in ⋃ j) \land o \subseteq ⋃ j) \to (o \in nei (j) (\{x\}) \leftrightarrow \exists z \in j (x \in z \land z \subseteq o))$
54	43 49 50 53	syl21anc	$⊢ (((φ \land j \in TopOn (X)) \land o \in 𝒫 X) \land (x \in o \land nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\})) \to (o \in nei (j) (\{x\}) \leftrightarrow \exists z \in j (x \in z \land z \subseteq o))$
55		pweq	$⊢ n = o \to 𝒫 n = 𝒫 o$
56	55	ineq2d	$⊢ n = o \to F (x) \cap 𝒫 n = F (x) \cap 𝒫 o$
57	56	neeq1d	$⊢ n = o \to (F (x) \cap 𝒫 n \neq \emptyset \leftrightarrow F (x) \cap 𝒫 o \neq \emptyset)$
58	57	elrab3	$⊢ o \in 𝒫 X \to (o \in \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\} \leftrightarrow F (x) \cap 𝒫 o \neq \emptyset)$
59	58	ad2antlr	$⊢ (((φ \land j \in TopOn (X)) \land o \in 𝒫 X) \land (x \in o \land nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\})) \to (o \in \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\} \leftrightarrow F (x) \cap 𝒫 o \neq \emptyset)$
60	42 54 59	3bitr3d	$⊢ (((φ \land j \in TopOn (X)) \land o \in 𝒫 X) \land (x \in o \land nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\})) \to (\exists z \in j (x \in z \land z \subseteq o) \leftrightarrow F (x) \cap 𝒫 o \neq \emptyset)$
61	60	expr	$⊢ (((φ \land j \in TopOn (X)) \land o \in 𝒫 X) \land x \in o) \to (nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\} \to (\exists z \in j (x \in z \land z \subseteq o) \leftrightarrow F (x) \cap 𝒫 o \neq \emptyset))$
62	61	ralimdva	$⊢ ((φ \land j \in TopOn (X)) \land o \in 𝒫 X) \to (\forall x \in o nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\} \to \forall x \in o (\exists z \in j (x \in z \land z \subseteq o) \leftrightarrow F (x) \cap 𝒫 o \neq \emptyset))$
63	40 62	syld	$⊢ ((φ \land j \in TopOn (X)) \land o \in 𝒫 X) \to (\forall x \in X nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\} \to \forall x \in o (\exists z \in j (x \in z \land z \subseteq o) \leftrightarrow F (x) \cap 𝒫 o \neq \emptyset))$
64	63	imp	$⊢ (((φ \land j \in TopOn (X)) \land o \in 𝒫 X) \land \forall x \in X nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\}) \to \forall x \in o (\exists z \in j (x \in z \land z \subseteq o) \leftrightarrow F (x) \cap 𝒫 o \neq \emptyset)$
65	64	an32s	$⊢ (((φ \land j \in TopOn (X)) \land \forall x \in X nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\}) \land o \in 𝒫 X) \to \forall x \in o (\exists z \in j (x \in z \land z \subseteq o) \leftrightarrow F (x) \cap 𝒫 o \neq \emptyset)$
66		ralbi	$⊢ \forall x \in o (\exists z \in j (x \in z \land z \subseteq o) \leftrightarrow F (x) \cap 𝒫 o \neq \emptyset) \to (\forall x \in o \exists z \in j (x \in z \land z \subseteq o) \leftrightarrow \forall x \in o F (x) \cap 𝒫 o \neq \emptyset)$
67	65 66	syl	$⊢ (((φ \land j \in TopOn (X)) \land \forall x \in X nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\}) \land o \in 𝒫 X) \to (\forall x \in o \exists z \in j (x \in z \land z \subseteq o) \leftrightarrow \forall x \in o F (x) \cap 𝒫 o \neq \emptyset)$
68	36 67	bitrd	$⊢ (((φ \land j \in TopOn (X)) \land \forall x \in X nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\}) \land o \in 𝒫 X) \to (o \in j \leftrightarrow \forall x \in o F (x) \cap 𝒫 o \neq \emptyset)$
69	68	rabbi2dva	$⊢ ((φ \land j \in TopOn (X)) \land \forall x \in X nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\}) \to 𝒫 X \cap j = \{o \in 𝒫 X \| \forall x \in o F (x) \cap 𝒫 o \neq \emptyset\}$
70	69 4	eqtr4di	$⊢ ((φ \land j \in TopOn (X)) \land \forall x \in X nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\}) \to 𝒫 X \cap j = J$
71	32 70	eqtr3d	$⊢ ((φ \land j \in TopOn (X)) \land \forall x \in X nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\}) \to j = J$
72	71	expl	$⊢ φ \to ((j \in TopOn (X) \land \forall x \in X nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\}) \to j = J)$
73	72	alrimiv	$⊢ φ \to \forall j ((j \in TopOn (X) \land \forall x \in X nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\}) \to j = J)$
74		eleq1	$⊢ j = J \to (j \in TopOn (X) \leftrightarrow J \in TopOn (X))$
75		fveq2	$⊢ j = J \to nei (j) = nei (J)$
76	75	fveq1d	$⊢ j = J \to nei (j) (\{x\}) = nei (J) (\{x\})$
77	76	eqeq1d	$⊢ j = J \to (nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\} \leftrightarrow nei (J) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\})$
78	77	ralbidv	$⊢ j = J \to (\forall x \in X nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\} \leftrightarrow \forall x \in X nei (J) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\})$
79	74 78	anbi12d	$⊢ j = J \to ((j \in TopOn (X) \land \forall x \in X nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\}) \leftrightarrow (J \in TopOn (X) \land \forall x \in X nei (J) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\}))$
80	79	eqeu	$⊢ (J \in TopOn (X) \land (J \in TopOn (X) \land \forall x \in X nei (J) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\}) \land \forall j ((j \in TopOn (X) \land \forall x \in X nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\}) \to j = J)) \to \exists! j (j \in TopOn (X) \land \forall x \in X nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\})$
81	7 7 24 73 80	syl121anc	$⊢ φ \to \exists! j (j \in TopOn (X) \land \forall x \in X nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\})$
82		df-reu	$⊢ \exists! j \in TopOn (X) \forall x \in X nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\} \leftrightarrow \exists! j (j \in TopOn (X) \land \forall x \in X nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\})$
83	81 82	sylibr	$⊢ φ \to \exists! j \in TopOn (X) \forall x \in X nei (j) (\{x\}) = \{n \in 𝒫 X \| F (x) \cap 𝒫 n \neq \emptyset\}$

Metamath Proof Explorer

Theorem neibastop3

Proof