Metamath Proof Explorer

Theorem elutop

Description: Open sets in the topology induced by a 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 ∈ U v x ⊆ A

Proof

Step Hyp Ref Expression
1 utopval ⊢ U ∈ UnifOn ⁡ X → unifTop ⁡ U = a ∈ 𝒫 X | ∀ x ∈ a ∃ v ∈ U v x ⊆ a
2 1 eleq2d ⊢ U ∈ UnifOn ⁡ X → A ∈ unifTop ⁡ U ↔ A ∈ a ∈ 𝒫 X | ∀ x ∈ a ∃ v ∈ U v x ⊆ a
3 sseq2 ⊢ a = A → v x ⊆ a ↔ v x ⊆ A
4 3 rexbidv ⊢ a = A → ∃ v ∈ U v x ⊆ a ↔ ∃ v ∈ U v x ⊆ A
5 4 raleqbi1dv ⊢ a = A → ∀ x ∈ a ∃ v ∈ U v x ⊆ a ↔ ∀ x ∈ A ∃ v ∈ U v x ⊆ A
6 5 elrab ⊢ A ∈ a ∈ 𝒫 X | ∀ x ∈ a ∃ v ∈ U v x ⊆ a ↔ A ∈ 𝒫 X ∧ ∀ x ∈ A ∃ v ∈ U v x ⊆ A
7 2 6 bitrdi ⊢ U ∈ UnifOn ⁡ X → A ∈ unifTop ⁡ U ↔ A ∈ 𝒫 X ∧ ∀ x ∈ A ∃ v ∈ U v x ⊆ 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 ∈ U v x ⊆ A ↔ A ⊆ X ∧ ∀ x ∈ A ∃ v ∈ U v x ⊆ A
19 7 18 bitrd ⊢ U ∈ UnifOn ⁡ X → A ∈ unifTop ⁡ U ↔ A ⊆ X ∧ ∀ x ∈ A ∃ v ∈ U v x ⊆ A