Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
neibastop1.2 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 𝒫 𝒫 𝑋 ∖ { ∅ } ) )
neibastop1.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑣 ∈ ( 𝐹 ‘ 𝑥 ) ∧ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ( 𝑣 ∩ 𝑤 ) ) ≠ ∅ )
neibastop1.4 ⊢ 𝐽 = { 𝑜 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑜 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ }
neibastop1.5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑣 ∈ ( 𝐹 ‘ 𝑥 ) ) ) → 𝑥 ∈ 𝑣 )
neibastop1.6 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑣 ∈ ( 𝐹 ‘ 𝑥 ) ) ) → ∃ 𝑡 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 ∈ 𝑡 ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑣 ) ≠ ∅ )
Assertion neibastop3 ( 𝜑 → ∃! 𝑗 ∈ ( TopOn ‘ 𝑋 ) ∀ 𝑥 ∈ 𝑋 ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } )

Proof

Step Hyp Ref Expression
1 neibastop1.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2 neibastop1.2 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 𝒫 𝒫 𝑋 ∖ { ∅ } ) )
3 neibastop1.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑣 ∈ ( 𝐹 ‘ 𝑥 ) ∧ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ( 𝑣 ∩ 𝑤 ) ) ≠ ∅ )
4 neibastop1.4 ⊢ 𝐽 = { 𝑜 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑜 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ }
5 neibastop1.5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑣 ∈ ( 𝐹 ‘ 𝑥 ) ) ) → 𝑥 ∈ 𝑣 )
6 neibastop1.6 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑣 ∈ ( 𝐹 ‘ 𝑥 ) ) ) → ∃ 𝑡 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 ∈ 𝑡 ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑣 ) ≠ ∅ )
7 1 2 3 4 neibastop1 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
8 1 2 3 4 5 6 neibastop2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↔ ( 𝑛 ⊆ 𝑋 ∧ ( ( 𝐹 ‘ 𝑧 ) ∩ 𝒫 𝑛 ) ≠ ∅ ) ) )
9 velpw ⊢ ( 𝑛 ∈ 𝒫 𝑋 ↔ 𝑛 ⊆ 𝑋 )
10 9 anbi1i ⊢ ( ( 𝑛 ∈ 𝒫 𝑋 ∧ ( ( 𝐹 ‘ 𝑧 ) ∩ 𝒫 𝑛 ) ≠ ∅ ) ↔ ( 𝑛 ⊆ 𝑋 ∧ ( ( 𝐹 ‘ 𝑧 ) ∩ 𝒫 𝑛 ) ≠ ∅ ) )
11 8 10 bitr4di ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ↔ ( 𝑛 ∈ 𝒫 𝑋 ∧ ( ( 𝐹 ‘ 𝑧 ) ∩ 𝒫 𝑛 ) ≠ ∅ ) ) )
12 11 abbi2dv ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) = { 𝑛 ∣ ( 𝑛 ∈ 𝒫 𝑋 ∧ ( ( 𝐹 ‘ 𝑧 ) ∩ 𝒫 𝑛 ) ≠ ∅ ) } )
13 df-rab ⊢ { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑧 ) ∩ 𝒫 𝑛 ) ≠ ∅ } = { 𝑛 ∣ ( 𝑛 ∈ 𝒫 𝑋 ∧ ( ( 𝐹 ‘ 𝑧 ) ∩ 𝒫 𝑛 ) ≠ ∅ ) }
14 12 13 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑧 ) ∩ 𝒫 𝑛 ) ≠ ∅ } )
15 14 ralrimiva ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑋 ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑧 ) ∩ 𝒫 𝑛 ) ≠ ∅ } )
16 sneq ⊢ ( 𝑥 = 𝑧 → { 𝑥 } = { 𝑧 } )
17 16 fveq2d ⊢ ( 𝑥 = 𝑧 → ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) = ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) )
18 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) )
19 18 ineq1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) = ( ( 𝐹 ‘ 𝑧 ) ∩ 𝒫 𝑛 ) )
20 19 neeq1d ⊢ ( 𝑥 = 𝑧 → ( ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ ↔ ( ( 𝐹 ‘ 𝑧 ) ∩ 𝒫 𝑛 ) ≠ ∅ ) )
21 20 rabbidv ⊢ ( 𝑥 = 𝑧 → { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑧 ) ∩ 𝒫 𝑛 ) ≠ ∅ } )
22 17 21 eqeq12d ⊢ ( 𝑥 = 𝑧 → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ↔ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑧 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) )
23 22 cbvralvw ⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ↔ ∀ 𝑧 ∈ 𝑋 ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑧 ) ∩ 𝒫 𝑛 ) ≠ ∅ } )
24 15 23 sylibr ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } )
25 toponuni ⊢ ( 𝑗 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝑗 )
26 eqimss2 ⊢ ( 𝑋 = ∪ 𝑗 → ∪ 𝑗 ⊆ 𝑋 )
27 25 26 syl ⊢ ( 𝑗 ∈ ( TopOn ‘ 𝑋 ) → ∪ 𝑗 ⊆ 𝑋 )
28 sspwuni ⊢ ( 𝑗 ⊆ 𝒫 𝑋 ↔ ∪ 𝑗 ⊆ 𝑋 )
29 27 28 sylibr ⊢ ( 𝑗 ∈ ( TopOn ‘ 𝑋 ) → 𝑗 ⊆ 𝒫 𝑋 )
30 29 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) → 𝑗 ⊆ 𝒫 𝑋 )
31 sseqin2 ⊢ ( 𝑗 ⊆ 𝒫 𝑋 ↔ ( 𝒫 𝑋 ∩ 𝑗 ) = 𝑗 )
32 30 31 sylib ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) → ( 𝒫 𝑋 ∩ 𝑗 ) = 𝑗 )
33 topontop ⊢ ( 𝑗 ∈ ( TopOn ‘ 𝑋 ) → 𝑗 ∈ Top )
34 33 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) ∧ 𝑜 ∈ 𝒫 𝑋 ) → 𝑗 ∈ Top )
35 eltop2 ⊢ ( 𝑗 ∈ Top → ( 𝑜 ∈ 𝑗 ↔ ∀ 𝑥 ∈ 𝑜 ∃ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑜 ) ) )
36 34 35 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) ∧ 𝑜 ∈ 𝒫 𝑋 ) → ( 𝑜 ∈ 𝑗 ↔ ∀ 𝑥 ∈ 𝑜 ∃ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑜 ) ) )
37 elpwi ⊢ ( 𝑜 ∈ 𝒫 𝑋 → 𝑜 ⊆ 𝑋 )
38 ssralv ⊢ ( 𝑜 ⊆ 𝑋 → ( ∀ 𝑥 ∈ 𝑋 ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } → ∀ 𝑥 ∈ 𝑜 ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) )
39 37 38 syl ⊢ ( 𝑜 ∈ 𝒫 𝑋 → ( ∀ 𝑥 ∈ 𝑋 ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } → ∀ 𝑥 ∈ 𝑜 ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) )
40 39 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑜 ∈ 𝒫 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } → ∀ 𝑥 ∈ 𝑜 ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) )
41 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑜 ∈ 𝒫 𝑋 ) ∧ ( 𝑥 ∈ 𝑜 ∧ ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) ) → ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } )
42 41 eleq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑜 ∈ 𝒫 𝑋 ) ∧ ( 𝑥 ∈ 𝑜 ∧ ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) ) → ( 𝑜 ∈ ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ↔ 𝑜 ∈ { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) )
43 33 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑜 ∈ 𝒫 𝑋 ) ∧ ( 𝑥 ∈ 𝑜 ∧ ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) ) → 𝑗 ∈ Top )
44 25 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) → 𝑋 = ∪ 𝑗 )
45 44 sseq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) → ( 𝑜 ⊆ 𝑋 ↔ 𝑜 ⊆ ∪ 𝑗 ) )
46 45 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑜 ⊆ 𝑋 ) → 𝑜 ⊆ ∪ 𝑗 )
47 37 46 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑜 ∈ 𝒫 𝑋 ) → 𝑜 ⊆ ∪ 𝑗 )
48 47 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑜 ∈ 𝒫 𝑋 ) ∧ 𝑥 ∈ 𝑜 ) → 𝑥 ∈ ∪ 𝑗 )
49 48 adantrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑜 ∈ 𝒫 𝑋 ) ∧ ( 𝑥 ∈ 𝑜 ∧ ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) ) → 𝑥 ∈ ∪ 𝑗 )
50 47 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑜 ∈ 𝒫 𝑋 ) ∧ ( 𝑥 ∈ 𝑜 ∧ ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) ) → 𝑜 ⊆ ∪ 𝑗 )
51 eqid ⊢ ∪ 𝑗 = ∪ 𝑗
52 51 isneip ⊢ ( ( 𝑗 ∈ Top ∧ 𝑥 ∈ ∪ 𝑗 ) → ( 𝑜 ∈ ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ↔ ( 𝑜 ⊆ ∪ 𝑗 ∧ ∃ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑜 ) ) ) )
53 52 baibd ⊢ ( ( ( 𝑗 ∈ Top ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑜 ⊆ ∪ 𝑗 ) → ( 𝑜 ∈ ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ↔ ∃ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑜 ) ) )
54 43 49 50 53 syl21anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑜 ∈ 𝒫 𝑋 ) ∧ ( 𝑥 ∈ 𝑜 ∧ ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) ) → ( 𝑜 ∈ ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ↔ ∃ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑜 ) ) )
55 pweq ⊢ ( 𝑛 = 𝑜 → 𝒫 𝑛 = 𝒫 𝑜 )
56 55 ineq2d ⊢ ( 𝑛 = 𝑜 → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) = ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) )
57 56 neeq1d ⊢ ( 𝑛 = 𝑜 → ( ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ ↔ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ ) )
58 57 elrab3 ⊢ ( 𝑜 ∈ 𝒫 𝑋 → ( 𝑜 ∈ { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ↔ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ ) )
59 58 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑜 ∈ 𝒫 𝑋 ) ∧ ( 𝑥 ∈ 𝑜 ∧ ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) ) → ( 𝑜 ∈ { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ↔ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ ) )
60 42 54 59 3bitr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑜 ∈ 𝒫 𝑋 ) ∧ ( 𝑥 ∈ 𝑜 ∧ ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) ) → ( ∃ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑜 ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ ) )
61 60 expr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑜 ∈ 𝒫 𝑋 ) ∧ 𝑥 ∈ 𝑜 ) → ( ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } → ( ∃ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑜 ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ ) ) )
62 61 ralimdva ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑜 ∈ 𝒫 𝑋 ) → ( ∀ 𝑥 ∈ 𝑜 ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } → ∀ 𝑥 ∈ 𝑜 ( ∃ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑜 ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ ) ) )
63 40 62 syld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑜 ∈ 𝒫 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } → ∀ 𝑥 ∈ 𝑜 ( ∃ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑜 ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ ) ) )
64 63 imp ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑜 ∈ 𝒫 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) → ∀ 𝑥 ∈ 𝑜 ( ∃ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑜 ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ ) )
65 64 an32s ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) ∧ 𝑜 ∈ 𝒫 𝑋 ) → ∀ 𝑥 ∈ 𝑜 ( ∃ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑜 ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ ) )
66 ralbi ⊢ ( ∀ 𝑥 ∈ 𝑜 ( ∃ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑜 ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ ) → ( ∀ 𝑥 ∈ 𝑜 ∃ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑜 ) ↔ ∀ 𝑥 ∈ 𝑜 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ ) )
67 65 66 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) ∧ 𝑜 ∈ 𝒫 𝑋 ) → ( ∀ 𝑥 ∈ 𝑜 ∃ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑜 ) ↔ ∀ 𝑥 ∈ 𝑜 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ ) )
68 36 67 bitrd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) ∧ 𝑜 ∈ 𝒫 𝑋 ) → ( 𝑜 ∈ 𝑗 ↔ ∀ 𝑥 ∈ 𝑜 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ ) )
69 68 rabbi2dva ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) → ( 𝒫 𝑋 ∩ 𝑗 ) = { 𝑜 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑜 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ } )
70 69 4 eqtr4di ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) → ( 𝒫 𝑋 ∩ 𝑗 ) = 𝐽 )
71 32 70 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) → 𝑗 = 𝐽 )
72 71 expl ⊢ ( 𝜑 → ( ( 𝑗 ∈ ( TopOn ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) → 𝑗 = 𝐽 ) )
73 72 alrimiv ⊢ ( 𝜑 → ∀ 𝑗 ( ( 𝑗 ∈ ( TopOn ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) → 𝑗 = 𝐽 ) )
74 eleq1 ⊢ ( 𝑗 = 𝐽 → ( 𝑗 ∈ ( TopOn ‘ 𝑋 ) ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) )
75 fveq2 ⊢ ( 𝑗 = 𝐽 → ( nei ‘ 𝑗 ) = ( nei ‘ 𝐽 ) )
76 75 fveq1d ⊢ ( 𝑗 = 𝐽 → ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) )
77 76 eqeq1d ⊢ ( 𝑗 = 𝐽 → ( ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ↔ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) )
78 77 ralbidv ⊢ ( 𝑗 = 𝐽 → ( ∀ 𝑥 ∈ 𝑋 ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ↔ ∀ 𝑥 ∈ 𝑋 ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) )
79 74 78 anbi12d ⊢ ( 𝑗 = 𝐽 → ( ( 𝑗 ∈ ( TopOn ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) ↔ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) ) )
80 79 eqeu ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) ∧ ∀ 𝑗 ( ( 𝑗 ∈ ( TopOn ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) → 𝑗 = 𝐽 ) ) → ∃! 𝑗 ( 𝑗 ∈ ( TopOn ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) )
81 7 7 24 73 80 syl121anc ⊢ ( 𝜑 → ∃! 𝑗 ( 𝑗 ∈ ( TopOn ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) )
82 df-reu ⊢ ( ∃! 𝑗 ∈ ( TopOn ‘ 𝑋 ) ∀ 𝑥 ∈ 𝑋 ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ↔ ∃! 𝑗 ( 𝑗 ∈ ( TopOn ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } ) )
83 81 82 sylibr ⊢ ( 𝜑 → ∃! 𝑗 ∈ ( TopOn ‘ 𝑋 ) ∀ 𝑥 ∈ 𝑋 ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = { 𝑛 ∈ 𝒫 𝑋 ∣ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑛 ) ≠ ∅ } )