Metamath Proof Explorer


Theorem ustuqtop

Description: For a given uniform structure U on a set X , there is a unique topology j such that the set ran ( v e. U |-> ( v " { p } ) ) is the filter of the neighborhoods of p for that topology. Proposition 1 of BourbakiTop1 p. II.3. (Contributed by Thierry Arnoux, 11-Jan-2018)

Ref Expression
Hypothesis utopustuq.1 𝑁 = ( 𝑝𝑋 ↦ ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) )
Assertion ustuqtop ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∃! 𝑗 ∈ ( TopOn ‘ 𝑋 ) ∀ 𝑝𝑋 ( 𝑁𝑝 ) = ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) )

Proof

Step Hyp Ref Expression
1 utopustuq.1 𝑁 = ( 𝑝𝑋 ↦ ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) )
2 fveq2 ( 𝑝 = 𝑟 → ( 𝑁𝑝 ) = ( 𝑁𝑟 ) )
3 2 eleq2d ( 𝑝 = 𝑟 → ( 𝑐 ∈ ( 𝑁𝑝 ) ↔ 𝑐 ∈ ( 𝑁𝑟 ) ) )
4 3 cbvralvw ( ∀ 𝑝𝑐 𝑐 ∈ ( 𝑁𝑝 ) ↔ ∀ 𝑟𝑐 𝑐 ∈ ( 𝑁𝑟 ) )
5 eleq1w ( 𝑐 = 𝑎 → ( 𝑐 ∈ ( 𝑁𝑝 ) ↔ 𝑎 ∈ ( 𝑁𝑝 ) ) )
6 5 raleqbi1dv ( 𝑐 = 𝑎 → ( ∀ 𝑝𝑐 𝑐 ∈ ( 𝑁𝑝 ) ↔ ∀ 𝑝𝑎 𝑎 ∈ ( 𝑁𝑝 ) ) )
7 4 6 bitr3id ( 𝑐 = 𝑎 → ( ∀ 𝑟𝑐 𝑐 ∈ ( 𝑁𝑟 ) ↔ ∀ 𝑝𝑎 𝑎 ∈ ( 𝑁𝑝 ) ) )
8 7 cbvrabv { 𝑐 ∈ 𝒫 𝑋 ∣ ∀ 𝑟𝑐 𝑐 ∈ ( 𝑁𝑟 ) } = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑝𝑎 𝑎 ∈ ( 𝑁𝑝 ) }
9 1 ustuqtop0 ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑁 : 𝑋 ⟶ 𝒫 𝒫 𝑋 )
10 1 ustuqtop1 ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑎𝑏𝑏𝑋 ) ∧ 𝑎 ∈ ( 𝑁𝑝 ) ) → 𝑏 ∈ ( 𝑁𝑝 ) )
11 1 ustuqtop2 ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) → ( fi ‘ ( 𝑁𝑝 ) ) ⊆ ( 𝑁𝑝 ) )
12 1 ustuqtop3 ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑎 ∈ ( 𝑁𝑝 ) ) → 𝑝𝑎 )
13 1 ustuqtop4 ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑎 ∈ ( 𝑁𝑝 ) ) → ∃ 𝑏 ∈ ( 𝑁𝑝 ) ∀ 𝑥𝑏 𝑎 ∈ ( 𝑁𝑥 ) )
14 1 ustuqtop5 ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) → 𝑋 ∈ ( 𝑁𝑝 ) )
15 8 9 10 11 12 13 14 neiptopreu ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∃! 𝑗 ∈ ( TopOn ‘ 𝑋 ) 𝑁 = ( 𝑝𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) )
16 9 feqmptd ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑁 = ( 𝑝𝑋 ↦ ( 𝑁𝑝 ) ) )
17 16 eqeq1d ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑁 = ( 𝑝𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ↔ ( 𝑝𝑋 ↦ ( 𝑁𝑝 ) ) = ( 𝑝𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ) )
18 fvex ( 𝑁𝑝 ) ∈ V
19 18 rgenw 𝑝𝑋 ( 𝑁𝑝 ) ∈ V
20 mpteqb ( ∀ 𝑝𝑋 ( 𝑁𝑝 ) ∈ V → ( ( 𝑝𝑋 ↦ ( 𝑁𝑝 ) ) = ( 𝑝𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ↔ ∀ 𝑝𝑋 ( 𝑁𝑝 ) = ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) )
21 19 20 ax-mp ( ( 𝑝𝑋 ↦ ( 𝑁𝑝 ) ) = ( 𝑝𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ↔ ∀ 𝑝𝑋 ( 𝑁𝑝 ) = ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) )
22 17 21 bitrdi ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑁 = ( 𝑝𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ↔ ∀ 𝑝𝑋 ( 𝑁𝑝 ) = ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) )
23 22 reubidv ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( ∃! 𝑗 ∈ ( TopOn ‘ 𝑋 ) 𝑁 = ( 𝑝𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ↔ ∃! 𝑗 ∈ ( TopOn ‘ 𝑋 ) ∀ 𝑝𝑋 ( 𝑁𝑝 ) = ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) )
24 15 23 mpbid ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∃! 𝑗 ∈ ( TopOn ‘ 𝑋 ) ∀ 𝑝𝑋 ( 𝑁𝑝 ) = ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) )