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 ‘ 𝑗 ) ‘ { 𝑝 } ) )