Theorem utopbas

Description: The base of the topology induced by a uniform structure U . (Contributed by Thierry Arnoux, 5-Dec-2017)

	Ref	Expression
Assertion	utopbas	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 = ∪ ( unifTop ‘ 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		utopval	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 } )
2		ssrab2	⊢ { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 } ⊆ 𝒫 𝑋
3	1 2	eqsstrdi	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) ⊆ 𝒫 𝑋 )
4		ssidd	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 ⊆ 𝑋 )
5		ustssxp	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑣 ∈ 𝑈 ) → 𝑣 ⊆ ( 𝑋 × 𝑋 ) )
6		imassrn	⊢ ( 𝑣 “ { 𝑥 } ) ⊆ ran 𝑣
7		rnss	⊢ ( 𝑣 ⊆ ( 𝑋 × 𝑋 ) → ran 𝑣 ⊆ ran ( 𝑋 × 𝑋 ) )
8		rnxpid	⊢ ran ( 𝑋 × 𝑋 ) = 𝑋
9	7 8	sseqtrdi	⊢ ( 𝑣 ⊆ ( 𝑋 × 𝑋 ) → ran 𝑣 ⊆ 𝑋 )
10	6 9	sstrid	⊢ ( 𝑣 ⊆ ( 𝑋 × 𝑋 ) → ( 𝑣 “ { 𝑥 } ) ⊆ 𝑋 )
11	5 10	syl	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑣 ∈ 𝑈 ) → ( 𝑣 “ { 𝑥 } ) ⊆ 𝑋 )
12	11	ralrimiva	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∀ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑋 )
13		ustne0	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑈 ≠ ∅ )
14		r19.2zb	⊢ ( 𝑈 ≠ ∅ ↔ ( ∀ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑋 → ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑋 ) )
15	13 14	sylib	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( ∀ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑋 → ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑋 ) )
16	12 15	mpd	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑋 )
17	16	ralrimivw	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑋 )
18		elutop	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑋 ∈ ( unifTop ‘ 𝑈 ) ↔ ( 𝑋 ⊆ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑋 ) ) )
19	4 17 18	mpbir2and	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 ∈ ( unifTop ‘ 𝑈 ) )
20		elpwuni	⊢ ( 𝑋 ∈ ( unifTop ‘ 𝑈 ) → ( ( unifTop ‘ 𝑈 ) ⊆ 𝒫 𝑋 ↔ ∪ ( unifTop ‘ 𝑈 ) = 𝑋 ) )
21	19 20	syl	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( ( unifTop ‘ 𝑈 ) ⊆ 𝒫 𝑋 ↔ ∪ ( unifTop ‘ 𝑈 ) = 𝑋 ) )
22	3 21	mpbid	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∪ ( unifTop ‘ 𝑈 ) = 𝑋 )
23	22	eqcomd	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 = ∪ ( unifTop ‘ 𝑈 ) )