P. 332 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33101-33200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-elccinfty 33101	A lemma for infinite extended complex numbers. (Contributed by BJ, 27-Jun-2019.)
⊢ (𝐴 ∈ (-π(,]π) → (inftyexpi ‘𝐴) ∈ ℂ∞)
Syntax	cccbar 33102	Syntax for the set of extended complex numbers ℂ̅.
class ℂ̅
Definition	df-bj-ccbar 33103	Definition of the set of extended complex numbers ℂ̅. (Contributed by BJ, 22-Jun-2019.)
⊢ ℂ̅ = (ℂ ∪ ℂ∞)
Theorem	bj-ccssccbar 33104	Complex numbers are extended complex numbers. (Contributed by BJ, 27-Jun-2019.)
⊢ ℂ ⊆ ℂ̅
Theorem	bj-ccinftyssccbar 33105	Infinite extended complex numbers are extended complex numbers. (Contributed by BJ, 27-Jun-2019.)
⊢ ℂ∞ ⊆ ℂ̅
Syntax	cpinfty 33106	Syntax for +∞.
class +∞
Definition	df-bj-pinfty 33107	Definition of +∞. (Contributed by BJ, 27-Jun-2019.)
⊢ +∞ = (inftyexpi ‘0)
Theorem	bj-pinftyccb 33108	The class +∞ is an extended complex number. (Contributed by BJ, 27-Jun-2019.)
⊢ +∞ ∈ ℂ̅
Theorem	bj-pinftynrr 33109	The extended complex number +∞ is not a complex number. (Contributed by BJ, 27-Jun-2019.)
⊢ ¬ +∞ ∈ ℂ
Syntax	cminfty 33110	Syntax for -∞.
class -∞
Definition	df-bj-minfty 33111	Definition of -∞. (Contributed by BJ, 27-Jun-2019.)
⊢ -∞ = (inftyexpi ‘π)
Theorem	bj-minftyccb 33112	The class -∞ is an extended complex number. (Contributed by BJ, 27-Jun-2019.)
⊢ -∞ ∈ ℂ̅
Theorem	bj-minftynrr 33113	The extended complex number -∞ is not a complex number. (Contributed by BJ, 27-Jun-2019.)
⊢ ¬ -∞ ∈ ℂ
Theorem	bj-pinftynminfty 33114	The extended complex numbers +∞ and -∞ are different. (Contributed by BJ, 27-Jun-2019.)
⊢ +∞ ≠ -∞
Syntax	crrbar 33115	Syntax for the set of extended real numbers ℝ̅.
class ℝ̅
Definition	df-bj-rrbar 33116	Definition of the set of extended real numbers ℝ̅. See df-xr 10078. (Contributed by BJ, 29-Jun-2019.)
⊢ ℝ̅ = (ℝ ∪ {-∞, +∞})
Syntax	cinfty 33117	Syntax for ∞.
class ∞
Definition	df-bj-infty 33118	Definition of ∞, the point at infinity of the real or complex projective line. (Contributed by BJ, 27-Jun-2019.) The precise definition is irrelevant and should generally not be used. (New usage is discouraged.)
⊢ ∞ = 𝒫 ∪ ℂ
Syntax	ccchat 33119	Syntax for ℂ̂.
class ℂ̂
Definition	df-bj-cchat 33120	Define the complex projective line, or Riemann sphere. (Contributed by BJ, 27-Jun-2019.)
⊢ ℂ̂ = (ℂ ∪ {∞})
Syntax	crrhat 33121	Syntax for ℝ̂.
class ℝ̂
Definition	df-bj-rrhat 33122	Define the real projective line. (Contributed by BJ, 27-Jun-2019.)
⊢ ℝ̂ = (ℝ ∪ {∞})
Theorem	bj-rrhatsscchat 33123	The real projective line is included in the complex projective line. (Contributed by BJ, 27-Jun-2019.)
⊢ ℝ̂ ⊆ ℂ̂
20.14.6.3  Addition and opposite We define the operations on the extended real and complex numbers and on the real and complex projective lines simultaneously, thus "overloading" the operations.
Syntax	caddcc 33124	Syntax for the addition of extended complex numbers.
class +ℂ̅
Definition	df-bj-addc 33125	Define the additions on the extended complex numbers (on the subset of (ℂ̅ × ℂ̅) where it makes sense) and on the complex projective line (Riemann sphere). (Contributed by BJ, 22-Jun-2019.)
⊢ +ℂ̅ = (𝑥 ∈ (((ℂ × ℂ̅) ∪ (ℂ̅ × ℂ)) ∪ ((ℂ̂ × ℂ̂) ∪ (Diag‘ℂ∞))) ↦ if(((1st ‘𝑥) = ∞ ∨ (2nd ‘𝑥) = ∞), ∞, if((1st ‘𝑥) ∈ ℂ, if((2nd ‘𝑥) ∈ ℂ, ((1st ‘𝑥) + (2nd ‘𝑥)), (2nd ‘𝑥)), (1st ‘𝑥))))
Syntax	coppcc 33126	Syntax for the opposite of extended complex numbers.
class -ℂ̅
Definition	df-bj-oppc 33127	Define the negation (operation givin the opposite) the set of extended complex numbers and the complex projective line (Riemann sphere). One could use the prcpal function in the infinite case, but we want to use only basic functions at this point. (Contributed by BJ, 22-Jun-2019.)
⊢ -ℂ̅ = (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = ∞, ∞, if(𝑥 ∈ ℂ, -𝑥, (inftyexpi ‘if(0 < (1st ‘𝑥), ((1st ‘𝑥) − π), ((1st ‘𝑥) + π))))))
20.14.6.4  Argument, multiplication and inverse Since one needs arguments in order to define multiplication in ℂ̅, it seems harder to put this at the very beginning of the introduction of complex numbers.
Syntax	cprcpal 33128	Syntax for the function prcpal.
class prcpal
Definition	df-bj-prcpal 33129	Define the function prcpal. (Contributed by BJ, 22-Jun-2019.)
⊢ prcpal = (𝑥 ∈ ℝ ↦ ((𝑥 mod (2 · π)) − if((𝑥 mod (2 · π)) ≤ π, 0, (2 · π))))
Syntax	carg 33130	Syntax for the argument of a nonzero extended complex number.
class Arg
Definition	df-bj-arg 33131	Define the argument of a nonzero extended complex number. By convention, it has values in (-π, π]. Another convention chooses [0, 2π) but the present one simplifies formulas giving the argument as an arctangent. (Contributed by BJ, 22-Jun-2019.)
⊢ Arg = (𝑥 ∈ (ℂ̅ ∖ {0}) ↦ if(𝑥 ∈ ℂ, (ℑ‘(log‘𝑥)), (1st ‘𝑥)))
Syntax	cmulc 33132	Syntax for the multiplication of extended complex numbers.
class ·ℂ̅
Definition	df-bj-mulc 33133	Define the multiplication of extended complex numbers and of the complex projective line (Riemann sphere). In our convention, a product with 0 is 0, even when the other factor is infinite. An alternate convention leaves products of 0 with an infinite number undefined since the multiplication is not continuous at these points. Note that our convention entails (0 / 0) = 0. (Contributed by BJ, 22-Jun-2019.)
⊢ ·ℂ̅ = (𝑥 ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ↦ if(((1st ‘𝑥) = 0 ∨ (2nd ‘𝑥) = 0), 0, if(((1st ‘𝑥) = ∞ ∨ (2nd ‘𝑥) = ∞), ∞, if(𝑥 ∈ (ℂ × ℂ), ((1st ‘𝑥) · (2nd ‘𝑥)), (inftyexpi ‘(prcpal‘((Arg‘(1st ‘𝑥)) + (Arg‘(2nd ‘𝑥)))))))))
Syntax	cinvc 33134	Syntax for the inverse of nonzero extended complex numbers.
class -1ℂ̅
Definition	df-bj-invc 33135	Define inversion, which maps a nonzero extended complex number or element of the complex projective line (Riemann sphere) to its inverse. Beware of the overloading: the equality (-1ℂ̅‘0) = ∞ is to be understood in the complex projective line, but 0 as an extended complex number does not have an inverse, which we can state as (-1ℂ̅‘0) ∉ ℂ̅. (Contributed by BJ, 22-Jun-2019.)
⊢ -1ℂ̅ = (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = 0, ∞, if(𝑥 ∈ ℂ, (1 / 𝑥), 0)))
20.14.7  Monoids See ccmn 18193 and subsequents. The first few statements of this subsection can be put very early after ccmn 18193. Proposal: in the main part, make separate subsections of commutative monoids and abelian groups. Relabel cabl 18194 to "cabl" or, preferably, other labels containing "abl" to "abel", for consistency.
Theorem	bj-cmnssmnd 33136	Commutative monoids are monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ CMnd ⊆ Mnd
Theorem	bj-cmnssmndel 33137	Commutative monoids are monoids (elemental version). This is a more direct proof of cmnmnd 18208, which relies on iscmn 18200. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ CMnd → 𝐴 ∈ Mnd)
Theorem	bj-ablssgrp 33138	Abelian groups are groups. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ Abel ⊆ Grp
Theorem	bj-ablssgrpel 33139	Abelian groups are groups (elemental version). This is a shorter proof of ablgrp 18198. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ Abel → 𝐴 ∈ Grp)
Theorem	bj-ablsscmn 33140	Abelian groups are commutative monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ Abel ⊆ CMnd
Theorem	bj-ablsscmnel 33141	Abelian groups are commutative monoids (elemental version). This is a shorter proof of ablcmn 18199. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ Abel → 𝐴 ∈ CMnd)
Theorem	bj-modssabl 33142	(The additive groups of) modules are abelian groups. (The elemental version is lmodabl 18910; see also lmodgrp 18870 and lmodcmn 18911.) (Contributed by BJ, 9-Jun-2019.)
⊢ LMod ⊆ Abel
Theorem	bj-vecssmod 33143	Vector spaces are modules. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ LVec ⊆ LMod
Theorem	bj-vecssmodel 33144	Vector spaces are modules (elemental version). This is a shorter proof of lveclmod 19106. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ LVec → 𝐴 ∈ LMod)
20.14.7.1  Finite sums in monoids UPDATE: a similar summation is already defined as df-gsum 16103 (although it mixes finite and infinite sums, which makes it harder to understand).
Syntax	cfinsum 33145	Syntax for the class "finite summation in monoids".
class FinSum
Definition	df-bj-finsum 33146*	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 33147*	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‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(#‘𝐼)))))
20.14.8  Affine, Euclidean, and Cartesian geometry A few basic theorems to start affine, Euclidean, and Cartesian geometry.
20.14.8.1  Convex hull in real vector spaces A few basic definitions and theorems about convex hulls in real vector spaces. TODO: prove inclusion in the class of subcomplex vector spaces.
Syntax	crrvec 33148	Syntax for the class of real vector spaces.
class ℝ-Vec
Definition	df-bj-rrvec 33149	Definition of the class of real vector spaces. (Contributed by BJ, 9-Jun-2019.)
⊢ ℝ-Vec = {𝑥 ∈ LVec ∣ (Scalar‘𝑥) = ℝfld}
Theorem	bj-rrvecssvec 33150	Real vector spaces are vector spaces. (Contributed by BJ, 9-Jun-2019.)
⊢ ℝ-Vec ⊆ LVec
Theorem	bj-rrvecssvecel 33151	Real vector spaces are vector spaces (elemental version). (Contributed by BJ, 9-Jun-2019.)
⊢ (𝐴 ∈ ℝ-Vec → 𝐴 ∈ LVec)
Theorem	bj-rrvecsscmn 33152	(The additive groups of) real vector spaces are commutative monoids. (Contributed by BJ, 9-Jun-2019.)
⊢ ℝ-Vec ⊆ CMnd
Theorem	bj-rrvecsscmnel 33153	(The additive groups of) real vector spaces are commutative monoids (elemental version). (Contributed by BJ, 9-Jun-2019.)
⊢ (𝐴 ∈ ℝ-Vec → 𝐴 ∈ CMnd)
20.14.8.2  Complex numbers (supplements) Some lemmas to ease algebraic manipulations.
Theorem	bj-subcom 33154	A consequence of commutativity of multiplication. (Contributed by BJ, 6-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) − (𝐵 · 𝐴)) = 0)
Theorem	bj-ldiv 33155	Left-division. (Contributed by BJ, 6-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) = 𝐶 ↔ 𝐴 = (𝐶 / 𝐵)))
Theorem	bj-rdiv 33156	Right-division. (Contributed by BJ, 6-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) = 𝐶 ↔ 𝐵 = (𝐶 / 𝐴)))
Theorem	bj-mdiv 33157	A division law. (Contributed by BJ, 6-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 = (𝐶 / 𝐵) ↔ 𝐵 = (𝐶 / 𝐴)))
Theorem	bj-lineq 33158	Solution of a (scalar) linear equation. (Contributed by BJ, 6-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑌 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (((𝐴 · 𝑋) + 𝐵) = 𝑌 ↔ 𝑋 = ((𝑌 − 𝐵) / 𝐴)))
Theorem	bj-lineqi 33159	Solution of a (scalar) linear equation. (Contributed by BJ, 6-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑌 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → ((𝐴 · 𝑋) + 𝐵) = 𝑌)    ⇒   ⊢ (𝜑 → 𝑋 = ((𝑌 − 𝐵) / 𝐴))
20.14.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 33162 (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 33160	A lemma for barycentric coordinates in one dimension. (Contributed by BJ, 6-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 = ((((𝐵 − 𝑋) / (𝐵 − 𝐴)) · 𝐴) + (((𝑋 − 𝐴) / (𝐵 − 𝐴)) · 𝐵)))
Theorem	bj-bary1lem1 33161	Existence and uniqueness (and actual computation) of barycentric coordinates in dimension 1 (complex line). (Contributed by BJ, 6-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝑆 ∈ ℂ)    &   ⊢ (𝜑 → 𝑇 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝑋 = ((𝑆 · 𝐴) + (𝑇 · 𝐵)) ∧ (𝑆 + 𝑇) = 1) → 𝑇 = ((𝑋 − 𝐴) / (𝐵 − 𝐴))))
Theorem	bj-bary1 33162	Barycentric coordinates in one dimension. (Contributed by BJ, 6-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝑆 ∈ ℂ)    &   ⊢ (𝜑 → 𝑇 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝑋 = ((𝑆 · 𝐴) + (𝑇 · 𝐵)) ∧ (𝑆 + 𝑇) = 1) ↔ (𝑆 = ((𝐵 − 𝑋) / (𝐵 − 𝐴)) ∧ 𝑇 = ((𝑋 − 𝐴) / (𝐵 − 𝐴)))))
20.15  Mathbox for Jim Kingdon
20.15.0.1  Circle constant
Syntax	ctau 33163	Extend class notation to include tau = 6.283185....
class τ
Definition	df-tau 33164	Define tau = 6.283185..., which is the smallest positive real number whose cosine is one. Various notations have been used or proposed for this number including τ, a three-legged variant of π, or 2π. Note the difference between this constant τ and the variable 𝜏 which is a variable representing a propositional logic formula. Only the latter is italic, and the colors are different. (Contributed by Jim Kingdon, 9-Apr-2018.) (Revised by AV, 1-Oct-2020.)
⊢ τ = inf((ℝ+ ∩ (◡cos “ {1})), ℝ, < )
Theorem	taupilem3 33165	Lemma for tau-related theorems . (Contributed by Jim Kingdon, 16-Feb-2019.)
⊢ (𝐴 ∈ (ℝ+ ∩ (◡cos “ {1})) ↔ (𝐴 ∈ ℝ+ ∧ (cos‘𝐴) = 1))
Theorem	taupilemrplb 33166*	A set of positive reals has (in the reals) a lower bound. (Contributed by Jim Kingdon, 19-Feb-2019.)
⊢ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (ℝ+ ∩ 𝐴)𝑥 ≤ 𝑦
Theorem	taupilem1 33167	Lemma for taupi 33169. A positive real whose cosine is one is at least 2 · π. (Contributed by Jim Kingdon, 19-Feb-2019.)
⊢ ((𝐴 ∈ ℝ+ ∧ (cos‘𝐴) = 1) → (2 · π) ≤ 𝐴)
Theorem	taupilem2 33168	Lemma for taupi 33169. 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 33169	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 · π)
20.15.0.2  Number theory
Theorem	dfgcd3 33170*	Alternate definition of the gcd operator. (Contributed by Jim Kingdon, 31-Dec-2021.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (℩𝑑 ∈ ℕ0 ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))))
20.16  Mathbox for ML
Theorem	csbdif 33171	Distribution of class substitution over difference of two classes. (Contributed by ML, 14-Jul-2020.)
⊢ ⦋𝐴 / 𝑥⦌(𝐵 ∖ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∖ ⦋𝐴 / 𝑥⦌𝐶)
Theorem	csbpredg 33172	Move class substitution in and out of the predecessor class of a relationship. (Contributed by ML, 25-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌Pred(𝑅, 𝐷, 𝑋) = Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, ⦋𝐴 / 𝑥⦌𝑋))
Theorem	csbwrecsg 33173	Move class substitution in and out of the well-founded recursive function generator . (Contributed by ML, 25-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌wrecs(𝑅, 𝐷, 𝐹) = wrecs(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, ⦋𝐴 / 𝑥⦌𝐹))
Theorem	csbrecsg 33174	Move class substitution in and out of recs. (Contributed by ML, 25-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌recs(𝐹) = recs(⦋𝐴 / 𝑥⦌𝐹))
Theorem	csbrdgg 33175	Move class substitution in and out of the recursive function generator. (Contributed by ML, 25-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌rec(𝐹, 𝐼) = rec(⦋𝐴 / 𝑥⦌𝐹, ⦋𝐴 / 𝑥⦌𝐼))
Theorem	csboprabg 33176*	Move class substitution in and out of class abstractions of nested ordered pairs. (Contributed by ML, 25-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∣ 𝜑} = {⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∣ [𝐴 / 𝑥]𝜑})
Theorem	csbmpt22g 33177*	Move class substitution in and out of maps-to notation for operations. (Contributed by ML, 25-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝑦 ∈ 𝑌, 𝑧 ∈ 𝑍 ↦ 𝐷) = (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝑌, 𝑧 ∈ ⦋𝐴 / 𝑥⦌𝑍 ↦ ⦋𝐴 / 𝑥⦌𝐷))
Theorem	mpnanrd 33178	Eliminate the right side of a negated conjunction in an implication. (Contributed by ML, 17-Oct-2020.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜑 → ¬ 𝜒)
Theorem	con1bii2 33179	A contraposition inference. (Contributed by ML, 18-Oct-2020.)
⊢ (¬ 𝜑 ↔ 𝜓)    ⇒   ⊢ (𝜑 ↔ ¬ 𝜓)
Theorem	con2bii2 33180	A contraposition inference. (Contributed by ML, 18-Oct-2020.)
⊢ (𝜑 ↔ ¬ 𝜓)    ⇒   ⊢ (¬ 𝜑 ↔ 𝜓)
Theorem	vtoclefex 33181*	Implicit substitution of a class for a setvar variable. (Contributed by ML, 17-Oct-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝑥 = 𝐴 → 𝜑)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜑)
Theorem	rnmptsn 33182*	The range of a function mapping to singletons. (Contributed by ML, 15-Jul-2020.)
⊢ ran (𝑥 ∈ 𝐴 ↦ {𝑥}) = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}}
Theorem	f1omptsnlem 33183*	This is the core of the proof of f1omptsn 33184, 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 33184*	A function mapping to singletons is bijective onto a set of singletons. (Contributed by ML, 16-Jul-2020.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ {𝑥})    &   ⊢ 𝑅 = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}}    ⇒   ⊢ 𝐹:𝐴–1-1-onto→𝑅
Theorem	mptsnunlem 33185*	This is the core of the proof of mptsnun 33186, but to avoid the distinct variables on the definitions, we split this proof into two. (Contributed by ML, 16-Jul-2020.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ {𝑥})    &   ⊢ 𝑅 = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}}    ⇒   ⊢ (𝐵 ⊆ 𝐴 → 𝐵 = ∪ (𝐹 “ 𝐵))
Theorem	mptsnun 33186*	A class 𝐵 is equal to the union of the class of all singletons of elements of 𝐵. (Contributed by ML, 16-Jul-2020.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ {𝑥})    &   ⊢ 𝑅 = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}}    ⇒   ⊢ (𝐵 ⊆ 𝐴 → 𝐵 = ∪ (𝐹 “ 𝐵))
Theorem	dissneqlem 33187*	This is the core of the proof of dissneq 33188, but to avoid the distinct variables on the definitions, we split this proof into two. (Contributed by ML, 16-Jul-2020.)
⊢ 𝐶 = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}}    ⇒   ⊢ ((𝐶 ⊆ 𝐵 ∧ 𝐵 ∈ (TopOn‘𝐴)) → 𝐵 = 𝒫 𝐴)
Theorem	dissneq 33188*	Any topology that contains every single-point set is the discrete topology. (Contributed by ML, 16-Jul-2020.)
⊢ 𝐶 = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}}    ⇒   ⊢ ((𝐶 ⊆ 𝐵 ∧ 𝐵 ∈ (TopOn‘𝐴)) → 𝐵 = 𝒫 𝐴)
Theorem	exlimim 33189*	Closed form of exlimimd 33190. (Contributed by ML, 17-Jul-2020.)
⊢ ((∃𝑥𝜑 ∧ ∀𝑥(𝜑 → 𝜓)) → 𝜓)
Theorem	exlimimd 33190*	Existential elimination rule of natural deduction. (Contributed by ML, 17-Jul-2020.)
⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	exlimimdd 33191	Existential elimination rule of natural deduction. (Contributed by ML, 17-Jul-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	exellim 33192*	Closed form of exellimddv 33193. See also exlimim 33189 for a more general theorem. (Contributed by ML, 17-Jul-2020.)
⊢ ((∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) → 𝜑)
Theorem	exellimddv 33193*	Eliminate an antecedent when the antecedent is elementhood, deduction version. See exellim 33192 for the closed form, which requires the use of a universal quantifier. (Contributed by ML, 17-Jul-2020.)
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	topdifinfindis 33194*	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 33195*	This is the core of the proof of topdifinffin 33196, 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 33196*	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 33197*	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 33198*	Two different ways of defining the collection from Exercise 3 of [Munkres] p. 83. (Contributed by ML, 18-Jul-2020.)
⊢ {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ ((𝐴 ∖ 𝑥) = ∅ ∨ (𝐴 ∖ 𝑥) = 𝐴))} = {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))}
Theorem	icorempt2 33199*	Closed-below, open-above intervals of reals. (Contributed by ML, 26-Jul-2020.)
⊢ 𝐹 = ([,) ↾ (ℝ × ℝ))    ⇒   ⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
Theorem	icoreresf 33200	Closed-below, open-above intervals of reals map to subsets of reals. (Contributed by ML, 25-Jul-2020.)
⊢ ([,) ↾ (ℝ × ℝ)):(ℝ × ℝ)⟶𝒫 ℝ