Theorem utopval

Description: The topology induced by a uniform structure U . (Contributed by Thierry Arnoux, 30-Nov-2017)

	Ref	Expression
Assertion	utopval	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 } )

Proof

Step	Hyp	Ref	Expression
1		df-utop	⊢ unifTop = ( 𝑢 ∈ ∪ ran UnifOn ↦ { 𝑎 ∈ 𝒫 dom ∪ 𝑢 ∣ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ 𝑢 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 } )
2		simpr	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → 𝑢 = 𝑈 )
3	2	unieqd	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → ∪ 𝑢 = ∪ 𝑈 )
4	3	dmeqd	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → dom ∪ 𝑢 = dom ∪ 𝑈 )
5		ustbas2	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 = dom ∪ 𝑈 )
6	5	adantr	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → 𝑋 = dom ∪ 𝑈 )
7	4 6	eqtr4d	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → dom ∪ 𝑢 = 𝑋 )
8	7	pweqd	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → 𝒫 dom ∪ 𝑢 = 𝒫 𝑋 )
9	2	rexeqdv	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → ( ∃ 𝑣 ∈ 𝑢 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 ↔ ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 ) )
10	9	ralbidv	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → ( ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ 𝑢 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 ↔ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 ) )
11	8 10	rabeqbidv	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → { 𝑎 ∈ 𝒫 dom ∪ 𝑢 ∣ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ 𝑢 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 } = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 } )
12		elrnust	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑈 ∈ ∪ ran UnifOn )
13		elfvex	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 ∈ V )
14		pwexg	⊢ ( 𝑋 ∈ V → 𝒫 𝑋 ∈ V )
15		rabexg	⊢ ( 𝒫 𝑋 ∈ V → { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 } ∈ V )
16	13 14 15	3syl	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 } ∈ V )
17	1 11 12 16	fvmptd2	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 } )