This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ⊢ 𝐽 = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑝 ∈ 𝑎 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) }
neiptop.0 ⊢ ( 𝜑 → 𝑁 : 𝑋 ⟶ 𝒫 𝒫 𝑋 )
neiptop.1 ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) )
neiptop.2 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) → ( fi ‘ ( 𝑁 ‘ 𝑝 ) ) ⊆ ( 𝑁 ‘ 𝑝 ) )
neiptop.3 ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑝 ∈ 𝑎 )
neiptop.4 ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ∀ 𝑞 ∈ 𝑏 𝑎 ∈ ( 𝑁 ‘ 𝑞 ) )
neiptop.5 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) → 𝑋 ∈ ( 𝑁 ‘ 𝑝 ) )
Assertion neiptopreu ( 𝜑 → ∃! 𝑗 ∈ ( TopOn ‘ 𝑋 ) 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) )

Proof

Step Hyp Ref Expression
1 neiptop.o ⊢ 𝐽 = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑝 ∈ 𝑎 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) }
2 neiptop.0 ⊢ ( 𝜑 → 𝑁 : 𝑋 ⟶ 𝒫 𝒫 𝑋 )
3 neiptop.1 ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) )
4 neiptop.2 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) → ( fi ‘ ( 𝑁 ‘ 𝑝 ) ) ⊆ ( 𝑁 ‘ 𝑝 ) )
5 neiptop.3 ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑝 ∈ 𝑎 )
6 neiptop.4 ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ∀ 𝑞 ∈ 𝑏 𝑎 ∈ ( 𝑁 ‘ 𝑞 ) )
7 neiptop.5 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑋 ) → 𝑋 ∈ ( 𝑁 ‘ 𝑝 ) )
8 1 2 3 4 5 6 7 neiptoptop ⊢ ( 𝜑 → 𝐽 ∈ Top )
9 toptopon2 ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
10 8 9 sylib ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
11 1 2 3 4 5 6 7 neiptopuni ⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
12 11 fveq2d ⊢ ( 𝜑 → ( TopOn ‘ 𝑋 ) = ( TopOn ‘ ∪ 𝐽 ) )
13 10 12 eleqtrrd ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
14 1 2 3 4 5 6 7 neiptopnei ⊢ ( 𝜑 → 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ) )
15 nfv ⊢ Ⅎ 𝑝 ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) )
16 nfmpt1 ⊢ Ⅎ 𝑝 ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) )
17 16 nfeq2 ⊢ Ⅎ 𝑝 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) )
18 15 17 nfan ⊢ Ⅎ 𝑝 ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) )
19 nfv ⊢ Ⅎ 𝑝 𝑏 ⊆ 𝑋
20 18 19 nfan ⊢ Ⅎ 𝑝 ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ) ∧ 𝑏 ⊆ 𝑋 )
21 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ) ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑝 ∈ 𝑏 ) → 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) )
22 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ) ∧ 𝑏 ⊆ 𝑋 ) → 𝑏 ⊆ 𝑋 )
23 22 sselda ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ) ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑝 ∈ 𝑏 ) → 𝑝 ∈ 𝑋 )
24 id ⊢ ( 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) → 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) )
25 fvexd ⊢ ( ( 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ∧ 𝑝 ∈ 𝑋 ) → ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ∈ V )
26 24 25 fvmpt2d ⊢ ( ( 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ∧ 𝑝 ∈ 𝑋 ) → ( 𝑁 ‘ 𝑝 ) = ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) )
27 21 23 26 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ) ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑝 ∈ 𝑏 ) → ( 𝑁 ‘ 𝑝 ) = ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) )
28 27 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ) ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑝 ∈ 𝑏 ) → ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) = ( 𝑁 ‘ 𝑝 ) )
29 28 eleq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ) ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑝 ∈ 𝑏 ) → ( 𝑏 ∈ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ↔ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) )
30 20 29 ralbida ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ) ∧ 𝑏 ⊆ 𝑋 ) → ( ∀ 𝑝 ∈ 𝑏 𝑏 ∈ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ↔ ∀ 𝑝 ∈ 𝑏 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) )
31 30 pm5.32da ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ) → ( ( 𝑏 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ 𝑏 𝑏 ∈ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ↔ ( 𝑏 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ 𝑏 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) ) )
32 toponss ⊢ ( ( 𝑗 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑏 ∈ 𝑗 ) → 𝑏 ⊆ 𝑋 )
33 32 ad4ant24 ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ) ∧ 𝑏 ∈ 𝑗 ) → 𝑏 ⊆ 𝑋 )
34 topontop ⊢ ( 𝑗 ∈ ( TopOn ‘ 𝑋 ) → 𝑗 ∈ Top )
35 34 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ) → 𝑗 ∈ Top )
36 opnnei ⊢ ( 𝑗 ∈ Top → ( 𝑏 ∈ 𝑗 ↔ ∀ 𝑝 ∈ 𝑏 𝑏 ∈ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) )
37 35 36 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ) → ( 𝑏 ∈ 𝑗 ↔ ∀ 𝑝 ∈ 𝑏 𝑏 ∈ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) )
38 37 biimpa ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ) ∧ 𝑏 ∈ 𝑗 ) → ∀ 𝑝 ∈ 𝑏 𝑏 ∈ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) )
39 33 38 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ) ∧ 𝑏 ∈ 𝑗 ) → ( 𝑏 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ 𝑏 𝑏 ∈ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) )
40 37 biimpar ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ) ∧ ∀ 𝑝 ∈ 𝑏 𝑏 ∈ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) → 𝑏 ∈ 𝑗 )
41 40 adantrl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ) ∧ ( 𝑏 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ 𝑏 𝑏 ∈ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ) → 𝑏 ∈ 𝑗 )
42 39 41 impbida ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ) → ( 𝑏 ∈ 𝑗 ↔ ( 𝑏 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ 𝑏 𝑏 ∈ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ) )
43 1 neipeltop ⊢ ( 𝑏 ∈ 𝐽 ↔ ( 𝑏 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ 𝑏 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) )
44 43 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ) → ( 𝑏 ∈ 𝐽 ↔ ( 𝑏 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ 𝑏 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) ) )
45 31 42 44 3bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ) → ( 𝑏 ∈ 𝑗 ↔ 𝑏 ∈ 𝐽 ) )
46 45 eqrdv ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ) → 𝑗 = 𝐽 )
47 46 ex ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) → ( 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) → 𝑗 = 𝐽 ) )
48 47 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ( 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) → 𝑗 = 𝐽 ) )
49 simpl ⊢ ( ( 𝑗 = 𝐽 ∧ 𝑝 ∈ 𝑋 ) → 𝑗 = 𝐽 )
50 49 fveq2d ⊢ ( ( 𝑗 = 𝐽 ∧ 𝑝 ∈ 𝑋 ) → ( nei ‘ 𝑗 ) = ( nei ‘ 𝐽 ) )
51 50 fveq1d ⊢ ( ( 𝑗 = 𝐽 ∧ 𝑝 ∈ 𝑋 ) → ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) = ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) )
52 51 mpteq2dva ⊢ ( 𝑗 = 𝐽 → ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ) )
53 52 eqeq2d ⊢ ( 𝑗 = 𝐽 → ( 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ↔ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ) ) )
54 53 eqreu ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝐽 ) ‘ { 𝑝 } ) ) ∧ ∀ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ( 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) → 𝑗 = 𝐽 ) ) → ∃! 𝑗 ∈ ( TopOn ‘ 𝑋 ) 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) )
55 13 14 48 54 syl3anc ⊢ ( 𝜑 → ∃! 𝑗 ∈ ( TopOn ‘ 𝑋 ) 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) )