This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝐴 ∈ ( unifTop ‘ 𝑈 ) ↔ ( 𝐴 ⊆ 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 utopval ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 } )
2 1 eleq2d ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝐴 ∈ ( unifTop ‘ 𝑈 ) ↔ 𝐴 ∈ { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 } ) )
3 sseq2 ⊢ ( 𝑎 = 𝐴 → ( ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 ↔ ( 𝑣 “ { 𝑥 } ) ⊆ 𝐴 ) )
4 3 rexbidv ⊢ ( 𝑎 = 𝐴 → ( ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 ↔ ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝐴 ) )
5 4 raleqbi1dv ⊢ ( 𝑎 = 𝐴 → ( ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝐴 ) )
6 5 elrab ⊢ ( 𝐴 ∈ { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 } ↔ ( 𝐴 ∈ 𝒫 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝐴 ) )
7 2 6 bitrdi ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝐴 ∈ ( unifTop ‘ 𝑈 ) ↔ ( 𝐴 ∈ 𝒫 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝐴 ) ) )
8 elex ⊢ ( 𝐴 ∈ 𝒫 𝑋 → 𝐴 ∈ V )
9 8 a1i ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝐴 ∈ 𝒫 𝑋 → 𝐴 ∈ V ) )
10 elfvex ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 ∈ V )
11 10 adantr ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝑋 ∈ V )
12 simpr ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ⊆ 𝑋 )
13 11 12 ssexd ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ∈ V )
14 13 ex ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝐴 ⊆ 𝑋 → 𝐴 ∈ V ) )
15 elpwg ⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 ⊆ 𝑋 ) )
16 15 a1i ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝐴 ∈ V → ( 𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 ⊆ 𝑋 ) ) )
17 9 14 16 pm5.21ndd ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 ⊆ 𝑋 ) )
18 17 anbi1d ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( ( 𝐴 ∈ 𝒫 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝐴 ) ↔ ( 𝐴 ⊆ 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝐴 ) ) )
19 7 18 bitrd ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝐴 ∈ ( unifTop ‘ 𝑈 ) ↔ ( 𝐴 ⊆ 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝐴 ) ) )