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