P. 380 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37901-38000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-ablssgrp 37901	Abelian groups are groups. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ Abel ⊆ Grp
Theorem	bj-ablssgrpel 37902	Abelian groups are groups (elemental version). This is a shorter proof of ablgrp 19856. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ Abel → 𝐴 ∈ Grp)
Theorem	bj-ablsscmn 37903	Abelian groups are commutative monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ Abel ⊆ CMnd
Theorem	bj-ablsscmnel 37904	Abelian groups are commutative monoids (elemental version). This is a shorter proof of ablcmn 19858. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ Abel → 𝐴 ∈ CMnd)
Theorem	bj-modssabl 37905	(The additive groups of) modules are abelian groups. (The elemental version is lmodabl 21011; see also lmodgrp 20969 and lmodcmn 21012.) (Contributed by BJ, 9-Jun-2019.)
⊢ LMod ⊆ Abel
Theorem	bj-vecssmod 37906	Vector spaces are modules. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ LVec ⊆ LMod
Theorem	bj-vecssmodel 37907	Vector spaces are modules (elemental version). This is a shorter proof of lveclmod 21208. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ LVec → 𝐴 ∈ LMod)
21.19.7.1  Finite sums in monoids UPDATE: a similar summation is already defined as df-gsum 17496 (although it mixes finite and infinite sums, which makes it harder to understand).
Syntax	cfinsum 37908	Syntax for the class "finite summation in monoids".
class FinSum
Definition	df-bj-finsum 37909*	Finite summation in commutative monoids. This finite summation function can be extended to pairs ⟨𝑦, 𝑧⟩ where 𝑦 is a left-unital magma and 𝑧 is defined on a totally ordered set (choosing left-associative composition), or dropping unitality and requiring nonempty families, or on any monoids for families of permutable elements, etc. We use the term "summation", even though the definition stands for any unital, commutative and associative composition law. (Contributed by BJ, 9-Jun-2019.)
⊢ FinSum = (𝑥 ∈ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))} ↦ (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd ‘𝑥) ∧ 𝑠 = (seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚))))
Theorem	bj-finsumval0 37910*	Value of a finite sum. (Contributed by BJ, 9-Jun-2019.) (Proof shortened by AV, 5-May-2021.)
⊢ (𝜑 → 𝐴 ∈ CMnd)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵:𝐼⟶(Base‘𝐴))    ⇒   ⊢ (𝜑 → (𝐴 FinSum 𝐵) = (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(♯‘𝐼)))))
21.19.8  Affine, Euclidean, and Cartesian geometry A few basic theorems to start affine, Euclidean, and Cartesian geometry. The first step is to define real vector spaces, then barycentric coordinates and convex hulls.
21.19.8.1  Real vector spaces In this section, we introduce real vector spaces.
Theorem	bj-fvimacnv0 37911	Variant of fvimacnv 7050 where membership of 𝐴 in the domain is not needed provided the containing class 𝐵 does not contain the empty set. Note that this antecedent would not be needed with Definition df-afv 47840. (Contributed by BJ, 7-Jan-2024.)
⊢ ((Fun 𝐹 ∧ ¬ ∅ ∈ 𝐵) → ((𝐹‘𝐴) ∈ 𝐵 ↔ 𝐴 ∈ (◡𝐹 “ 𝐵)))
Theorem	bj-isvec 37912	The predicate "is a vector space". (Contributed by BJ, 6-Jan-2024.)
⊢ (𝜑 → 𝐾 = (Scalar‘𝑉))    ⇒   ⊢ (𝜑 → (𝑉 ∈ LVec ↔ (𝑉 ∈ LMod ∧ 𝐾 ∈ DivRing)))
Theorem	bj-fldssdrng 37913	Fields are division rings. (Contributed by BJ, 6-Jan-2024.)
⊢ Field ⊆ DivRing
Theorem	bj-flddrng 37914	Fields are division rings (elemental version). (Contributed by BJ, 9-Nov-2024.)
⊢ (𝐹 ∈ Field → 𝐹 ∈ DivRing)
Theorem	bj-rrdrg 37915	The field of real numbers is a division ring. (Contributed by BJ, 6-Jan-2024.)
⊢ ℝfld ∈ DivRing
Theorem	bj-isclm 37916	The predicate "is a subcomplex module". (Contributed by BJ, 6-Jan-2024.)
⊢ (𝜑 → 𝐹 = (Scalar‘𝑊))    &   ⊢ (𝜑 → 𝐾 = (Base‘𝐹))    ⇒   ⊢ (𝜑 → (𝑊 ∈ ℂMod ↔ (𝑊 ∈ LMod ∧ 𝐹 = (ℂfld ↾s 𝐾) ∧ 𝐾 ∈ (SubRing‘ℂfld))))
Syntax	crrvec 37917	Syntax for the class of real vector spaces.
class ℝ-Vec
Definition	df-bj-rvec 37918	Definition of the class of real vector spaces. The previous definition, ⊢ ℝ-Vec = {𝑥 ∈ LMod ∣ (Scalar‘𝑥) = ℝfld}, can be recovered using bj-isrvec 37919. The present one is preferred since it does not use any dummy variable. That ℝ-Vec could be defined with LVec in place of LMod is a consequence of bj-isrvec2 37925. (Contributed by BJ, 9-Jun-2019.)
⊢ ℝ-Vec = (LMod ∩ (◡Scalar “ {ℝfld}))
Theorem	bj-isrvec 37919	The predicate "is a real vector space". Using df-sca 17327 instead of scaid 17369 shortens the proof by two syntactic steps, but it is preferable not to rely on the precise definition df-sca 17327. (Contributed by BJ, 6-Jan-2024.)
⊢ (𝑉 ∈ ℝ-Vec ↔ (𝑉 ∈ LMod ∧ (Scalar‘𝑉) = ℝfld))
Theorem	bj-rvecmod 37920	Real vector spaces are modules (elemental version). (Contributed by BJ, 6-Jan-2024.)
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ LMod)
Theorem	bj-rvecssmod 37921	Real vector spaces are modules. (Contributed by BJ, 6-Jan-2024.)
⊢ ℝ-Vec ⊆ LMod
Theorem	bj-rvecrr 37922	The field of scalars of a real vector space is the field of real numbers. (Contributed by BJ, 6-Jan-2024.)
⊢ (𝑉 ∈ ℝ-Vec → (Scalar‘𝑉) = ℝfld)
Theorem	bj-isrvecd 37923	The predicate "is a real vector space". (Contributed by BJ, 6-Jan-2024.)
⊢ (𝜑 → (Scalar‘𝑉) = 𝐾)    ⇒   ⊢ (𝜑 → (𝑉 ∈ ℝ-Vec ↔ (𝑉 ∈ LMod ∧ 𝐾 = ℝfld)))
Theorem	bj-rvecvec 37924	Real vector spaces are vector spaces (elemental version). (Contributed by BJ, 6-Jan-2024.)
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ LVec)
Theorem	bj-isrvec2 37925	The predicate "is a real vector space". (Contributed by BJ, 6-Jan-2024.)
⊢ (𝜑 → (Scalar‘𝑉) = 𝐾)    ⇒   ⊢ (𝜑 → (𝑉 ∈ ℝ-Vec ↔ (𝑉 ∈ LVec ∧ 𝐾 = ℝfld)))
Theorem	bj-rvecssvec 37926	Real vector spaces are vector spaces. (Contributed by BJ, 6-Jan-2024.)
⊢ ℝ-Vec ⊆ LVec
Theorem	bj-rveccmod 37927	Real vector spaces are subcomplex modules (elemental version). (Contributed by BJ, 6-Jan-2024.)
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ ℂMod)
Theorem	bj-rvecsscmod 37928	Real vector spaces are subcomplex modules. (Contributed by BJ, 6-Jan-2024.)
⊢ ℝ-Vec ⊆ ℂMod
Theorem	bj-rvecsscvec 37929	Real vector spaces are subcomplex vector spaces. (Contributed by BJ, 6-Jan-2024.)
⊢ ℝ-Vec ⊆ ℂVec
Theorem	bj-rveccvec 37930	Real vector spaces are subcomplex vector spaces (elemental version). (Contributed by BJ, 6-Jan-2024.)
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ ℂVec)
Theorem	bj-rvecssabl 37931	(The additive groups of) real vector spaces are commutative groups. (Contributed by BJ, 9-Jun-2019.)
⊢ ℝ-Vec ⊆ Abel
Theorem	bj-rvecabl 37932	(The additive groups of) real vector spaces are commutative groups (elemental version). (Contributed by BJ, 9-Jun-2019.)
⊢ (𝐴 ∈ ℝ-Vec → 𝐴 ∈ Abel)
21.19.8.2  Complex numbers (supplements) Some lemmas to ease algebraic manipulations.
Theorem	bj-subcom 37933	A consequence of commutativity of multiplication. (Contributed by BJ, 6-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) − (𝐵 · 𝐴)) = 0)
Theorem	bj-lineqi 37934	Solution of a (scalar) linear equation. (Contributed by BJ, 6-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑌 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → ((𝐴 · 𝑋) + 𝐵) = 𝑌)    ⇒   ⊢ (𝜑 → 𝑋 = ((𝑌 − 𝐵) / 𝐴))
21.19.8.3  Barycentric coordinates Lemmas about barycentric coordinates. For the moment, this is limited to the one-dimensional case (complex line), where existence and uniqueness of barycentric coordinates are proved by bj-bary1 37937 (which computes them). It would be nice to prove the two-dimensional case (is it easier to use ad hoc computations, or Cramer formulas?), in order to do some planar geometry.
Theorem	bj-bary1lem 37935	Lemma for bj-bary1 37937: expression for a barycenter of two points in one dimension (complex line). (Contributed by BJ, 6-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 = ((((𝐵 − 𝑋) / (𝐵 − 𝐴)) · 𝐴) + (((𝑋 − 𝐴) / (𝐵 − 𝐴)) · 𝐵)))
Theorem	bj-bary1lem1 37936	Lemma for bj-bary1 37937: computation of one of the two barycentric coordinates of a barycenter of two points in one dimension (complex line). (Contributed by BJ, 6-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝑆 ∈ ℂ)    &   ⊢ (𝜑 → 𝑇 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝑋 = ((𝑆 · 𝐴) + (𝑇 · 𝐵)) ∧ (𝑆 + 𝑇) = 1) → 𝑇 = ((𝑋 − 𝐴) / (𝐵 − 𝐴))))
Theorem	bj-bary1 37937	Barycentric coordinates in one dimension (complex line). In the statement, 𝑋 is the barycenter of the two points 𝐴, 𝐵 with respective normalized coefficients 𝑆, 𝑇. (Contributed by BJ, 6-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝑆 ∈ ℂ)    &   ⊢ (𝜑 → 𝑇 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝑋 = ((𝑆 · 𝐴) + (𝑇 · 𝐵)) ∧ (𝑆 + 𝑇) = 1) ↔ (𝑆 = ((𝐵 − 𝑋) / (𝐵 − 𝐴)) ∧ 𝑇 = ((𝑋 − 𝐴) / (𝐵 − 𝐴)))))
21.19.9  Monoid of endomorphisms
Syntax	cend 37938	Token for the monoid of endomorphisms.
class End
Definition	df-bj-end 37939*	The monoid of endomorphisms on an object of a category. (Contributed by BJ, 4-Apr-2024.)
⊢ End = (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐) ↦ {⟨(Base‘ndx), (𝑥(Hom ‘𝑐)𝑥)⟩, ⟨(+g‘ndx), (⟨𝑥, 𝑥⟩(comp‘𝑐)𝑥)⟩}))
Theorem	bj-endval 37940	Value of the monoid of endomorphisms on an object of a category. (Contributed by BJ, 5-Apr-2024.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    ⇒   ⊢ (𝜑 → ((End ‘𝐶)‘𝑋) = {⟨(Base‘ndx), (𝑋(Hom ‘𝐶)𝑋)⟩, ⟨(+g‘ndx), (⟨𝑋, 𝑋⟩(comp‘𝐶)𝑋)⟩})
Theorem	bj-endbase 37941	Base set of the monoid of endomorphisms on an object of a category. (Contributed by BJ, 5-Apr-2024.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    ⇒   ⊢ (𝜑 → (Base‘((End ‘𝐶)‘𝑋)) = (𝑋(Hom ‘𝐶)𝑋))
Theorem	bj-endcomp 37942	Composition law of the monoid of endomorphisms on an object of a category. (Contributed by BJ, 5-Apr-2024.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    ⇒   ⊢ (𝜑 → (+g‘((End ‘𝐶)‘𝑋)) = (⟨𝑋, 𝑋⟩(comp‘𝐶)𝑋))
Theorem	bj-endmnd 37943	The monoid of endomorphisms on an object of a category is a monoid. (Contributed by BJ, 5-Apr-2024.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    ⇒   ⊢ (𝜑 → ((End ‘𝐶)‘𝑋) ∈ Mnd)
21.20  Mathbox for Jim Kingdon
21.20.1  Circle constant
Theorem	taupilem3 37944	Lemma for tau-related theorems. (Contributed by Jim Kingdon, 16-Feb-2019.)
⊢ (𝐴 ∈ (ℝ+ ∩ (◡cos “ {1})) ↔ (𝐴 ∈ ℝ+ ∧ (cos‘𝐴) = 1))
Theorem	taupilemrplb 37945*	A set of positive reals has (in the reals) a lower bound. (Contributed by Jim Kingdon, 19-Feb-2019.)
⊢ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (ℝ+ ∩ 𝐴)𝑥 ≤ 𝑦
Theorem	taupilem1 37946	Lemma for taupi 37948. A positive real whose cosine is one is at least 2 · π. (Contributed by Jim Kingdon, 19-Feb-2019.)
⊢ ((𝐴 ∈ ℝ+ ∧ (cos‘𝐴) = 1) → (2 · π) ≤ 𝐴)
Theorem	taupilem2 37947	Lemma for taupi 37948. The smallest positive real whose cosine is one is at most 2 · π. (Contributed by Jim Kingdon, 19-Feb-2019.) (Revised by AV, 1-Oct-2020.)
⊢ τ ≤ (2 · π)
Theorem	taupi 37948	Relationship between τ and π. This can be seen as connecting the ratio of a circle's circumference to its radius and the ratio of a circle's circumference to its diameter. (Contributed by Jim Kingdon, 19-Feb-2019.) (Revised by AV, 1-Oct-2020.)
⊢ τ = (2 · π)
21.20.2  Number theory
Theorem	dfgcd3 37949*	Alternate definition of the gcd operator. (Contributed by Jim Kingdon, 31-Dec-2021.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (℩𝑑 ∈ ℕ0 ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))))
21.20.3  Real numbers
Theorem	irrdifflemf 37950	Lemma for irrdiff 37951. The forward direction. (Contributed by Jim Kingdon, 20-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → ¬ 𝐴 ∈ ℚ)    &   ⊢ (𝜑 → 𝑄 ∈ ℚ)    &   ⊢ (𝜑 → 𝑅 ∈ ℚ)    &   ⊢ (𝜑 → 𝑄 ≠ 𝑅)    ⇒   ⊢ (𝜑 → (abs‘(𝐴 − 𝑄)) ≠ (abs‘(𝐴 − 𝑅)))
Theorem	irrdiff 37951*	The irrationals are exactly those reals that are a different distance from every rational. (Contributed by Jim Kingdon, 19-May-2024.)
⊢ (𝐴 ∈ ℝ → (¬ 𝐴 ∈ ℚ ↔ ∀𝑞 ∈ ℚ ∀𝑟 ∈ ℚ (𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) ≠ (abs‘(𝐴 − 𝑟)))))
Theorem	qdiff 37952*	The rationals are exactly those reals for which there exist two distinct rationals that are the same distance from the original number. Similar to irrdiff 37951 but here proved with a proof which would also work in constructive mathematics. From an online post by Ingo Blechschmidt. For a proof using irrdiff 37951, see qdiffALT 37953. (Contributed by Jim Kingdon, 24-Apr-2026.)
⊢ (𝐴 ∈ ℝ → (𝐴 ∈ ℚ ↔ ∃𝑞 ∈ ℚ ∃𝑟 ∈ ℚ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))))
Theorem	qdiffALT 37953*	Alternate proof of qdiff 37952. This is a proof from irrdiff 37951 using excluded middle in a variety of places. (Contributed by Jim Kingdon, 27-Apr-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℝ → (𝐴 ∈ ℚ ↔ ∃𝑞 ∈ ℚ ∃𝑟 ∈ ℚ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))))
Theorem	iccioo01 37954	The closed unit interval is equinumerous to the open unit interval. Based on a Mastodon post by Michael Kinyon. (Contributed by Jim Kingdon, 4-Jun-2024.)
⊢ (0[,]1) ≈ (0(,)1)
21.21  Mathbox for ML
21.21.1  Miscellaneous
Theorem	csbrecsg 37955	Move class substitution in and out of recs. (Contributed by ML, 25-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌recs(𝐹) = recs(⦋𝐴 / 𝑥⦌𝐹))
Theorem	csbrdgg 37956	Move class substitution in and out of the recursive function generator. (Contributed by ML, 25-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌rec(𝐹, 𝐼) = rec(⦋𝐴 / 𝑥⦌𝐹, ⦋𝐴 / 𝑥⦌𝐼))
Theorem	csboprabg 37957*	Move class substitution in and out of class abstractions of nested ordered pairs. (Contributed by ML, 25-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∣ 𝜑} = {⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∣ [𝐴 / 𝑥]𝜑})
Theorem	csbmpo123 37958*	Move class substitution in and out of maps-to notation for operations. (Contributed by ML, 25-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝑦 ∈ 𝑌, 𝑧 ∈ 𝑍 ↦ 𝐷) = (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝑌, 𝑧 ∈ ⦋𝐴 / 𝑥⦌𝑍 ↦ ⦋𝐴 / 𝑥⦌𝐷))
Theorem	con1bii2 37959	A contraposition inference. (Contributed by ML, 18-Oct-2020.)
⊢ (¬ 𝜑 ↔ 𝜓)    ⇒   ⊢ (𝜑 ↔ ¬ 𝜓)
Theorem	con2bii2 37960	A contraposition inference. (Contributed by ML, 18-Oct-2020.)
⊢ (𝜑 ↔ ¬ 𝜓)    ⇒   ⊢ (¬ 𝜑 ↔ 𝜓)
Theorem	vtoclefex 37961*	Implicit substitution of a class for a setvar variable. (Contributed by ML, 17-Oct-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝑥 = 𝐴 → 𝜑)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜑)
Theorem	rnmptsn 37962*	The range of a function mapping to singletons. (Contributed by ML, 15-Jul-2020.)
⊢ ran (𝑥 ∈ 𝐴 ↦ {𝑥}) = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}}
Theorem	f1omptsnlem 37963*	This is the core of the proof of f1omptsn 37964, but to avoid the distinct variables on the definitions, we split this proof into two. (Contributed by ML, 15-Jul-2020.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ {𝑥})    &   ⊢ 𝑅 = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}}    ⇒   ⊢ 𝐹:𝐴–1-1-onto→𝑅
Theorem	f1omptsn 37964*	A function mapping to singletons is bijective onto a set of singletons. (Contributed by ML, 16-Jul-2020.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ {𝑥})    &   ⊢ 𝑅 = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}}    ⇒   ⊢ 𝐹:𝐴–1-1-onto→𝑅
Theorem	mptsnunlem 37965*	This is the core of the proof of mptsnun 37966, but to avoid the distinct variables on the definitions, we split this proof into two. (Contributed by ML, 16-Jul-2020.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ {𝑥})    &   ⊢ 𝑅 = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}}    ⇒   ⊢ (𝐵 ⊆ 𝐴 → 𝐵 = ∪ (𝐹 “ 𝐵))
Theorem	mptsnun 37966*	A class 𝐵 is equal to the union of the class of all singletons of elements of 𝐵. (Contributed by ML, 16-Jul-2020.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ {𝑥})    &   ⊢ 𝑅 = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}}    ⇒   ⊢ (𝐵 ⊆ 𝐴 → 𝐵 = ∪ (𝐹 “ 𝐵))
Theorem	dissneqlem 37967*	This is the core of the proof of dissneq 37968, but to avoid the distinct variables on the definitions, we split this proof into two. (Contributed by ML, 16-Jul-2020.)
⊢ 𝐶 = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}}    ⇒   ⊢ ((𝐶 ⊆ 𝐵 ∧ 𝐵 ∈ (TopOn‘𝐴)) → 𝐵 = 𝒫 𝐴)
Theorem	dissneq 37968*	Any topology that contains every single-point set is the discrete topology. (Contributed by ML, 16-Jul-2020.)
⊢ 𝐶 = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}}    ⇒   ⊢ ((𝐶 ⊆ 𝐵 ∧ 𝐵 ∈ (TopOn‘𝐴)) → 𝐵 = 𝒫 𝐴)
Theorem	exlimim 37969*	Closed form of exlimimd 37970. (Contributed by ML, 17-Jul-2020.)
⊢ ((∃𝑥𝜑 ∧ ∀𝑥(𝜑 → 𝜓)) → 𝜓)
Theorem	exlimimd 37970*	Existential elimination rule of natural deduction. (Contributed by ML, 17-Jul-2020.)
⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	exellim 37971*	Closed form of exellimddv 37972. See also exlimim 37969 for a more general theorem. (Contributed by ML, 17-Jul-2020.)
⊢ ((∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) → 𝜑)
Theorem	exellimddv 37972*	Eliminate an antecedent when the antecedent is elementhood, deduction version. See exellim 37971 for the closed form, which requires the use of a universal quantifier. (Contributed by ML, 17-Jul-2020.)
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	topdifinfindis 37973*	Part of Exercise 3 of [Munkres] p. 83. The topology of all subsets 𝑥 of 𝐴 such that the complement of 𝑥 in 𝐴 is infinite, or 𝑥 is the empty set, or 𝑥 is all of 𝐴, is the trivial topology when 𝐴 is finite. (Contributed by ML, 14-Jul-2020.)
⊢ 𝑇 = {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))}    ⇒   ⊢ (𝐴 ∈ Fin → 𝑇 = {∅, 𝐴})
Theorem	topdifinffinlem 37974*	This is the core of the proof of topdifinffin 37975, but to avoid the distinct variables on the definition, we need to split this proof into two. (Contributed by ML, 17-Jul-2020.)
⊢ 𝑇 = {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))}    ⇒   ⊢ (𝑇 ∈ (TopOn‘𝐴) → 𝐴 ∈ Fin)
Theorem	topdifinffin 37975*	Part of Exercise 3 of [Munkres] p. 83. The topology of all subsets 𝑥 of 𝐴 such that the complement of 𝑥 in 𝐴 is infinite, or 𝑥 is the empty set, or 𝑥 is all of 𝐴, is a topology only if 𝐴 is finite. (Contributed by ML, 17-Jul-2020.)
⊢ 𝑇 = {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))}    ⇒   ⊢ (𝑇 ∈ (TopOn‘𝐴) → 𝐴 ∈ Fin)
Theorem	topdifinf 37976*	Part of Exercise 3 of [Munkres] p. 83. The topology of all subsets 𝑥 of 𝐴 such that the complement of 𝑥 in 𝐴 is infinite, or 𝑥 is the empty set, or 𝑥 is all of 𝐴, is a topology if and only if 𝐴 is finite, in which case it is the trivial topology. (Contributed by ML, 17-Jul-2020.)
⊢ 𝑇 = {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))}    ⇒   ⊢ ((𝑇 ∈ (TopOn‘𝐴) ↔ 𝐴 ∈ Fin) ∧ (𝑇 ∈ (TopOn‘𝐴) → 𝑇 = {∅, 𝐴}))
Theorem	topdifinfeq 37977*	Two different ways of defining the collection from Exercise 3 of [Munkres] p. 83. (Contributed by ML, 18-Jul-2020.)
⊢ {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ ((𝐴 ∖ 𝑥) = ∅ ∨ (𝐴 ∖ 𝑥) = 𝐴))} = {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))}
Theorem	icorempo 37978*	Closed-below, open-above intervals of reals. (Contributed by ML, 26-Jul-2020.)
⊢ 𝐹 = ([,) ↾ (ℝ × ℝ))    ⇒   ⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
Theorem	icoreresf 37979	Closed-below, open-above intervals of reals map to subsets of reals. (Contributed by ML, 25-Jul-2020.)
⊢ ([,) ↾ (ℝ × ℝ)):(ℝ × ℝ)⟶𝒫 ℝ
Theorem	icoreval 37980*	Value of the closed-below, open-above interval function on reals. (Contributed by ML, 26-Jul-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,)𝐵) = {𝑧 ∈ ℝ ∣ (𝐴 ≤ 𝑧 ∧ 𝑧 < 𝐵)})
Theorem	icoreelrnab 37981*	Elementhood in the set of closed-below, open-above intervals of reals. (Contributed by ML, 27-Jul-2020.)
⊢ 𝐼 = ([,) “ (ℝ × ℝ))    ⇒   ⊢ (𝑋 ∈ 𝐼 ↔ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 𝑋 = {𝑧 ∈ ℝ ∣ (𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏)})
Theorem	isbasisrelowllem1 37982*	Lemma for isbasisrelowl 37985. (Contributed by ML, 27-Jul-2020.)
⊢ 𝐼 = ([,) “ (ℝ × ℝ))    ⇒   ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = {𝑧 ∈ ℝ ∣ (𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏)}) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = {𝑧 ∈ ℝ ∣ (𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑)})) ∧ (𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑)) → (𝑥 ∩ 𝑦) ∈ 𝐼)
Theorem	isbasisrelowllem2 37983*	Lemma for isbasisrelowl 37985. (Contributed by ML, 27-Jul-2020.)
⊢ 𝐼 = ([,) “ (ℝ × ℝ))    ⇒   ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = {𝑧 ∈ ℝ ∣ (𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏)}) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = {𝑧 ∈ ℝ ∣ (𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑)})) ∧ (𝑎 ≤ 𝑐 ∧ 𝑑 ≤ 𝑏)) → (𝑥 ∩ 𝑦) ∈ 𝐼)
Theorem	icoreclin 37984*	The set of closed-below, open-above intervals of reals is closed under finite intersection. (Contributed by ML, 27-Jul-2020.)
⊢ 𝐼 = ([,) “ (ℝ × ℝ))    ⇒   ⊢ ((𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼) → (𝑥 ∩ 𝑦) ∈ 𝐼)
Theorem	isbasisrelowl 37985	The set of all closed-below, open-above intervals of reals form a basis. (Contributed by ML, 27-Jul-2020.)
⊢ 𝐼 = ([,) “ (ℝ × ℝ))    ⇒   ⊢ 𝐼 ∈ TopBases
Theorem	icoreunrn 37986	The union of all closed-below, open-above intervals of reals is the set of reals. (Contributed by ML, 27-Jul-2020.)
⊢ 𝐼 = ([,) “ (ℝ × ℝ))    ⇒   ⊢ ℝ = ∪ 𝐼
Theorem	istoprelowl 37987	The set of all closed-below, open-above intervals of reals generate a topology on the reals. (Contributed by ML, 27-Jul-2020.)
⊢ 𝐼 = ([,) “ (ℝ × ℝ))    ⇒   ⊢ (topGen‘𝐼) ∈ (TopOn‘ℝ)
Theorem	icoreelrn 37988*	A class abstraction which is an element of the set of closed-below, open-above intervals of reals. (Contributed by ML, 1-Aug-2020.)
⊢ 𝐼 = ([,) “ (ℝ × ℝ))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → {𝑧 ∈ ℝ ∣ (𝐴 ≤ 𝑧 ∧ 𝑧 < 𝐵)} ∈ 𝐼)
Theorem	iooelexlt 37989*	An element of an open interval is not its smallest element. (Contributed by ML, 2-Aug-2020.)
⊢ (𝑋 ∈ (𝐴(,)𝐵) → ∃𝑦 ∈ (𝐴(,)𝐵)𝑦 < 𝑋)
Theorem	relowlssretop 37990	The lower limit topology on the reals is finer than the standard topology. (Contributed by ML, 1-Aug-2020.)
⊢ 𝐼 = ([,) “ (ℝ × ℝ))    ⇒   ⊢ (topGen‘ran (,)) ⊆ (topGen‘𝐼)
Theorem	relowlpssretop 37991	The lower limit topology on the reals is strictly finer than the standard topology. (Contributed by ML, 2-Aug-2020.)
⊢ 𝐼 = ([,) “ (ℝ × ℝ))    ⇒   ⊢ (topGen‘ran (,)) ⊊ (topGen‘𝐼)
Theorem	sucneqond 37992	Inequality of an ordinal set with its successor. Does not use the axiom of regularity. (Contributed by ML, 18-Oct-2020.)
⊢ (𝜑 → 𝑋 = suc 𝑌)    &   ⊢ (𝜑 → 𝑌 ∈ On)    ⇒   ⊢ (𝜑 → 𝑋 ≠ 𝑌)
Theorem	sucneqoni 37993	Inequality of an ordinal set with its successor. Does not use the axiom of regularity. (Contributed by ML, 18-Oct-2020.)
⊢ 𝑋 = suc 𝑌    &   ⊢ 𝑌 ∈ On    ⇒   ⊢ 𝑋 ≠ 𝑌
Theorem	onsucuni3 37994	If an ordinal number has a predecessor, then it is successor of that predecessor. (Contributed by ML, 17-Oct-2020.)
⊢ ((𝐵 ∈ On ∧ 𝐵 ≠ ∅ ∧ ¬ Lim 𝐵) → 𝐵 = suc ∪ 𝐵)
Theorem	1oequni2o 37995	The ordinal number 1o is the predecessor of the ordinal number 2o. (Contributed by ML, 19-Oct-2020.)
⊢ 1o = ∪ 2o
Theorem	rdgsucuni 37996	If an ordinal number has a predecessor, the value of the recursive definition generator at that number in terms of its predecessor. (Contributed by ML, 17-Oct-2020.)
⊢ ((𝐵 ∈ On ∧ 𝐵 ≠ ∅ ∧ ¬ Lim 𝐵) → (rec(𝐹, 𝐼)‘𝐵) = (𝐹‘(rec(𝐹, 𝐼)‘∪ 𝐵)))
Theorem	rdgeqoa 37997	If a recursive function with an initial value 𝐴 at step 𝑁 is equal to itself with an initial value 𝐵 at step 𝑀, then every finite number of successor steps will also be equal. (Contributed by ML, 21-Oct-2020.)
⊢ ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑋 ∈ ω) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑋)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑋))))
Theorem	elxp8 37998	Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp7 8022. (Contributed by ML, 19-Oct-2020.)
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ((1st ‘𝐴) ∈ 𝐵 ∧ 𝐴 ∈ (V × 𝐶)))
Theorem	cbveud 37999*	Deduction used to change bound variables in an existential uniqueness quantifier, using implicit substitution. (Contributed by ML, 27-Mar-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑦𝜒))
Theorem	cbvreud 38000*	Deduction used to change bound variables in a restricted existential uniqueness quantifier. (Contributed by ML, 27-Mar-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑦 ∈ 𝐴 𝜒))