neiptopreu

Description: If, to each element P of a set X , we associate a set ( NP ) fulfilling Properties V_i, V_ii, V_iii and Property V_iv of BourbakiTop1 p. I.2. , corresponding to ssnei , innei , elnei and neissex , then there is a unique topology j such that for any point p , ( Np ) is the set of neighborhoods of p . Proposition 2 of BourbakiTop1 p. I.3. This can be used to build a topology from a set of neighborhoods. Note that innei uses binary intersections whereas Property V_ii mentions finite intersections (which includes the empty intersection of subsets of X , which is equal to X ), so we add the hypothesis that X is a neighborhood of all points. TODO: when df-fi includes the empty intersection, remove that extra hypothesis. (Contributed by Thierry Arnoux, 6-Jan-2018)

	Ref	Expression
Hypotheses	neiptop.o	$⊢ J = \{a \in 𝒫 X \| \forall p \in a a \in N (p)\}$
	neiptop.0	$⊢ φ \to N : X ⟶ 𝒫 𝒫 X$
	neiptop.1	$⊢ (((φ \land p \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (p)) \to b \in N (p)$
	neiptop.2	$⊢ (φ \land p \in X) \to fi (N (p)) \subseteq N (p)$
	neiptop.3	$⊢ ((φ \land p \in X) \land a \in N (p)) \to p \in a$
	neiptop.4	$⊢ ((φ \land p \in X) \land a \in N (p)) \to \exists b \in N (p) \forall q \in b a \in N (q)$
	neiptop.5	$⊢ (φ \land p \in X) \to X \in N (p)$
Assertion	neiptopreu	$⊢ φ \to \exists! j \in TopOn (X) N = (p \in X ⟼ nei (j) (\{p\}))$

Proof

Step	Hyp	Ref	Expression
1		neiptop.o	$⊢ J = \{a \in 𝒫 X \| \forall p \in a a \in N (p)\}$
2		neiptop.0	$⊢ φ \to N : X ⟶ 𝒫 𝒫 X$
3		neiptop.1	$⊢ (((φ \land p \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (p)) \to b \in N (p)$
4		neiptop.2	$⊢ (φ \land p \in X) \to fi (N (p)) \subseteq N (p)$
5		neiptop.3	$⊢ ((φ \land p \in X) \land a \in N (p)) \to p \in a$
6		neiptop.4	$⊢ ((φ \land p \in X) \land a \in N (p)) \to \exists b \in N (p) \forall q \in b a \in N (q)$
7		neiptop.5	$⊢ (φ \land p \in X) \to X \in N (p)$
8	1 2 3 4 5 6 7	neiptoptop	$⊢ φ \to J \in Top$
9		toptopon2	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$
10	8 9	sylib	$⊢ φ \to J \in TopOn (⋃ J)$
11	1 2 3 4 5 6 7	neiptopuni	$⊢ φ \to X = ⋃ J$
12	11	fveq2d	$⊢ φ \to TopOn (X) = TopOn (⋃ J)$
13	10 12	eleqtrrd	$⊢ φ \to J \in TopOn (X)$
14	1 2 3 4 5 6 7	neiptopnei	$⊢ φ \to N = (p \in X ⟼ nei (J) (\{p\}))$
15		nfv	$⊢ Ⅎ p (φ \land j \in TopOn (X))$
16		nfmpt1	$⊢ \underline{Ⅎ} p (p \in X ⟼ nei (j) (\{p\}))$
17	16	nfeq2	$⊢ Ⅎ p N = (p \in X ⟼ nei (j) (\{p\}))$
18	15 17	nfan	$⊢ Ⅎ p ((φ \land j \in TopOn (X)) \land N = (p \in X ⟼ nei (j) (\{p\})))$
19		nfv	$⊢ Ⅎ p b \subseteq X$
20	18 19	nfan	$⊢ Ⅎ p (((φ \land j \in TopOn (X)) \land N = (p \in X ⟼ nei (j) (\{p\}))) \land b \subseteq X)$
21		simpllr	$⊢ ((((φ \land j \in TopOn (X)) \land N = (p \in X ⟼ nei (j) (\{p\}))) \land b \subseteq X) \land p \in b) \to N = (p \in X ⟼ nei (j) (\{p\}))$
22		simpr	$⊢ (((φ \land j \in TopOn (X)) \land N = (p \in X ⟼ nei (j) (\{p\}))) \land b \subseteq X) \to b \subseteq X$
23	22	sselda	$⊢ ((((φ \land j \in TopOn (X)) \land N = (p \in X ⟼ nei (j) (\{p\}))) \land b \subseteq X) \land p \in b) \to p \in X$
24		id	$⊢ N = (p \in X ⟼ nei (j) (\{p\})) \to N = (p \in X ⟼ nei (j) (\{p\}))$
25		fvexd	$⊢ (N = (p \in X ⟼ nei (j) (\{p\})) \land p \in X) \to nei (j) (\{p\}) \in V$
26	24 25	fvmpt2d	$⊢ (N = (p \in X ⟼ nei (j) (\{p\})) \land p \in X) \to N (p) = nei (j) (\{p\})$
27	21 23 26	syl2anc	$⊢ ((((φ \land j \in TopOn (X)) \land N = (p \in X ⟼ nei (j) (\{p\}))) \land b \subseteq X) \land p \in b) \to N (p) = nei (j) (\{p\})$
28	27	eqcomd	$⊢ ((((φ \land j \in TopOn (X)) \land N = (p \in X ⟼ nei (j) (\{p\}))) \land b \subseteq X) \land p \in b) \to nei (j) (\{p\}) = N (p)$
29	28	eleq2d	$⊢ ((((φ \land j \in TopOn (X)) \land N = (p \in X ⟼ nei (j) (\{p\}))) \land b \subseteq X) \land p \in b) \to (b \in nei (j) (\{p\}) \leftrightarrow b \in N (p))$
30	20 29	ralbida	$⊢ (((φ \land j \in TopOn (X)) \land N = (p \in X ⟼ nei (j) (\{p\}))) \land b \subseteq X) \to (\forall p \in b b \in nei (j) (\{p\}) \leftrightarrow \forall p \in b b \in N (p))$
31	30	pm5.32da	$⊢ ((φ \land j \in TopOn (X)) \land N = (p \in X ⟼ nei (j) (\{p\}))) \to ((b \subseteq X \land \forall p \in b b \in nei (j) (\{p\})) \leftrightarrow (b \subseteq X \land \forall p \in b b \in N (p)))$
32		toponss	$⊢ (j \in TopOn (X) \land b \in j) \to b \subseteq X$
33	32	ad4ant24	$⊢ (((φ \land j \in TopOn (X)) \land N = (p \in X ⟼ nei (j) (\{p\}))) \land b \in j) \to b \subseteq X$
34		topontop	$⊢ j \in TopOn (X) \to j \in Top$
35	34	ad2antlr	$⊢ ((φ \land j \in TopOn (X)) \land N = (p \in X ⟼ nei (j) (\{p\}))) \to j \in Top$
36		opnnei	$⊢ j \in Top \to (b \in j \leftrightarrow \forall p \in b b \in nei (j) (\{p\}))$
37	35 36	syl	$⊢ ((φ \land j \in TopOn (X)) \land N = (p \in X ⟼ nei (j) (\{p\}))) \to (b \in j \leftrightarrow \forall p \in b b \in nei (j) (\{p\}))$
38	37	biimpa	$⊢ (((φ \land j \in TopOn (X)) \land N = (p \in X ⟼ nei (j) (\{p\}))) \land b \in j) \to \forall p \in b b \in nei (j) (\{p\})$
39	33 38	jca	$⊢ (((φ \land j \in TopOn (X)) \land N = (p \in X ⟼ nei (j) (\{p\}))) \land b \in j) \to (b \subseteq X \land \forall p \in b b \in nei (j) (\{p\}))$
40	37	biimpar	$⊢ (((φ \land j \in TopOn (X)) \land N = (p \in X ⟼ nei (j) (\{p\}))) \land \forall p \in b b \in nei (j) (\{p\})) \to b \in j$
41	40	adantrl	$⊢ (((φ \land j \in TopOn (X)) \land N = (p \in X ⟼ nei (j) (\{p\}))) \land (b \subseteq X \land \forall p \in b b \in nei (j) (\{p\}))) \to b \in j$
42	39 41	impbida	$⊢ ((φ \land j \in TopOn (X)) \land N = (p \in X ⟼ nei (j) (\{p\}))) \to (b \in j \leftrightarrow (b \subseteq X \land \forall p \in b b \in nei (j) (\{p\})))$
43	1	neipeltop	$⊢ b \in J \leftrightarrow (b \subseteq X \land \forall p \in b b \in N (p))$
44	43	a1i	$⊢ ((φ \land j \in TopOn (X)) \land N = (p \in X ⟼ nei (j) (\{p\}))) \to (b \in J \leftrightarrow (b \subseteq X \land \forall p \in b b \in N (p)))$
45	31 42 44	3bitr4d	$⊢ ((φ \land j \in TopOn (X)) \land N = (p \in X ⟼ nei (j) (\{p\}))) \to (b \in j \leftrightarrow b \in J)$
46	45	eqrdv	$⊢ ((φ \land j \in TopOn (X)) \land N = (p \in X ⟼ nei (j) (\{p\}))) \to j = J$
47	46	ex	$⊢ (φ \land j \in TopOn (X)) \to (N = (p \in X ⟼ nei (j) (\{p\})) \to j = J)$
48	47	ralrimiva	$⊢ φ \to \forall j \in TopOn (X) (N = (p \in X ⟼ nei (j) (\{p\})) \to j = J)$
49		simpl	$⊢ (j = J \land p \in X) \to j = J$
50	49	fveq2d	$⊢ (j = J \land p \in X) \to nei (j) = nei (J)$
51	50	fveq1d	$⊢ (j = J \land p \in X) \to nei (j) (\{p\}) = nei (J) (\{p\})$
52	51	mpteq2dva	$⊢ j = J \to (p \in X ⟼ nei (j) (\{p\})) = (p \in X ⟼ nei (J) (\{p\}))$
53	52	eqeq2d	$⊢ j = J \to (N = (p \in X ⟼ nei (j) (\{p\})) \leftrightarrow N = (p \in X ⟼ nei (J) (\{p\})))$
54	53	eqreu	$⊢ (J \in TopOn (X) \land N = (p \in X ⟼ nei (J) (\{p\})) \land \forall j \in TopOn (X) (N = (p \in X ⟼ nei (j) (\{p\})) \to j = J)) \to \exists! j \in TopOn (X) N = (p \in X ⟼ nei (j) (\{p\}))$
55	13 14 48 54	syl3anc	$⊢ φ \to \exists! j \in TopOn (X) N = (p \in X ⟼ nei (j) (\{p\}))$

Metamath Proof Explorer

Theorem neiptopreu

Proof