Metamath Proof Explorer

Theorem elutop

Description: Open sets in the topology induced by an uniform structure U on X (Contributed by Thierry Arnoux, 30-Nov-2017)

Ref Expression
Assertion elutop ⊢U∈UnifOn⁡X→A∈unifTop⁡U↔A⊆X∧∀x∈A∃v∈Uvx⊆A

Proof

Step Hyp Ref Expression
1 utopval ⊢U∈UnifOn⁡X→unifTop⁡U=a∈𝒫X|∀x∈a∃v∈Uvx⊆a
2 1 eleq2d ⊢U∈UnifOn⁡X→A∈unifTop⁡U↔A∈a∈𝒫X|∀x∈a∃v∈Uvx⊆a
3 sseq2 ⊢a=A→vx⊆a↔vx⊆A
4 3 rexbidv ⊢a=A→∃v∈Uvx⊆a↔∃v∈Uvx⊆A
5 4 raleqbi1dv ⊢a=A→∀x∈a∃v∈Uvx⊆a↔∀x∈A∃v∈Uvx⊆A
6 5 elrab ⊢A∈a∈𝒫X|∀x∈a∃v∈Uvx⊆a↔A∈𝒫X∧∀x∈A∃v∈Uvx⊆A
7 2 6 bitrdi ⊢U∈UnifOn⁡X→A∈unifTop⁡U↔A∈𝒫X∧∀x∈A∃v∈Uvx⊆A
8 elex ⊢A∈𝒫X→A∈V
9 8 a1i ⊢U∈UnifOn⁡X→A∈𝒫X→A∈V
10 elfvex ⊢U∈UnifOn⁡X→X∈V
11 10 adantr ⊢U∈UnifOn⁡X∧A⊆X→X∈V
12 simpr ⊢U∈UnifOn⁡X∧A⊆X→A⊆X
13 11 12 ssexd ⊢U∈UnifOn⁡X∧A⊆X→A∈V
14 13 ex ⊢U∈UnifOn⁡X→A⊆X→A∈V
15 elpwg ⊢A∈V→A∈𝒫X↔A⊆X
16 15 a1i ⊢U∈UnifOn⁡X→A∈V→A∈𝒫X↔A⊆X
17 9 14 16 pm5.21ndd ⊢U∈UnifOn⁡X→A∈𝒫X↔A⊆X
18 17 anbi1d ⊢U∈UnifOn⁡X→A∈𝒫X∧∀x∈A∃v∈Uvx⊆A↔A⊆X∧∀x∈A∃v∈Uvx⊆A
19 7 18 bitrd ⊢U∈UnifOn⁡X→A∈unifTop⁡U↔A⊆X∧∀x∈A∃v∈Uvx⊆A