P. 381 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38001-38100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	blssp 38001	A ball in the subspace metric. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 5-Jan-2014.)
⊢ 𝑁 = (𝑀 ↾ (𝑆 × 𝑆))    ⇒   ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑌 ∈ 𝑆 ∧ 𝑅 ∈ ℝ+)) → (𝑌(ball‘𝑁)𝑅) = ((𝑌(ball‘𝑀)𝑅) ∩ 𝑆))
Theorem	mettrifi 38002*	Generalized triangle inequality for arbitrary finite sums. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 4-Jun-2014.)
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ 𝑋)    ⇒   ⊢ (𝜑 → ((𝐹‘𝑀)𝐷(𝐹‘𝑁)) ≤ Σ𝑘 ∈ (𝑀...(𝑁 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))))
Theorem	lmclim2 38003*	A sequence in a metric space converges to a point iff the distance between the point and the elements of the sequence converges to 0. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 5-Jun-2014.)
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝐹:ℕ⟶𝑋)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐺 = (𝑥 ∈ ℕ ↦ ((𝐹‘𝑥)𝐷𝑌))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑌 ↔ 𝐺 ⇝ 0))
Theorem	geomcau 38004*	If the distance between consecutive points in a sequence is bounded by a geometric sequence, then the sequence is Cauchy. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 5-Jun-2014.)
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝐹:ℕ⟶𝑋)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 < 1)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (𝐵↑𝑘)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (Cau‘𝐷))
Theorem	caures 38005	The restriction of a Cauchy sequence to an upper set of integers is Cauchy. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 5-Jun-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋 ↑pm ℂ))    ⇒   ⊢ (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ↾ 𝑍) ∈ (Cau‘𝐷)))
Theorem	caushft 38006*	A shifted Cauchy sequence is Cauchy. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 5-Jun-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ 𝑊 = (ℤ≥‘(𝑀 + 𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐺‘(𝑘 + 𝑁)))    &   ⊢ (𝜑 → 𝐹 ∈ (Cau‘𝐷))    &   ⊢ (𝜑 → 𝐺:𝑊⟶𝑋)    ⇒   ⊢ (𝜑 → 𝐺 ∈ (Cau‘𝐷))
21.24.6  Continuous maps and homeomorphisms
Theorem	constcncf 38007*	A constant function is a continuous function on ℂ. (Contributed by Jeff Madsen, 2-Sep-2009.) (Moved into main set.mm as cncfmptc 24873 and may be deleted by mathbox owner, JM. --MC 12-Sep-2015.) (Revised by Mario Carneiro, 12-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ 𝐴)    ⇒   ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ))
Theorem	cnres2 38008*	The restriction of a continuous function to a subset is continuous. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐹 ∈ (𝐽 Cn 𝐾) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) → (𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn (𝐾 ↾t 𝐵)))
Theorem	cnresima 38009	A continuous function is continuous onto its image. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 ∈ (𝐽 Cn (𝐾 ↾t ran 𝐹)))
Theorem	cncfres 38010*	A continuous function on complex numbers restricted to a subset. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.)
⊢ 𝐴 ⊆ ℂ    &   ⊢ 𝐵 ⊆ ℂ    &   ⊢ 𝐹 = (𝑥 ∈ ℂ ↦ 𝐶)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)    &   ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵)    &   ⊢ 𝐹 ∈ (ℂ–cn→ℂ)    &   ⊢ 𝐽 = (MetOpen‘((abs ∘ − ) ↾ (𝐴 × 𝐴)))    &   ⊢ 𝐾 = (MetOpen‘((abs ∘ − ) ↾ (𝐵 × 𝐵)))    ⇒   ⊢ 𝐺 ∈ (𝐽 Cn 𝐾)
21.24.7  Boundedness
Syntax	ctotbnd 38011	Extend class notation with the class of totally bounded metric spaces.
class TotBnd
Syntax	cbnd 38012	Extend class notation with the class of bounded metric spaces.
class Bnd
Definition	df-totbnd 38013*	Define the class of totally bounded metrics. A metric space is totally bounded iff it can be covered by a finite number of balls of any given radius. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ TotBnd = (𝑥 ∈ V ↦ {𝑚 ∈ (Met‘𝑥) ∣ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ Fin (∪ 𝑣 = 𝑥 ∧ ∀𝑏 ∈ 𝑣 ∃𝑦 ∈ 𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑))})
Theorem	istotbnd 38014*	The predicate "is a totally bounded metric space". (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑀 ∈ (TotBnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ Fin (∪ 𝑣 = 𝑋 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))))
Theorem	istotbnd2 38015*	The predicate "is a totally bounded metric space." (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑀 ∈ (Met‘𝑋) → (𝑀 ∈ (TotBnd‘𝑋) ↔ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ Fin (∪ 𝑣 = 𝑋 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))))
Theorem	istotbnd3 38016*	A metric space is totally bounded iff there is a finite ε-net for every positive ε. This differs from the definition in providing a finite set of ball centers rather than a finite set of balls. (Contributed by Mario Carneiro, 12-Sep-2015.)
⊢ (𝑀 ∈ (TotBnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋))
Theorem	totbndmet 38017	The predicate "totally bounded" implies 𝑀 is a metric space. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑀 ∈ (TotBnd‘𝑋) → 𝑀 ∈ (Met‘𝑋))
Theorem	0totbnd 38018	The metric (there is only one) on the empty set is totally bounded. (Contributed by Mario Carneiro, 16-Sep-2015.)
⊢ (𝑋 = ∅ → (𝑀 ∈ (TotBnd‘𝑋) ↔ 𝑀 ∈ (Met‘𝑋)))
Theorem	sstotbnd2 38019*	Condition for a subset of a metric space to be totally bounded. (Contributed by Mario Carneiro, 12-Sep-2015.)
⊢ 𝑁 = (𝑀 ↾ (𝑌 × 𝑌))    ⇒   ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑)))
Theorem	sstotbnd 38020*	Condition for a subset of a metric space to be totally bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
⊢ 𝑁 = (𝑀 ↾ (𝑌 × 𝑌))    ⇒   ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ Fin (𝑌 ⊆ ∪ 𝑣 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑))))
Theorem	sstotbnd3 38021*	Use a net that is not necessarily finite, but for which only finitely many balls meet the subset. (Contributed by Mario Carneiro, 14-Sep-2015.)
⊢ 𝑁 = (𝑀 ↾ (𝑌 × 𝑌))    ⇒   ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ 𝒫 𝑋(𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) ∧ {𝑥 ∈ 𝑣 ∣ ((𝑥(ball‘𝑀)𝑑) ∩ 𝑌) ≠ ∅} ∈ Fin)))
Theorem	totbndss 38022	A subset of a totally bounded metric space is totally bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.)
⊢ ((𝑀 ∈ (TotBnd‘𝑋) ∧ 𝑆 ⊆ 𝑋) → (𝑀 ↾ (𝑆 × 𝑆)) ∈ (TotBnd‘𝑆))
Theorem	equivtotbnd 38023*	If the metric 𝑀 is "strongly finer" than 𝑁 (meaning that there is a positive real constant 𝑅 such that 𝑁(𝑥, 𝑦) ≤ 𝑅 · 𝑀(𝑥, 𝑦)), then total boundedness of 𝑀 implies total boundedness of 𝑁. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then one is totally bounded iff the other is.) (Contributed by Mario Carneiro, 14-Sep-2015.)
⊢ (𝜑 → 𝑀 ∈ (TotBnd‘𝑋))    &   ⊢ (𝜑 → 𝑁 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑁𝑦) ≤ (𝑅 · (𝑥𝑀𝑦)))    ⇒   ⊢ (𝜑 → 𝑁 ∈ (TotBnd‘𝑋))
Definition	df-bnd 38024*	Define the class of bounded metrics. A metric space is bounded iff it can be covered by a single ball. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ Bnd = (𝑥 ∈ V ↦ {𝑚 ∈ (Met‘𝑥) ∣ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑥 = (𝑦(ball‘𝑚)𝑟)})
Theorem	isbnd 38025*	The predicate "is a bounded metric space". (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.)
⊢ (𝑀 ∈ (Bnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟)))
Theorem	bndmet 38026	A bounded metric space is a metric space. (Contributed by Mario Carneiro, 16-Sep-2015.)
⊢ (𝑀 ∈ (Bnd‘𝑋) → 𝑀 ∈ (Met‘𝑋))
Theorem	isbndx 38027*	A "bounded extended metric" (meaning that it satisfies the same condition as a bounded metric, but with "metric" replaced with "extended metric") is a metric and thus is bounded in the conventional sense. (Contributed by Mario Carneiro, 12-Sep-2015.)
⊢ (𝑀 ∈ (Bnd‘𝑋) ↔ (𝑀 ∈ (∞Met‘𝑋) ∧ ∀𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟)))
Theorem	isbnd2 38028*	The predicate "is a bounded metric space". Uses a single point instead of an arbitrary point in the space. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 ≠ ∅) ↔ (𝑀 ∈ (∞Met‘𝑋) ∧ ∃𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑥(ball‘𝑀)𝑟)))
Theorem	isbnd3 38029*	A metric space is bounded iff the metric function maps to some bounded real interval. (Contributed by Mario Carneiro, 13-Sep-2015.)
⊢ (𝑀 ∈ (Bnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)))
Theorem	isbnd3b 38030*	A metric space is bounded iff the metric function maps to some bounded real interval. (Contributed by Mario Carneiro, 22-Sep-2015.)
⊢ (𝑀 ∈ (Bnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑦𝑀𝑧) ≤ 𝑥))
Theorem	bndss 38031	A subset of a bounded metric space is bounded. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑆 ⊆ 𝑋) → (𝑀 ↾ (𝑆 × 𝑆)) ∈ (Bnd‘𝑆))
Theorem	blbnd 38032	A ball is bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 15-Jan-2014.)
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑌 ∈ 𝑋 ∧ 𝑅 ∈ ℝ) → (𝑀 ↾ ((𝑌(ball‘𝑀)𝑅) × (𝑌(ball‘𝑀)𝑅))) ∈ (Bnd‘(𝑌(ball‘𝑀)𝑅)))
Theorem	ssbnd 38033*	A subset of a metric space is bounded iff it is contained in a ball around 𝑃, for any 𝑃 in the larger space. (Contributed by Mario Carneiro, 14-Sep-2015.)
⊢ 𝑁 = (𝑀 ↾ (𝑌 × 𝑌))    ⇒   ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝑁 ∈ (Bnd‘𝑌) ↔ ∃𝑑 ∈ ℝ 𝑌 ⊆ (𝑃(ball‘𝑀)𝑑)))
Theorem	totbndbnd 38034	A totally bounded metric space is bounded. This theorem fails for extended metrics - a bounded extended metric is a metric, but there are totally bounded extended metrics that are not metrics (if we were to weaken istotbnd 38014 to only require that 𝑀 be an extended metric). A counterexample is the discrete extended metric (assigning distinct points distance +∞) on a finite set. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
⊢ (𝑀 ∈ (TotBnd‘𝑋) → 𝑀 ∈ (Bnd‘𝑋))
Theorem	equivbnd 38035*	If the metric 𝑀 is "strongly finer" than 𝑁 (meaning that there is a positive real constant 𝑅 such that 𝑁(𝑥, 𝑦) ≤ 𝑅 · 𝑀(𝑥, 𝑦)), then boundedness of 𝑀 implies boundedness of 𝑁. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then one is bounded iff the other is.) (Contributed by Mario Carneiro, 14-Sep-2015.)
⊢ (𝜑 → 𝑀 ∈ (Bnd‘𝑋))    &   ⊢ (𝜑 → 𝑁 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑁𝑦) ≤ (𝑅 · (𝑥𝑀𝑦)))    ⇒   ⊢ (𝜑 → 𝑁 ∈ (Bnd‘𝑋))
Theorem	bnd2lem 38036	Lemma for equivbnd2 38037 and similar theorems. (Contributed by Jeff Madsen, 16-Sep-2015.)
⊢ 𝐷 = (𝑀 ↾ (𝑌 × 𝑌))    ⇒   ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝐷 ∈ (Bnd‘𝑌)) → 𝑌 ⊆ 𝑋)
Theorem	equivbnd2 38037*	If balls are totally bounded in the metric 𝑀, then balls are totally bounded in the equivalent metric 𝑁. (Contributed by Mario Carneiro, 15-Sep-2015.)
⊢ (𝜑 → 𝑀 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝑁 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑆 ∈ ℝ+)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑁𝑦) ≤ (𝑅 · (𝑥𝑀𝑦)))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝑀𝑦) ≤ (𝑆 · (𝑥𝑁𝑦)))    &   ⊢ 𝐶 = (𝑀 ↾ (𝑌 × 𝑌))    &   ⊢ 𝐷 = (𝑁 ↾ (𝑌 × 𝑌))    &   ⊢ (𝜑 → (𝐶 ∈ (TotBnd‘𝑌) ↔ 𝐶 ∈ (Bnd‘𝑌)))    ⇒   ⊢ (𝜑 → (𝐷 ∈ (TotBnd‘𝑌) ↔ 𝐷 ∈ (Bnd‘𝑌)))
Theorem	prdsbnd 38038*	The product metric over finite index set is bounded if all the factors are bounded. (Contributed by Mario Carneiro, 13-Sep-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝑉 = (Base‘(𝑅‘𝑥))    &   ⊢ 𝐸 = ((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉))    &   ⊢ 𝐷 = (dist‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 Fn 𝐼)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (Bnd‘𝑉))    ⇒   ⊢ (𝜑 → 𝐷 ∈ (Bnd‘𝐵))
Theorem	prdstotbnd 38039*	The product metric over finite index set is totally bounded if all the factors are totally bounded. (Contributed by Mario Carneiro, 20-Sep-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝑉 = (Base‘(𝑅‘𝑥))    &   ⊢ 𝐸 = ((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉))    &   ⊢ 𝐷 = (dist‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 Fn 𝐼)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (TotBnd‘𝑉))    ⇒   ⊢ (𝜑 → 𝐷 ∈ (TotBnd‘𝐵))
Theorem	prdsbnd2 38040*	If balls are totally bounded in each factor, then balls are bounded in a metric product. (Contributed by Mario Carneiro, 16-Sep-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝑉 = (Base‘(𝑅‘𝑥))    &   ⊢ 𝐸 = ((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉))    &   ⊢ 𝐷 = (dist‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 Fn 𝐼)    &   ⊢ 𝐶 = (𝐷 ↾ (𝐴 × 𝐴))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (Met‘𝑉))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (𝑦 × 𝑦)) ∈ (TotBnd‘𝑦) ↔ (𝐸 ↾ (𝑦 × 𝑦)) ∈ (Bnd‘𝑦)))    ⇒   ⊢ (𝜑 → (𝐶 ∈ (TotBnd‘𝐴) ↔ 𝐶 ∈ (Bnd‘𝐴)))
Theorem	cntotbnd 38041	A subset of the complex numbers is totally bounded iff it is bounded. (Contributed by Mario Carneiro, 14-Sep-2015.)
⊢ 𝐷 = ((abs ∘ − ) ↾ (𝑋 × 𝑋))    ⇒   ⊢ (𝐷 ∈ (TotBnd‘𝑋) ↔ 𝐷 ∈ (Bnd‘𝑋))
Theorem	cnpwstotbnd 38042	A subset of 𝐴↑𝐼, where 𝐴 ⊆ ℂ, is totally bounded iff it is bounded. (Contributed by Mario Carneiro, 14-Sep-2015.)
⊢ 𝑌 = ((ℂfld ↾s 𝐴) ↑s 𝐼)    &   ⊢ 𝐷 = ((dist‘𝑌) ↾ (𝑋 × 𝑋))    ⇒   ⊢ ((𝐴 ⊆ ℂ ∧ 𝐼 ∈ Fin) → (𝐷 ∈ (TotBnd‘𝑋) ↔ 𝐷 ∈ (Bnd‘𝑋)))
21.24.8  Isometries
Syntax	cismty 38043	Extend class notation with the class of metric space isometries.
class Ismty
Definition	df-ismty 38044*	Define a function which takes two metric spaces and returns the set of isometries between the spaces. An isometry is a bijection which preserves distance. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ Ismty = (𝑚 ∈ ∪ ran ∞Met, 𝑛 ∈ ∪ ran ∞Met ↦ {𝑓 ∣ (𝑓:dom dom 𝑚–1-1-onto→dom dom 𝑛 ∧ ∀𝑥 ∈ dom dom 𝑚∀𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓‘𝑥)𝑛(𝑓‘𝑦)))})
Theorem	ismtyval 38045*	The set of isometries between two metric spaces. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → (𝑀 Ismty 𝑁) = {𝑓 ∣ (𝑓:𝑋–1-1-onto→𝑌 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) = ((𝑓‘𝑥)𝑁(𝑓‘𝑦)))})
Theorem	isismty 38046*	The condition "is an isometry". (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → (𝐹 ∈ (𝑀 Ismty 𝑁) ↔ (𝐹:𝑋–1-1-onto→𝑌 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) = ((𝐹‘𝑥)𝑁(𝐹‘𝑦)))))
Theorem	ismtycnv 38047	The inverse of an isometry is an isometry. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → (𝐹 ∈ (𝑀 Ismty 𝑁) → ◡𝐹 ∈ (𝑁 Ismty 𝑀)))
Theorem	ismtyima 38048	The image of a ball under an isometry is another ball. (Contributed by Jeff Madsen, 31-Jan-2014.)
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌) ∧ 𝐹 ∈ (𝑀 Ismty 𝑁)) ∧ (𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*)) → (𝐹 “ (𝑃(ball‘𝑀)𝑅)) = ((𝐹‘𝑃)(ball‘𝑁)𝑅))
Theorem	ismtyhmeolem 38049	Lemma for ismtyhmeo 38050. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.)
⊢ 𝐽 = (MetOpen‘𝑀)    &   ⊢ 𝐾 = (MetOpen‘𝑁)    &   ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑀 Ismty 𝑁))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))
Theorem	ismtyhmeo 38050	An isometry is a homeomorphism on the induced topology. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.)
⊢ 𝐽 = (MetOpen‘𝑀)    &   ⊢ 𝐾 = (MetOpen‘𝑁)    ⇒   ⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → (𝑀 Ismty 𝑁) ⊆ (𝐽Homeo𝐾))
Theorem	ismtybndlem 38051	Lemma for ismtybnd 38052. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 19-Jan-2014.)
⊢ ((𝑁 ∈ (∞Met‘𝑌) ∧ 𝐹 ∈ (𝑀 Ismty 𝑁)) → (𝑀 ∈ (Bnd‘𝑋) → 𝑁 ∈ (Bnd‘𝑌)))
Theorem	ismtybnd 38052	Isometries preserve boundedness. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 19-Jan-2014.)
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌) ∧ 𝐹 ∈ (𝑀 Ismty 𝑁)) → (𝑀 ∈ (Bnd‘𝑋) ↔ 𝑁 ∈ (Bnd‘𝑌)))
Theorem	ismtyres 38053	A restriction of an isometry is an isometry. The condition 𝐴 ⊆ 𝑋 is not necessary but makes the proof easier. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.)
⊢ 𝐵 = (𝐹 “ 𝐴)    &   ⊢ 𝑆 = (𝑀 ↾ (𝐴 × 𝐴))    &   ⊢ 𝑇 = (𝑁 ↾ (𝐵 × 𝐵))    ⇒   ⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝐹 ∈ (𝑀 Ismty 𝑁) ∧ 𝐴 ⊆ 𝑋)) → (𝐹 ↾ 𝐴) ∈ (𝑆 Ismty 𝑇))
21.24.9  Heine-Borel Theorem
Theorem	heibor1lem 38054	Lemma for heibor1 38055. A compact metric space is complete. This proof works by considering the collection cls(𝐹 “ (ℤ≥‘𝑛)) for each 𝑛 ∈ ℕ, which has the finite intersection property because any finite intersection of upper integer sets is another upper integer set, so any finite intersection of the image closures will contain (𝐹 “ (ℤ≥‘𝑚)) for some 𝑚. Thus, by compactness, the intersection contains a point 𝑦, which must then be the convergent point of 𝐹. (Contributed by Jeff Madsen, 17-Jan-2014.) (Revised by Mario Carneiro, 5-Jun-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝐹 ∈ (Cau‘𝐷))    &   ⊢ (𝜑 → 𝐹:ℕ⟶𝑋)    ⇒   ⊢ (𝜑 → 𝐹 ∈ dom (⇝𝑡‘𝐽))
Theorem	heibor1 38055	One half of heibor 38066, that does not require any Choice. A compact metric space is complete and totally bounded. We prove completeness in cmpcmet 25287 and total boundedness here, which follows trivially from the fact that the set of all 𝑟-balls is an open cover of 𝑋, so finitely many cover 𝑋. (Contributed by Jeff Madsen, 16-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐽 ∈ Comp) → (𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋)))
Theorem	heiborlem1 38056*	Lemma for heibor 38066. We work with a fixed open cover 𝑈 throughout. The set 𝐾 is the set of all subsets of 𝑋 that admit no finite subcover of 𝑈. (We wish to prove that 𝐾 is empty.) If a set 𝐶 has no finite subcover, then any finite cover of 𝐶 must contain a set that also has no finite subcover. (Contributed by Jeff Madsen, 23-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣}    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝐴 ∈ Fin ∧ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝐶 ∈ 𝐾) → ∃𝑥 ∈ 𝐴 𝐵 ∈ 𝐾)
Theorem	heiborlem2 38057*	Lemma for heibor 38066. Substitutions for the set 𝐺. (Contributed by Jeff Madsen, 23-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣}    &   ⊢ 𝐺 = {⟨𝑦, 𝑛⟩ ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)}    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐴𝐺𝐶 ↔ (𝐶 ∈ ℕ0 ∧ 𝐴 ∈ (𝐹‘𝐶) ∧ (𝐴𝐵𝐶) ∈ 𝐾))
Theorem	heiborlem3 38058*	Lemma for heibor 38066. Using countable choice ax-cc 10357, we have fixed in advance a collection of finite 2↑-𝑛 nets (𝐹‘𝑛) for 𝑋 (note that an 𝑟-net is a set of points in 𝑋 whose 𝑟 -balls cover 𝑋). The set 𝐺 is the subset of these points whose corresponding balls have no finite subcover (i.e. in the set 𝐾). If the theorem was false, then 𝑋 would be in 𝐾, and so some ball at each level would also be in 𝐾. But we can say more than this; given a ball (𝑦𝐵𝑛) on level 𝑛, since level 𝑛 + 1 covers the space and thus also (𝑦𝐵𝑛), using heiborlem1 38056 there is a ball on the next level whose intersection with (𝑦𝐵𝑛) also has no finite subcover. Now since the set 𝐺 is a countable union of finite sets, it is countable (which needs ax-cc 10357 via iunctb 10497), and so we can apply ax-cc 10357 to 𝐺 directly to get a function from 𝐺 to itself, which points from each ball in 𝐾 to a ball on the next level in 𝐾, and such that the intersection between these balls is also in 𝐾. (Contributed by Jeff Madsen, 18-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣}    &   ⊢ 𝐺 = {⟨𝑦, 𝑛⟩ ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)}    &   ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))    &   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛))    ⇒   ⊢ (𝜑 → ∃𝑔∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))
Theorem	heiborlem4 38059*	Lemma for heibor 38066. Using the function 𝑇 constructed in heiborlem3 38058, construct an infinite path in 𝐺. (Contributed by Jeff Madsen, 23-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣}    &   ⊢ 𝐺 = {⟨𝑦, 𝑛⟩ ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)}    &   ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))    &   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))    &   ⊢ (𝜑 → 𝐶𝐺0)    &   ⊢ 𝑆 = seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ0) → (𝑆‘𝐴)𝐺𝐴)
Theorem	heiborlem5 38060*	Lemma for heibor 38066. The function 𝑀 is a set of point-and-radius pairs suitable for application to caubl 25276. (Contributed by Jeff Madsen, 23-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣}    &   ⊢ 𝐺 = {⟨𝑦, 𝑛⟩ ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)}    &   ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))    &   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))    &   ⊢ (𝜑 → 𝐶𝐺0)    &   ⊢ 𝑆 = seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))    &   ⊢ 𝑀 = (𝑛 ∈ ℕ ↦ ⟨(𝑆‘𝑛), (3 / (2↑𝑛))⟩)    ⇒   ⊢ (𝜑 → 𝑀:ℕ⟶(𝑋 × ℝ+))
Theorem	heiborlem6 38061*	Lemma for heibor 38066. Since the sequence of balls connected by the function 𝑇 ensures that each ball nontrivially intersects with the next (since the empty set has a finite subcover, the intersection of any two successive balls in the sequence is nonempty), and each ball is half the size of the previous one, the distance between the centers is at most 3 / 2 times the size of the larger, and so if we expand each ball by a factor of 3 we get a nested sequence of balls. (Contributed by Jeff Madsen, 23-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣}    &   ⊢ 𝐺 = {⟨𝑦, 𝑛⟩ ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)}    &   ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))    &   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))    &   ⊢ (𝜑 → 𝐶𝐺0)    &   ⊢ 𝑆 = seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))    &   ⊢ 𝑀 = (𝑛 ∈ ℕ ↦ ⟨(𝑆‘𝑛), (3 / (2↑𝑛))⟩)    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ ℕ ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝑀‘𝑘)))
Theorem	heiborlem7 38062*	Lemma for heibor 38066. Since the sizes of the balls decrease exponentially, the sequence converges to zero. (Contributed by Jeff Madsen, 23-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣}    &   ⊢ 𝐺 = {⟨𝑦, 𝑛⟩ ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)}    &   ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))    &   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))    &   ⊢ (𝜑 → 𝐶𝐺0)    &   ⊢ 𝑆 = seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))    &   ⊢ 𝑀 = (𝑛 ∈ ℕ ↦ ⟨(𝑆‘𝑛), (3 / (2↑𝑛))⟩)    ⇒   ⊢ ∀𝑟 ∈ ℝ+ ∃𝑘 ∈ ℕ (2nd ‘(𝑀‘𝑘)) < 𝑟
Theorem	heiborlem8 38063*	Lemma for heibor 38066. The previous lemmas establish that the sequence 𝑀 is Cauchy, so using completeness we now consider the convergent point 𝑌. By assumption, 𝑈 is an open cover, so 𝑌 is an element of some 𝑍 ∈ 𝑈, and some ball centered at 𝑌 is contained in 𝑍. But the sequence contains arbitrarily small balls close to 𝑌, so some element ball(𝑀‘𝑛) of the sequence is contained in 𝑍. And finally we arrive at a contradiction, because {𝑍} is a finite subcover of 𝑈 that covers ball(𝑀‘𝑛), yet ball(𝑀‘𝑛) ∈ 𝐾. For convenience, we write this contradiction as 𝜑 → 𝜓 where 𝜑 is all the accumulated hypotheses and 𝜓 is anything at all. (Contributed by Jeff Madsen, 22-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣}    &   ⊢ 𝐺 = {⟨𝑦, 𝑛⟩ ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)}    &   ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))    &   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))    &   ⊢ (𝜑 → 𝐶𝐺0)    &   ⊢ 𝑆 = seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))    &   ⊢ 𝑀 = (𝑛 ∈ ℕ ↦ ⟨(𝑆‘𝑛), (3 / (2↑𝑛))⟩)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝐽)    &   ⊢ 𝑌 ∈ V    &   ⊢ (𝜑 → 𝑌 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    &   ⊢ (𝜑 → (1st ∘ 𝑀)(⇝𝑡‘𝐽)𝑌)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	heiborlem9 38064*	Lemma for heibor 38066. Discharge the hypotheses of heiborlem8 38063 by applying caubl 25276 to get a convergent point and adding the open cover assumption. (Contributed by Jeff Madsen, 20-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣}    &   ⊢ 𝐺 = {⟨𝑦, 𝑛⟩ ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)}    &   ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))    &   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))    &   ⊢ (𝜑 → 𝐶𝐺0)    &   ⊢ 𝑆 = seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))    &   ⊢ 𝑀 = (𝑛 ∈ ℕ ↦ ⟨(𝑆‘𝑛), (3 / (2↑𝑛))⟩)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝐽)    &   ⊢ (𝜑 → ∪ 𝑈 = 𝑋)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	heiborlem10 38065*	Lemma for heibor 38066. The last remaining piece of the proof is to find an element 𝐶 such that 𝐶𝐺0, i.e. 𝐶 is an element of (𝐹‘0) that has no finite subcover, which is true by heiborlem1 38056, since (𝐹‘0) is a finite cover of 𝑋, which has no finite subcover. Thus, the rest of the proof follows to a contradiction, and thus there must be a finite subcover of 𝑈 that covers 𝑋, i.e. 𝑋 is compact. (Contributed by Jeff Madsen, 22-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣}    &   ⊢ 𝐺 = {⟨𝑦, 𝑛⟩ ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)}    &   ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))    &   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛))    ⇒   ⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈)) → ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∪ 𝐽 = ∪ 𝑣)
Theorem	heibor 38066	Generalized Heine-Borel Theorem. A metric space is compact iff it is complete and totally bounded. See heibor1 38055 and heiborlem1 38056 for a description of the proof. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 28-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐽 ∈ Comp) ↔ (𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋)))
21.24.10  Banach Fixed Point Theorem
Theorem	bfplem1 38067*	Lemma for bfp 38069. The sequence 𝐺, which simply starts from any point in the space and iterates 𝐹, satisfies the property that the distance from 𝐺(𝑛) to 𝐺(𝑛 + 1) decreases by at least 𝐾 after each step. Thus, the total distance from any 𝐺(𝑖) to 𝐺(𝑗) is bounded by a geometric series, and the sequence is Cauchy. Therefore, it converges to a point ((⇝𝑡‘𝐽)‘𝐺) since the space is complete. (Contributed by Jeff Madsen, 17-Jun-2014.)
⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ (𝜑 → 𝑋 ≠ ∅)    &   ⊢ (𝜑 → 𝐾 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐾 < 1)    &   ⊢ (𝜑 → 𝐹:𝑋⟶𝑋)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦)))    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐺 = seq1((𝐹 ∘ 1st ), (ℕ × {𝐴}))    ⇒   ⊢ (𝜑 → 𝐺(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝐺))
Theorem	bfplem2 38068*	Lemma for bfp 38069. Using the point found in bfplem1 38067, we show that this convergent point is a fixed point of 𝐹. Since for any positive 𝑥, the sequence 𝐺 is in 𝐵(𝑥 / 2, 𝑃) for all 𝑘 ∈ (ℤ≥‘𝑗) (where 𝑃 = ((⇝𝑡‘𝐽)‘𝐺)), we have 𝐷(𝐺(𝑗 + 1), 𝐹(𝑃)) ≤ 𝐷(𝐺(𝑗), 𝑃) < 𝑥 / 2 and 𝐷(𝐺(𝑗 + 1), 𝑃) < 𝑥 / 2, so 𝐹(𝑃) is in every neighborhood of 𝑃 and 𝑃 is a fixed point of 𝐹. (Contributed by Jeff Madsen, 5-Jun-2014.)
⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ (𝜑 → 𝑋 ≠ ∅)    &   ⊢ (𝜑 → 𝐾 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐾 < 1)    &   ⊢ (𝜑 → 𝐹:𝑋⟶𝑋)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦)))    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐺 = seq1((𝐹 ∘ 1st ), (ℕ × {𝐴}))    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ 𝑋 (𝐹‘𝑧) = 𝑧)
Theorem	bfp 38069*	Banach fixed point theorem, also known as contraction mapping theorem. A contraction on a complete metric space has a unique fixed point. We show existence in the lemmas, and uniqueness here - if 𝐹 has two fixed points, then the distance between them is less than 𝐾 times itself, a contradiction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 5-Jun-2014.)
⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ (𝜑 → 𝑋 ≠ ∅)    &   ⊢ (𝜑 → 𝐾 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐾 < 1)    &   ⊢ (𝜑 → 𝐹:𝑋⟶𝑋)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦)))    ⇒   ⊢ (𝜑 → ∃!𝑧 ∈ 𝑋 (𝐹‘𝑧) = 𝑧)
21.24.11  Euclidean space
Syntax	crrn 38070	Extend class notation with the n-dimensional Euclidean space.
class ℝn
Definition	df-rrn 38071*	Define n-dimensional Euclidean space as a metric space with the standard Euclidean norm given by the quadratic mean. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ℝn = (𝑖 ∈ Fin ↦ (𝑥 ∈ (ℝ ↑m 𝑖), 𝑦 ∈ (ℝ ↑m 𝑖) ↦ (√‘Σ𝑘 ∈ 𝑖 (((𝑥‘𝑘) − (𝑦‘𝑘))↑2))))
Theorem	rrnval 38072*	The n-dimensional Euclidean space. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.)
⊢ 𝑋 = (ℝ ↑m 𝐼)    ⇒   ⊢ (𝐼 ∈ Fin → (ℝn‘𝐼) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (√‘Σ𝑘 ∈ 𝐼 (((𝑥‘𝑘) − (𝑦‘𝑘))↑2))))
Theorem	rrnmval 38073*	The value of the Euclidean metric. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.)
⊢ 𝑋 = (ℝ ↑m 𝐼)    ⇒   ⊢ ((𝐼 ∈ Fin ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹(ℝn‘𝐼)𝐺) = (√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)))
Theorem	rrnmet 38074	Euclidean space is a metric space. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 5-Jun-2014.)
⊢ 𝑋 = (ℝ ↑m 𝐼)    ⇒   ⊢ (𝐼 ∈ Fin → (ℝn‘𝐼) ∈ (Met‘𝑋))
Theorem	rrndstprj1 38075	The distance between two points in Euclidean space is greater than the distance between the projections onto one coordinate. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.)
⊢ 𝑋 = (ℝ ↑m 𝐼)    &   ⊢ 𝑀 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ (((𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼) ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ((𝐹‘𝐴)𝑀(𝐺‘𝐴)) ≤ (𝐹(ℝn‘𝐼)𝐺))
Theorem	rrndstprj2 38076*	Bound on the distance between two points in Euclidean space given bounds on the distances in each coordinate. This theorem and rrndstprj1 38075 can be used to show that the supremum norm and Euclidean norm are equivalent. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.)
⊢ 𝑋 = (ℝ ↑m 𝐼)    &   ⊢ 𝑀 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (𝐹(ℝn‘𝐼)𝐺) < (𝑅 · (√‘(♯‘𝐼))))
Theorem	rrncmslem 38077*	Lemma for rrncms 38078. (Contributed by Jeff Madsen, 6-Jun-2014.) (Revised by Mario Carneiro, 13-Sep-2015.)
⊢ 𝑋 = (ℝ ↑m 𝐼)    &   ⊢ 𝑀 = ((abs ∘ − ) ↾ (ℝ × ℝ))    &   ⊢ 𝐽 = (MetOpen‘(ℝn‘𝐼))    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐹 ∈ (Cau‘(ℝn‘𝐼)))    &   ⊢ (𝜑 → 𝐹:ℕ⟶𝑋)    &   ⊢ 𝑃 = (𝑚 ∈ 𝐼 ↦ ( ⇝ ‘(𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑚))))    ⇒   ⊢ (𝜑 → 𝐹 ∈ dom (⇝𝑡‘𝐽))
Theorem	rrncms 38078	Euclidean space is complete. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.)
⊢ 𝑋 = (ℝ ↑m 𝐼)    ⇒   ⊢ (𝐼 ∈ Fin → (ℝn‘𝐼) ∈ (CMet‘𝑋))
Theorem	repwsmet 38079	The supremum metric on ℝ↑𝐼 is a metric. (Contributed by Jeff Madsen, 15-Sep-2015.)
⊢ 𝑌 = ((ℂfld ↾s ℝ) ↑s 𝐼)    &   ⊢ 𝐷 = (dist‘𝑌)    &   ⊢ 𝑋 = (ℝ ↑m 𝐼)    ⇒   ⊢ (𝐼 ∈ Fin → 𝐷 ∈ (Met‘𝑋))
Theorem	rrnequiv 38080	The supremum metric on ℝ↑𝐼 is equivalent to the ℝn metric. (Contributed by Jeff Madsen, 15-Sep-2015.)
⊢ 𝑌 = ((ℂfld ↾s ℝ) ↑s 𝐼)    &   ⊢ 𝐷 = (dist‘𝑌)    &   ⊢ 𝑋 = (ℝ ↑m 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    ⇒   ⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ((𝐹𝐷𝐺) ≤ (𝐹(ℝn‘𝐼)𝐺) ∧ (𝐹(ℝn‘𝐼)𝐺) ≤ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺))))
Theorem	rrntotbnd 38081	A set in Euclidean space is totally bounded iff its is bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 16-Sep-2015.)
⊢ 𝑋 = (ℝ ↑m 𝐼)    &   ⊢ 𝑀 = ((ℝn‘𝐼) ↾ (𝑌 × 𝑌))    ⇒   ⊢ (𝐼 ∈ Fin → (𝑀 ∈ (TotBnd‘𝑌) ↔ 𝑀 ∈ (Bnd‘𝑌)))
Theorem	rrnheibor 38082	Heine-Borel theorem for Euclidean space. A subset of Euclidean space is compact iff it is closed and bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 22-Sep-2015.)
⊢ 𝑋 = (ℝ ↑m 𝐼)    &   ⊢ 𝑀 = ((ℝn‘𝐼) ↾ (𝑌 × 𝑌))    &   ⊢ 𝑇 = (MetOpen‘𝑀)    &   ⊢ 𝑈 = (MetOpen‘(ℝn‘𝐼))    ⇒   ⊢ ((𝐼 ∈ Fin ∧ 𝑌 ⊆ 𝑋) → (𝑇 ∈ Comp ↔ (𝑌 ∈ (Clsd‘𝑈) ∧ 𝑀 ∈ (Bnd‘𝑌))))
21.24.12  Intervals (continued)
Theorem	ismrer1 38083*	An isometry between ℝ and ℝ↑1. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 22-Sep-2015.)
⊢ 𝑅 = ((abs ∘ − ) ↾ (ℝ × ℝ))    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ({𝐴} × {𝑥}))    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐹 ∈ (𝑅 Ismty (ℝn‘{𝐴})))
Theorem	reheibor 38084	Heine-Borel theorem for real numbers. A subset of ℝ is compact iff it is closed and bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 22-Sep-2015.)
⊢ 𝑀 = ((abs ∘ − ) ↾ (𝑌 × 𝑌))    &   ⊢ 𝑇 = (MetOpen‘𝑀)    &   ⊢ 𝑈 = (topGen‘ran (,))    ⇒   ⊢ (𝑌 ⊆ ℝ → (𝑇 ∈ Comp ↔ (𝑌 ∈ (Clsd‘𝑈) ∧ 𝑀 ∈ (Bnd‘𝑌))))
Theorem	iccbnd 38085	A closed interval in ℝ is bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Sep-2015.)
⊢ 𝐽 = (𝐴[,]𝐵)    &   ⊢ 𝑀 = ((abs ∘ − ) ↾ (𝐽 × 𝐽))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑀 ∈ (Bnd‘𝐽))
Theorem	icccmpALT 38086	A closed interval in ℝ is compact. Alternate proof of icccmp 24782 using the Heine-Borel theorem heibor 38066. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Aug-2014.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐽 = (𝐴[,]𝐵)    &   ⊢ 𝑀 = ((abs ∘ − ) ↾ (𝐽 × 𝐽))    &   ⊢ 𝑇 = (MetOpen‘𝑀)    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑇 ∈ Comp)
21.24.13  Operation properties
Syntax	cass 38087	Extend class notation with a device to add associativity to internal operations.
class Ass
Definition	df-ass 38088*	A device to add associativity to various sorts of internal operations. The definition is meaningful when 𝑔 is a magma at least. (Contributed by FL, 1-Nov-2009.) (New usage is discouraged.)
⊢ Ass = {𝑔 ∣ ∀𝑥 ∈ dom dom 𝑔∀𝑦 ∈ dom dom 𝑔∀𝑧 ∈ dom dom 𝑔((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))}
Syntax	cexid 38089	Extend class notation with the class of all the internal operations with an identity element.
class ExId
Definition	df-exid 38090*	A device to add an identity element to various sorts of internal operations. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
⊢ ExId = {𝑔 ∣ ∃𝑥 ∈ dom dom 𝑔∀𝑦 ∈ dom dom 𝑔((𝑥𝑔𝑦) = 𝑦 ∧ (𝑦𝑔𝑥) = 𝑦)}
Theorem	isass 38091*	The predicate "is an associative operation". (Contributed by FL, 1-Nov-2009.) (New usage is discouraged.)
⊢ 𝑋 = dom dom 𝐺    ⇒   ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ Ass ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))))
Theorem	isexid 38092*	The predicate 𝐺 has a left and right identity element. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = dom dom 𝐺    ⇒   ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ ExId ↔ ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝑥) = 𝑦)))
21.24.14  Groups and related structures
Syntax	cmagm 38093	Extend class notation with the class of all magmas.
class Magma
Definition	df-mgmOLD 38094*	Obsolete version of df-mgm 18577 as of 3-Feb-2020. A magma is a binary internal operation. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
⊢ Magma = {𝑔 ∣ ∃𝑡 𝑔:(𝑡 × 𝑡)⟶𝑡}
Theorem	ismgmOLD 38095	Obsolete version of ismgm 18578 as of 3-Feb-2020. The predicate "is a magma". (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑋 = dom dom 𝐺    ⇒   ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ Magma ↔ 𝐺:(𝑋 × 𝑋)⟶𝑋))
Theorem	clmgmOLD 38096	Obsolete version of mgmcl 18580 as of 3-Feb-2020. Closure of a magma. (Contributed by FL, 14-Sep-2010.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑋 = dom dom 𝐺    ⇒   ⊢ ((𝐺 ∈ Magma ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) ∈ 𝑋)
Theorem	opidonOLD 38097	Obsolete version of mndpfo 18694 as of 23-Jan-2020. An operation with a left and right identity element is onto. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑋 = dom dom 𝐺    ⇒   ⊢ (𝐺 ∈ (Magma ∩ ExId ) → 𝐺:(𝑋 × 𝑋)–onto→𝑋)
Theorem	rngopidOLD 38098	Obsolete version of mndpfo 18694 as of 23-Jan-2020. Range of an operation with a left and right identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐺 ∈ (Magma ∩ ExId ) → ran 𝐺 = dom dom 𝐺)
Theorem	opidon2OLD 38099	Obsolete version of mndpfo 18694 as of 23-Jan-2020. An operation with a left and right identity element is onto. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝐺 ∈ (Magma ∩ ExId ) → 𝐺:(𝑋 × 𝑋)–onto→𝑋)
Theorem	isexid2 38100*	If 𝐺 ∈ (Magma ∩ ExId ), then it has a left and right identity element that belongs to the range of the operation. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝐺 ∈ (Magma ∩ ExId ) → ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥))