P. 226 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22501-22600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tlmtmd 22501	A topological module is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopMnd)
Theorem	tlmtps 22502	A topological module is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopSp)
Theorem	tlmlmod 22503	A topological module is a left module. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ LMod)
Theorem	tlmtrg 22504	The scalar ring of a topological module is a topological ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ TopMod → 𝐹 ∈ TopRing)
Theorem	tlmscatps 22505	The scalar ring of a topological module is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ TopMod → 𝐹 ∈ TopSp)
Theorem	istvc 22506	A topological vector space is a topological module over a topological division ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ TopVec ↔ (𝑊 ∈ TopMod ∧ 𝐹 ∈ TopDRing))
Theorem	tvctdrg 22507	The scalar field of a topological vector space is a topological division ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ TopVec → 𝐹 ∈ TopDRing)
Theorem	cnmpt1vsca 22508*	Continuity of scalar multiplication; analogue of cnmpt12f 21981 which cannot be used directly because ·𝑠 is not a function. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝐾 = (TopOpen‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ TopMod)    &   ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐿 Cn 𝐾))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐿 Cn 𝐽))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 · 𝐵)) ∈ (𝐿 Cn 𝐽))
Theorem	cnmpt2vsca 22509*	Continuity of scalar multiplication; analogue of cnmpt22f 21990 which cannot be used directly because ·𝑠 is not a function. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝐾 = (TopOpen‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ TopMod)    &   ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝑀 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐿 ×t 𝑀) Cn 𝐾))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐿 ×t 𝑀) Cn 𝐽))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝐴 · 𝐵)) ∈ ((𝐿 ×t 𝑀) Cn 𝐽))
Theorem	tlmtgp 22510	A topological vector space is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopGrp)
Theorem	tvctlm 22511	A topological vector space is a topological module. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑊 ∈ TopVec → 𝑊 ∈ TopMod)
Theorem	tvclmod 22512	A topological vector space is a left module. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑊 ∈ TopVec → 𝑊 ∈ LMod)
Theorem	tvclvec 22513	A topological vector space is a vector space. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ (𝑊 ∈ TopVec → 𝑊 ∈ LVec)
12.3  Uniform Structures and Spaces
12.3.1  Uniform structures
Syntax	cust 22514	Extend class notation with the class function of uniform structures.
class UnifOn
Definition	df-ust 22515*	Definition of a uniform structure. Definition 1 of [BourbakiTop1] p. II.1. A uniform structure is used to give a generalization of the idea of Cauchy's sequence. This definition is analogous to TopOn. Elements of an uniform structure are called entourages. (Contributed by FL, 29-May-2014.) (Revised by Thierry Arnoux, 15-Nov-2017.)
⊢ UnifOn = (𝑥 ∈ V ↦ {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑥 × 𝑥) ∧ (𝑥 × 𝑥) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑥) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)))})
Theorem	ustfn 22516	The defined uniform structure as a function. (Contributed by Thierry Arnoux, 15-Nov-2017.)
⊢ UnifOn Fn V
Theorem	ustval 22517*	The class of all uniform structures for a base 𝑋. (Contributed by Thierry Arnoux, 15-Nov-2017.) (Revised by AV, 17-Sep-2021.)
⊢ (𝑋 ∈ 𝑉 → (UnifOn‘𝑋) = {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)))})
Theorem	isust 22518*	The predicate "𝑈 is a uniform structure with base 𝑋". (Contributed by Thierry Arnoux, 15-Nov-2017.) (Revised by AV, 17-Sep-2021.)
⊢ (𝑋 ∈ 𝑉 → (𝑈 ∈ (UnifOn‘𝑋) ↔ (𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑈 ∧ ∀𝑣 ∈ 𝑈 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈) ∧ ∀𝑤 ∈ 𝑈 (𝑣 ∩ 𝑤) ∈ 𝑈 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑈 ∧ ∃𝑤 ∈ 𝑈 (𝑤 ∘ 𝑤) ⊆ 𝑣)))))
Theorem	ustssxp 22519	Entourages are subsets of the Cartesian product of the base set. (Contributed by Thierry Arnoux, 19-Nov-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → 𝑉 ⊆ (𝑋 × 𝑋))
Theorem	ustssel 22520	A uniform structure is upward closed. Condition FI of [BourbakiTop1] p. I.36. (Contributed by Thierry Arnoux, 19-Nov-2017.) (Proof shortened by AV, 17-Sep-2021.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑊 ⊆ (𝑋 × 𝑋)) → (𝑉 ⊆ 𝑊 → 𝑊 ∈ 𝑈))
Theorem	ustbasel 22521	The full set is always an entourage. Condition FIIb of [BourbakiTop1] p. I.36. (Contributed by Thierry Arnoux, 19-Nov-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 × 𝑋) ∈ 𝑈)
Theorem	ustincl 22522	A uniform structure is closed under finite intersection. Condition FII of [BourbakiTop1] p. I.36. (Contributed by Thierry Arnoux, 30-Nov-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑊 ∈ 𝑈) → (𝑉 ∩ 𝑊) ∈ 𝑈)
Theorem	ustdiag 22523	The diagonal set is included in any entourage, i.e. any point is 𝑉 -close to itself. Condition UI of [BourbakiTop1] p. II.1. (Contributed by Thierry Arnoux, 2-Dec-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → ( I ↾ 𝑋) ⊆ 𝑉)
Theorem	ustinvel 22524	If 𝑉 is an entourage, so is its inverse. Condition UII of [BourbakiTop1] p. II.1. (Contributed by Thierry Arnoux, 2-Dec-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → ◡𝑉 ∈ 𝑈)
Theorem	ustexhalf 22525*	For each entourage 𝑉 there is an entourage 𝑤 that is "not more than half as large". Condition UIII of [BourbakiTop1] p. II.1. (Contributed by Thierry Arnoux, 2-Dec-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → ∃𝑤 ∈ 𝑈 (𝑤 ∘ 𝑤) ⊆ 𝑉)
Theorem	ustrel 22526	The elements of uniform structures, called entourages, are relations. (Contributed by Thierry Arnoux, 15-Nov-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → Rel 𝑉)
Theorem	ustfilxp 22527	A uniform structure on a nonempty base is a filter. Remark 3 of [BourbakiTop1] p. II.2. (Contributed by Thierry Arnoux, 15-Nov-2017.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → 𝑈 ∈ (Fil‘(𝑋 × 𝑋)))
Theorem	ustne0 22528	A uniform structure cannot be empty. (Contributed by Thierry Arnoux, 16-Nov-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 ≠ ∅)
Theorem	ustssco 22529	In an uniform structure, any entourage 𝑉 is a subset of its composition with itself. (Contributed by Thierry Arnoux, 5-Jan-2018.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → 𝑉 ⊆ (𝑉 ∘ 𝑉))
Theorem	ustexsym 22530*	In an uniform structure, for any entourage 𝑉, there exists a smaller symmetrical entourage. (Contributed by Thierry Arnoux, 4-Jan-2018.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → ∃𝑤 ∈ 𝑈 (◡𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑉))
Theorem	ustex2sym 22531*	In an uniform structure, for any entourage 𝑉, there exists a symmetrical entourage smaller than half 𝑉. (Contributed by Thierry Arnoux, 16-Jan-2018.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → ∃𝑤 ∈ 𝑈 (◡𝑤 = 𝑤 ∧ (𝑤 ∘ 𝑤) ⊆ 𝑉))
Theorem	ustex3sym 22532*	In an uniform structure, for any entourage 𝑉, there exists a symmetrical entourage smaller than a third of 𝑉. (Contributed by Thierry Arnoux, 16-Jan-2018.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → ∃𝑤 ∈ 𝑈 (◡𝑤 = 𝑤 ∧ (𝑤 ∘ (𝑤 ∘ 𝑤)) ⊆ 𝑉))
Theorem	ustref 22533	Any element of the base set is "near" itself, i.e. entourages are reflexive. (Contributed by Thierry Arnoux, 16-Nov-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝐴 ∈ 𝑋) → 𝐴𝑉𝐴)
Theorem	ust0 22534	The unique uniform structure of the empty set is the empty set. Remark 3 of [BourbakiTop1] p. II.2. (Contributed by Thierry Arnoux, 15-Nov-2017.)
⊢ (UnifOn‘∅) = {{∅}}
Theorem	ustn0 22535	The empty set is not an uniform structure. (Contributed by Thierry Arnoux, 3-Dec-2017.)
⊢ ¬ ∅ ∈ ∪ ran UnifOn
Theorem	ustund 22536	If two intersecting sets 𝐴 and 𝐵 are both small in 𝑉, their union is small in (𝑉↑2). Proposition 1 of [BourbakiTop1] p. II.12. This proposition actually does not require any axiom of the definition of uniform structures. (Contributed by Thierry Arnoux, 17-Nov-2017.)
⊢ (𝜑 → (𝐴 × 𝐴) ⊆ 𝑉)    &   ⊢ (𝜑 → (𝐵 × 𝐵) ⊆ 𝑉)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) ≠ ∅)    ⇒   ⊢ (𝜑 → ((𝐴 ∪ 𝐵) × (𝐴 ∪ 𝐵)) ⊆ (𝑉 ∘ 𝑉))
Theorem	ustelimasn 22537	Any point 𝐴 is near enough to itself. (Contributed by Thierry Arnoux, 18-Nov-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ (𝑉 “ {𝐴}))
Theorem	ustneism 22538	For a point 𝐴 in 𝑋, (𝑉 “ {𝐴}) is small enough in (𝑉 ∘ ◡𝑉). This proposition actually does not require any axiom of the definition of uniform structures. (Contributed by Thierry Arnoux, 18-Nov-2017.)
⊢ ((𝑉 ⊆ (𝑋 × 𝑋) ∧ 𝐴 ∈ 𝑋) → ((𝑉 “ {𝐴}) × (𝑉 “ {𝐴})) ⊆ (𝑉 ∘ ◡𝑉))
Theorem	elrnust 22539	First direction for ustbas 22542. (Contributed by Thierry Arnoux, 16-Nov-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 ∈ ∪ ran UnifOn)
Theorem	ustbas2 22540	Second direction for ustbas 22542. (Contributed by Thierry Arnoux, 16-Nov-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = dom ∪ 𝑈)
Theorem	ustuni 22541	The set union of a uniform structure is the Cartesian product of its base. (Contributed by Thierry Arnoux, 5-Dec-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∪ 𝑈 = (𝑋 × 𝑋))
Theorem	ustbas 22542	Recover the base of an uniform structure 𝑈. ∪ ran UnifOn is to UnifOn what Top is to TopOn. (Contributed by Thierry Arnoux, 16-Nov-2017.)
⊢ 𝑋 = dom ∪ 𝑈    ⇒   ⊢ (𝑈 ∈ ∪ ran UnifOn ↔ 𝑈 ∈ (UnifOn‘𝑋))
Theorem	ustimasn 22543	Lemma for ustuqtop 22561. (Contributed by Thierry Arnoux, 5-Dec-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑃 ∈ 𝑋) → (𝑉 “ {𝑃}) ⊆ 𝑋)
Theorem	trust 22544	The trace of a uniform structure 𝑈 on a subset 𝐴 is a uniform structure on 𝐴. Definition 3 of [BourbakiTop1] p. II.9. (Contributed by Thierry Arnoux, 2-Dec-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑈 ↾t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴))
12.3.2  The topology induced by an uniform structure
Syntax	cutop 22545	Extend class notation with the function inducing a topology from a uniform structure.
class unifTop
Definition	df-utop 22546*	Definition of a topology induced by a uniform structure. Definition 3 of [BourbakiTop1] p. II.4. (Contributed by Thierry Arnoux, 17-Nov-2017.)
⊢ unifTop = (𝑢 ∈ ∪ ran UnifOn ↦ {𝑎 ∈ 𝒫 dom ∪ 𝑢 ∣ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ 𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎})
Theorem	utopval 22547*	The topology induced by a uniform structure 𝑈. (Contributed by Thierry Arnoux, 30-Nov-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑎})
Theorem	elutop 22548*	Open sets in the topology induced by an uniform structure 𝑈 on 𝑋 (Contributed by Thierry Arnoux, 30-Nov-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝐴 ∈ (unifTop‘𝑈) ↔ (𝐴 ⊆ 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝐴)))
Theorem	utoptop 22549	The topology induced by a uniform structure 𝑈 is a topology. (Contributed by Thierry Arnoux, 30-Nov-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) ∈ Top)
Theorem	utopbas 22550	The base of the topology induced by a uniform structure 𝑈. (Contributed by Thierry Arnoux, 5-Dec-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = ∪ (unifTop‘𝑈))
Theorem	utoptopon 22551	Topology induced by a uniform structure 𝑈 with its base set. (Contributed by Thierry Arnoux, 5-Jan-2018.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) ∈ (TopOn‘𝑋))
Theorem	restutop 22552	Restriction of a topology induced by an uniform structure. (Contributed by Thierry Arnoux, 12-Dec-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((unifTop‘𝑈) ↾t 𝐴) ⊆ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴))))
Theorem	restutopopn 22553	The restriction of the topology induced by an uniform structure to an open set. (Contributed by Thierry Arnoux, 16-Dec-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ∈ (unifTop‘𝑈)) → ((unifTop‘𝑈) ↾t 𝐴) = (unifTop‘(𝑈 ↾t (𝐴 × 𝐴))))
Theorem	ustuqtoplem 22554*	Lemma for ustuqtop 22561. (Contributed by Thierry Arnoux, 11-Jan-2018.)
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))    ⇒   ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝐴 ∈ 𝑉) → (𝐴 ∈ (𝑁‘𝑃) ↔ ∃𝑤 ∈ 𝑈 𝐴 = (𝑤 “ {𝑃})))
Theorem	ustuqtop0 22555*	Lemma for ustuqtop 22561. (Contributed by Thierry Arnoux, 11-Jan-2018.)
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))    ⇒   ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑁:𝑋⟶𝒫 𝒫 𝑋)
Theorem	ustuqtop1 22556*	Lemma for ustuqtop 22561, similar to ssnei2 21431. (Contributed by Thierry Arnoux, 11-Jan-2018.)
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))    ⇒   ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝))
Theorem	ustuqtop2 22557*	Lemma for ustuqtop 22561. (Contributed by Thierry Arnoux, 11-Jan-2018.)
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))    ⇒   ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝))
Theorem	ustuqtop3 22558*	Lemma for ustuqtop 22561, similar to elnei 21426. (Contributed by Thierry Arnoux, 11-Jan-2018.)
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))    ⇒   ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎)
Theorem	ustuqtop4 22559*	Lemma for ustuqtop 22561. (Contributed by Thierry Arnoux, 11-Jan-2018.)
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))    ⇒   ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))
Theorem	ustuqtop5 22560*	Lemma for ustuqtop 22561. (Contributed by Thierry Arnoux, 11-Jan-2018.)
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))    ⇒   ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝))
Theorem	ustuqtop 22561*	For a given uniform structure 𝑈 on a set 𝑋, there is a unique topology 𝑗 such that the set ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) is the filter of the neighborhoods of 𝑝 for that topology. Proposition 1 of [BourbakiTop1] p. II.3. (Contributed by Thierry Arnoux, 11-Jan-2018.)
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))    ⇒   ⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∃!𝑗 ∈ (TopOn‘𝑋)∀𝑝 ∈ 𝑋 (𝑁‘𝑝) = ((nei‘𝑗)‘{𝑝}))
Theorem	utopsnneiplem 22562*	The neighborhoods of a point 𝑃 for the topology induced by an uniform space 𝑈. (Contributed by Thierry Arnoux, 11-Jan-2018.)
⊢ 𝐽 = (unifTop‘𝑈)    &   ⊢ 𝐾 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)}    &   ⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))    ⇒   ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → ((nei‘𝐽)‘{𝑃}) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})))
Theorem	utopsnneip 22563*	The neighborhoods of a point 𝑃 for the topology induced by an uniform space 𝑈. (Contributed by Thierry Arnoux, 13-Jan-2018.)
⊢ 𝐽 = (unifTop‘𝑈)    ⇒   ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → ((nei‘𝐽)‘{𝑃}) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})))
Theorem	utopsnnei 22564	Images of singletons by entourages 𝑉 are neighborhoods of those singletons. (Contributed by Thierry Arnoux, 13-Jan-2018.)
⊢ 𝐽 = (unifTop‘𝑈)    ⇒   ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑃 ∈ 𝑋) → (𝑉 “ {𝑃}) ∈ ((nei‘𝐽)‘{𝑃}))
Theorem	utop2nei 22565	For any symmetrical entourage 𝑉 and any relation 𝑀, build a neighborhood of 𝑀. First part of proposition 2 of [BourbakiTop1] p. II.4. (Contributed by Thierry Arnoux, 14-Jan-2018.)
⊢ 𝐽 = (unifTop‘𝑈)    ⇒   ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((nei‘(𝐽 ×t 𝐽))‘𝑀))
Theorem	utop3cls 22566	Relation between a topological closure and a symmetric entourage in an uniform space. Second part of proposition 2 of [BourbakiTop1] p. II.4. (Contributed by Thierry Arnoux, 17-Jan-2018.)
⊢ 𝐽 = (unifTop‘𝑈)    ⇒   ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) → ((cls‘(𝐽 ×t 𝐽))‘𝑀) ⊆ (𝑉 ∘ (𝑀 ∘ 𝑉)))
Theorem	utopreg 22567	All Hausdorff uniform spaces are regular. Proposition 3 of [BourbakiTop1] p. II.5. (Contributed by Thierry Arnoux, 16-Jan-2018.)
⊢ 𝐽 = (unifTop‘𝑈)    ⇒   ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐽 ∈ Haus) → 𝐽 ∈ Reg)
12.3.3  Uniform Spaces
Syntax	cuss 22568	Extend class notation with the Uniform Structure extractor function.
class UnifSt
Syntax	cusp 22569	Extend class notation with the class of uniform spaces.
class UnifSp
Syntax	ctus 22570	Extend class notation with the function mapping a uniform structure to a uniform space.
class toUnifSp
Definition	df-uss 22571	Define the uniform structure extractor function. Similarly with df-topn 16556 this differs from df-unif 16447 when a structure has been restricted using df-ress 16350; in this case the UnifSet component will still have a uniform set over the larger set, and this function fixes this by restricting the uniform set as well. (Contributed by Thierry Arnoux, 1-Dec-2017.)
⊢ UnifSt = (𝑓 ∈ V ↦ ((UnifSet‘𝑓) ↾t ((Base‘𝑓) × (Base‘𝑓))))
Definition	df-usp 22572	Definition of a uniform space, i.e. a base set with an uniform structure and its induced topology. Derived from definition 3 of [BourbakiTop1] p. II.4. (Contributed by Thierry Arnoux, 17-Nov-2017.)
⊢ UnifSp = {𝑓 ∣ ((UnifSt‘𝑓) ∈ (UnifOn‘(Base‘𝑓)) ∧ (TopOpen‘𝑓) = (unifTop‘(UnifSt‘𝑓)))}
Definition	df-tus 22573	Define the function mapping a uniform structure to a uniform space. (Contributed by Thierry Arnoux, 17-Nov-2017.)
⊢ toUnifSp = (𝑢 ∈ ∪ ran UnifOn ↦ ({⟨(Base‘ndx), dom ∪ 𝑢⟩, ⟨(UnifSet‘ndx), 𝑢⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑢)⟩))
Theorem	ussval 22574	The uniform structure on uniform space 𝑊. This proof uses a trick with fvprc 6494 to avoid requiring 𝑊 to be a set. (Contributed by Thierry Arnoux, 3-Dec-2017.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑈 = (UnifSet‘𝑊)    ⇒   ⊢ (𝑈 ↾t (𝐵 × 𝐵)) = (UnifSt‘𝑊)
Theorem	ussid 22575	In case the base of the UnifSt element of the uniform space is the base of its element structure, then UnifSt does not restrict it further. (Contributed by Thierry Arnoux, 4-Dec-2017.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑈 = (UnifSet‘𝑊)    ⇒   ⊢ ((𝐵 × 𝐵) = ∪ 𝑈 → 𝑈 = (UnifSt‘𝑊))
Theorem	isusp 22576	The predicate 𝑊 is a uniform space. (Contributed by Thierry Arnoux, 4-Dec-2017.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑈 = (UnifSt‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    ⇒   ⊢ (𝑊 ∈ UnifSp ↔ (𝑈 ∈ (UnifOn‘𝐵) ∧ 𝐽 = (unifTop‘𝑈)))
Theorem	ressunif 22577	UnifSet is unaffected by restriction. (Contributed by Thierry Arnoux, 7-Dec-2017.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ 𝑈 = (UnifSet‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝑈 = (UnifSet‘𝐻))
Theorem	ressuss 22578	Value of the uniform structure of a restricted space. (Contributed by Thierry Arnoux, 12-Dec-2017.)
⊢ (𝐴 ∈ 𝑉 → (UnifSt‘(𝑊 ↾s 𝐴)) = ((UnifSt‘𝑊) ↾t (𝐴 × 𝐴)))
Theorem	ressust 22579	The uniform structure of a restricted space. (Contributed by Thierry Arnoux, 22-Jan-2018.)
⊢ 𝑋 = (Base‘𝑊)    &   ⊢ 𝑇 = (UnifSt‘(𝑊 ↾s 𝐴))    ⇒   ⊢ ((𝑊 ∈ UnifSp ∧ 𝐴 ⊆ 𝑋) → 𝑇 ∈ (UnifOn‘𝐴))
Theorem	ressusp 22580	The restriction of a uniform topological space to an open set is a uniform space. (Contributed by Thierry Arnoux, 16-Dec-2017.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    ⇒   ⊢ ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝐴 ∈ 𝐽) → (𝑊 ↾s 𝐴) ∈ UnifSp)
Theorem	tusval 22581	The value of the uniform space mapping function. (Contributed by Thierry Arnoux, 5-Dec-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (toUnifSp‘𝑈) = ({⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑈)⟩))
Theorem	tuslem 22582	Lemma for tusbas 22583, tusunif 22584, and tustopn 22586. (Contributed by Thierry Arnoux, 5-Dec-2017.)
⊢ 𝐾 = (toUnifSp‘𝑈)    ⇒   ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 = (Base‘𝐾) ∧ 𝑈 = (UnifSet‘𝐾) ∧ (unifTop‘𝑈) = (TopOpen‘𝐾)))
Theorem	tusbas 22583	The base set of a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.)
⊢ 𝐾 = (toUnifSp‘𝑈)    ⇒   ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = (Base‘𝐾))
Theorem	tusunif 22584	The uniform structure of a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.)
⊢ 𝐾 = (toUnifSp‘𝑈)    ⇒   ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 = (UnifSet‘𝐾))
Theorem	tususs 22585	The uniform structure of a constructed uniform space. (Contributed by Thierry Arnoux, 15-Dec-2017.)
⊢ 𝐾 = (toUnifSp‘𝑈)    ⇒   ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 = (UnifSt‘𝐾))
Theorem	tustopn 22586	The topology induced by a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.)
⊢ 𝐾 = (toUnifSp‘𝑈)    &   ⊢ 𝐽 = (unifTop‘𝑈)    ⇒   ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐽 = (TopOpen‘𝐾))
Theorem	tususp 22587	A constructed uniform space is an uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.)
⊢ 𝐾 = (toUnifSp‘𝑈)    ⇒   ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐾 ∈ UnifSp)
Theorem	tustps 22588	A constructed uniform space is a topological space. (Contributed by Thierry Arnoux, 25-Jan-2018.)
⊢ 𝐾 = (toUnifSp‘𝑈)    ⇒   ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐾 ∈ TopSp)
Theorem	uspreg 22589	If a uniform space is Hausdorff, it is regular. Proposition 3 of [BourbakiTop1] p. II.5. (Contributed by Thierry Arnoux, 4-Jan-2018.)
⊢ 𝐽 = (TopOpen‘𝑊)    ⇒   ⊢ ((𝑊 ∈ UnifSp ∧ 𝐽 ∈ Haus) → 𝐽 ∈ Reg)
12.3.4  Uniform continuity
Syntax	cucn 22590	Extend class notation with the uniform continuity operation.
class Cnu
Definition	df-ucn 22591*	Define a function on two uniform structures which value is the set of uniformly continuous functions from the first uniform structure to the second. A function 𝑓 is uniformly continuous if, roughly speaking, it is possible to guarantee that (𝑓‘𝑥) and (𝑓‘𝑦) be as close to each other as we please by requiring only that 𝑥 and 𝑦 are sufficiently close to each other; unlike ordinary continuity, the maximum distance between (𝑓‘𝑥) and (𝑓‘𝑦) cannot depend on 𝑥 and 𝑦 themselves. This formulation is the definition 1 of [BourbakiTop1] p. II.6. (Contributed by Thierry Arnoux, 16-Nov-2017.)
⊢ Cnu = (𝑢 ∈ ∪ ran UnifOn, 𝑣 ∈ ∪ ran UnifOn ↦ {𝑓 ∈ (dom ∪ 𝑣 ↑𝑚 dom ∪ 𝑢) ∣ ∀𝑠 ∈ 𝑣 ∃𝑟 ∈ 𝑢 ∀𝑥 ∈ dom ∪ 𝑢∀𝑦 ∈ dom ∪ 𝑢(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))})
Theorem	ucnval 22592*	The set of all uniformly continuous function from uniform space 𝑈 to uniform space 𝑉. (Contributed by Thierry Arnoux, 16-Nov-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝑈 Cnu𝑉) = {𝑓 ∈ (𝑌 ↑𝑚 𝑋) ∣ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))})
Theorem	isucn 22593*	The predicate "𝐹 is a uniformly continuous function from uniform space 𝑈 to uniform space 𝑉". (Contributed by Thierry Arnoux, 16-Nov-2017.)
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)))))
Theorem	isucn2 22594*	The predicate "𝐹 is a uniformly continuous function from uniform space 𝑈 to uniform space 𝑉", expressed with filter bases for the entourages. (Contributed by Thierry Arnoux, 26-Jan-2018.)
⊢ 𝑈 = ((𝑋 × 𝑋)filGen𝑅)    &   ⊢ 𝑉 = ((𝑌 × 𝑌)filGen𝑆)    &   ⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋))    &   ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌))    &   ⊢ (𝜑 → 𝑅 ∈ (fBas‘(𝑋 × 𝑋)))    &   ⊢ (𝜑 → 𝑆 ∈ (fBas‘(𝑌 × 𝑌)))    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑠 ∈ 𝑆 ∃𝑟 ∈ 𝑅 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑠(𝐹‘𝑦)))))
Theorem	ucnimalem 22595*	Reformulate the 𝐺 function as a mapping with one variable. (Contributed by Thierry Arnoux, 19-Nov-2017.)
⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋))    &   ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑈 Cnu𝑉))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)    ⇒   ⊢ 𝐺 = (𝑝 ∈ (𝑋 × 𝑋) ↦ ⟨(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))⟩)
Theorem	ucnima 22596*	An equivalent statement of the definition of uniformly continuous function. (Contributed by Thierry Arnoux, 19-Nov-2017.)
⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋))    &   ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑈 Cnu𝑉))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)    ⇒   ⊢ (𝜑 → ∃𝑟 ∈ 𝑈 (𝐺 “ 𝑟) ⊆ 𝑊)
Theorem	ucnprima 22597*	The preimage by a uniformly continuous function 𝐹 of an entourage 𝑊 of 𝑌 is an entourage of 𝑋. Note of the definition 1 of [BourbakiTop1] p. II.6. (Contributed by Thierry Arnoux, 19-Nov-2017.)
⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋))    &   ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑈 Cnu𝑉))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)    ⇒   ⊢ (𝜑 → (◡𝐺 “ 𝑊) ∈ 𝑈)
Theorem	iducn 22598	The identity is uniformly continuous from a uniform structure to itself. Example 1 of [BourbakiTop1] p. II.6. (Contributed by Thierry Arnoux, 16-Nov-2017.)
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ( I ↾ 𝑋) ∈ (𝑈 Cnu𝑈))
Theorem	cstucnd 22599	A constant function is uniformly continuous. Deduction form. Example 1 of [BourbakiTop1] p. II.6. (Contributed by Thierry Arnoux, 16-Nov-2017.)
⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋))    &   ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑌)    ⇒   ⊢ (𝜑 → (𝑋 × {𝐴}) ∈ (𝑈 Cnu𝑉))
Theorem	ucncn 22600	Uniform continuity implies continuity. Deduction form. Proposition 1 of [BourbakiTop1] p. II.6. (Contributed by Thierry Arnoux, 30-Nov-2017.)
⊢ 𝐽 = (TopOpen‘𝑅)    &   ⊢ 𝐾 = (TopOpen‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ UnifSp)    &   ⊢ (𝜑 → 𝑆 ∈ UnifSp)    &   ⊢ (𝜑 → 𝑅 ∈ TopSp)    &   ⊢ (𝜑 → 𝑆 ∈ TopSp)    &   ⊢ (𝜑 → 𝐹 ∈ ((UnifSt‘𝑅) Cnu(UnifSt‘𝑆)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))