P. 420 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 41901-42000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rngunsnply 41901*	Adjoining one element to a ring results in a set of polynomial evaluations. (Contributed by Stefan O'Rear, 30-Nov-2014.)
⊢ (𝜑 → 𝐵 ∈ (SubRing‘ℂfld))    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑆 = ((RingSpan‘ℂfld)‘(𝐵 ∪ {𝑋})))    ⇒   ⊢ (𝜑 → (𝑉 ∈ 𝑆 ↔ ∃𝑝 ∈ (Poly‘𝐵)𝑉 = (𝑝‘𝑋)))
Theorem	flcidc 41902*	Finite linear combinations with an indicator function. (Contributed by Stefan O'Rear, 5-Dec-2014.)
⊢ (𝜑 → 𝐹 = (𝑗 ∈ 𝑆 ↦ if(𝑗 = 𝐾, 1, 0)))    &   ⊢ (𝜑 → 𝑆 ∈ Fin)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑆) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑖 ∈ 𝑆 ((𝐹‘𝑖) · 𝐵) = ⦋𝐾 / 𝑖⦌𝐵)
21.31.46  Endomorphism algebra
Syntax	cmend 41903	Syntax for module endomorphism algebra.
class MEndo
Definition	df-mend 41904*	Define the endomorphism algebra of a module. (Contributed by Stefan O'Rear, 2-Sep-2015.)
⊢ MEndo = (𝑚 ∈ V ↦ ⦋(𝑚 LMHom 𝑚) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f (+g‘𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠 ‘𝑚)𝑦))⟩}))
Theorem	algstr 41905	Lemma to shorten proofs of algbase 41906 through algvsca 41910. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐴 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩})    ⇒   ⊢ 𝐴 Struct ⟨1, 6⟩
Theorem	algbase 41906	The base set of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐴 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩})    ⇒   ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝐴))
Theorem	algaddg 41907	The additive operation of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐴 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩})    ⇒   ⊢ ( + ∈ 𝑉 → + = (+g‘𝐴))
Theorem	algmulr 41908	The multiplicative operation of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐴 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩})    ⇒   ⊢ ( × ∈ 𝑉 → × = (.r‘𝐴))
Theorem	algsca 41909	The set of scalars of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐴 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩})    ⇒   ⊢ (𝑆 ∈ 𝑉 → 𝑆 = (Scalar‘𝐴))
Theorem	algvsca 41910	The scalar product operation of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐴 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩})    ⇒   ⊢ ( · ∈ 𝑉 → · = ( ·𝑠 ‘𝐴))
Theorem	mendval 41911*	Value of the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.)
⊢ 𝐵 = (𝑀 LMHom 𝑀)    &   ⊢ + = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f (+g‘𝑀)𝑦))    &   ⊢ × = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))    &   ⊢ 𝑆 = (Scalar‘𝑀)    &   ⊢ · = (𝑥 ∈ (Base‘𝑆), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f ( ·𝑠 ‘𝑀)𝑦))    ⇒   ⊢ (𝑀 ∈ 𝑋 → (MEndo‘𝑀) = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩}))
Theorem	mendbas 41912	Base set of the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.)
⊢ 𝐴 = (MEndo‘𝑀)    ⇒   ⊢ (𝑀 LMHom 𝑀) = (Base‘𝐴)
Theorem	mendplusgfval 41913*	Addition in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 31-Oct-2024.)
⊢ 𝐴 = (MEndo‘𝑀)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ + = (+g‘𝑀)    ⇒   ⊢ (+g‘𝐴) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f + 𝑦))
Theorem	mendplusg 41914	A specific addition in the module endomorphism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.)
⊢ 𝐴 = (MEndo‘𝑀)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ + = (+g‘𝑀)    &   ⊢ ✚ = (+g‘𝐴)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ✚ 𝑌) = (𝑋 ∘f + 𝑌))
Theorem	mendmulrfval 41915*	Multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 31-Oct-2024.)
⊢ 𝐴 = (MEndo‘𝑀)    &   ⊢ 𝐵 = (Base‘𝐴)    ⇒   ⊢ (.r‘𝐴) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))
Theorem	mendmulr 41916	A specific multiplication in the module endormoprhism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.)
⊢ 𝐴 = (MEndo‘𝑀)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = (.r‘𝐴)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) = (𝑋 ∘ 𝑌))
Theorem	mendsca 41917	The module endomorphism algebra has the same scalars as the underlying module. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 31-Oct-2024.)
⊢ 𝐴 = (MEndo‘𝑀)    &   ⊢ 𝑆 = (Scalar‘𝑀)    ⇒   ⊢ 𝑆 = (Scalar‘𝐴)
Theorem	mendvscafval 41918*	Scalar multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 31-Oct-2024.)
⊢ 𝐴 = (MEndo‘𝑀)    &   ⊢ · = ( ·𝑠 ‘𝑀)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑆 = (Scalar‘𝑀)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐸 = (Base‘𝑀)    ⇒   ⊢ ( ·𝑠 ‘𝐴) = (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘f · 𝑦))
Theorem	mendvsca 41919	A specific scalar multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.)
⊢ 𝐴 = (MEndo‘𝑀)    &   ⊢ · = ( ·𝑠 ‘𝑀)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑆 = (Scalar‘𝑀)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐸 = (Base‘𝑀)    &   ⊢ ∙ = ( ·𝑠 ‘𝐴)    ⇒   ⊢ ((𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∙ 𝑌) = ((𝐸 × {𝑋}) ∘f · 𝑌))
Theorem	mendring 41920	The module endomorphism algebra is a ring. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐴 = (MEndo‘𝑀)    ⇒   ⊢ (𝑀 ∈ LMod → 𝐴 ∈ Ring)
Theorem	mendlmod 41921	The module endomorphism algebra is a left module. (Contributed by Mario Carneiro, 22-Sep-2015.)
⊢ 𝐴 = (MEndo‘𝑀)    &   ⊢ 𝑆 = (Scalar‘𝑀)    ⇒   ⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝐴 ∈ LMod)
Theorem	mendassa 41922	The module endomorphism algebra is an algebra. (Contributed by Mario Carneiro, 22-Sep-2015.)
⊢ 𝐴 = (MEndo‘𝑀)    &   ⊢ 𝑆 = (Scalar‘𝑀)    ⇒   ⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝐴 ∈ AssAlg)
21.31.47  Cyclic groups and order
Theorem	idomrootle 41923*	No element of an integral domain can have more than 𝑁 𝑁-th roots. (Contributed by Stefan O'Rear, 11-Sep-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑅))    ⇒   ⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → (♯‘{𝑦 ∈ 𝐵 ∣ (𝑁 ↑ 𝑦) = 𝑋}) ≤ 𝑁)
Theorem	idomodle 41924*	Limit on the number of 𝑁-th roots of unity in an integral domain. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (Unit‘𝑅))    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    ⇒   ⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → (♯‘{𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁}) ≤ 𝑁)
Theorem	fiuneneq 41925	Two finite sets of equal size have a union of the same size iff they were equal. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Fin) → ((𝐴 ∪ 𝐵) ≈ 𝐴 ↔ 𝐴 = 𝐵))
Theorem	idomsubgmo 41926*	The units of an integral domain have at most one subgroup of any single finite cardinality. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Revised by NM, 17-Jun-2017.)
⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (Unit‘𝑅))    ⇒   ⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → ∃*𝑦 ∈ (SubGrp‘𝐺)(♯‘𝑦) = 𝑁)
Theorem	proot1mul 41927	Any primitive 𝑁-th root of unity is a multiple of any other. (Contributed by Stefan O'Rear, 2-Nov-2015.)
⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (Unit‘𝑅))    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    ⇒   ⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑋 ∈ (◡𝑂 “ {𝑁}) ∧ 𝑌 ∈ (◡𝑂 “ {𝑁}))) → 𝑋 ∈ (𝐾‘{𝑌}))
Theorem	proot1hash 41928	If an integral domain has a primitive 𝑁-th root of unity, it has exactly (ϕ‘𝑁) of them. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (Unit‘𝑅))    &   ⊢ 𝑂 = (od‘𝐺)    ⇒   ⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ (◡𝑂 “ {𝑁})) → (♯‘(◡𝑂 “ {𝑁})) = (ϕ‘𝑁))
Theorem	proot1ex 41929	The complex field has primitive 𝑁-th roots of unity for all 𝑁. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ 𝐺 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))    &   ⊢ 𝑂 = (od‘𝐺)    ⇒   ⊢ (𝑁 ∈ ℕ → (-1↑𝑐(2 / 𝑁)) ∈ (◡𝑂 “ {𝑁}))
21.31.48  Cyclotomic polynomials
Syntax	ccytp 41930	Syntax for the sequence of cyclotomic polynomials.
class CytP
Definition	df-cytp 41931*	The Nth cyclotomic polynomial is the polynomial which has as its zeros precisely the primitive Nth roots of unity. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ CytP = (𝑛 ∈ ℕ ↦ ((mulGrp‘(Poly1‘ℂfld)) Σg (𝑟 ∈ (◡(od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛}) ↦ ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟)))))
Theorem	isdomn3 41932	Nonzero elements form a multiplicative submonoid of any domain. (Contributed by Stefan O'Rear, 11-Sep-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (mulGrp‘𝑅)    ⇒   ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ Ring ∧ (𝐵 ∖ { 0 }) ∈ (SubMnd‘𝑈)))
Theorem	mon1pid 41933	Monicity and degree of the unit polynomial. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 1 = (1r‘𝑃)    &   ⊢ 𝑀 = (Monic1p‘𝑅)    &   ⊢ 𝐷 = ( deg1 ‘𝑅)    ⇒   ⊢ (𝑅 ∈ NzRing → ( 1 ∈ 𝑀 ∧ (𝐷‘ 1 ) = 0))
Theorem	mon1psubm 41934	Monic polynomials are a multiplicative submonoid. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑀 = (Monic1p‘𝑅)    &   ⊢ 𝑈 = (mulGrp‘𝑃)    ⇒   ⊢ (𝑅 ∈ NzRing → 𝑀 ∈ (SubMnd‘𝑈))
Theorem	deg1mhm 41935	Homomorphic property of the polynomial degree. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ 𝐷 = ( deg1 ‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ 𝑌 = ((mulGrp‘𝑃) ↾s (𝐵 ∖ { 0 }))    &   ⊢ 𝑁 = (ℂfld ↾s ℕ0)    ⇒   ⊢ (𝑅 ∈ Domn → (𝐷 ↾ (𝐵 ∖ { 0 })) ∈ (𝑌 MndHom 𝑁))
Theorem	cytpfn 41936	Functionality of the cyclotomic polynomial sequence. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ CytP Fn ℕ
Theorem	cytpval 41937*	Substitutions for the Nth cyclotomic polynomial. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝑇 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))    &   ⊢ 𝑂 = (od‘𝑇)    &   ⊢ 𝑃 = (Poly1‘ℂfld)    &   ⊢ 𝑋 = (var1‘ℂfld)    &   ⊢ 𝑄 = (mulGrp‘𝑃)    &   ⊢ − = (-g‘𝑃)    &   ⊢ 𝐴 = (algSc‘𝑃)    ⇒   ⊢ (𝑁 ∈ ℕ → (CytP‘𝑁) = (𝑄 Σg (𝑟 ∈ (◡𝑂 “ {𝑁}) ↦ (𝑋 − (𝐴‘𝑟)))))
21.31.49  Miscellaneous topology
Theorem	fgraphopab 41938*	Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐹‘𝑎) = 𝑏)})
Theorem	fgraphxp 41939*	Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 = {𝑥 ∈ (𝐴 × 𝐵) ∣ (𝐹‘(1st ‘𝑥)) = (2nd ‘𝑥)})
Theorem	hausgraph 41940	The graph of a continuous function into a Hausdorff space is closed. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 ∈ (Clsd‘(𝐽 ×t 𝐾)))
Syntax	ctopsep 41941	The class of separable topologies.
class TopSep
Syntax	ctoplnd 41942	The class of Lindelöf topologies.
class TopLnd
Definition	df-topsep 41943*	A topology is separable iff it has a countable dense subset. (Contributed by Stefan O'Rear, 8-Jan-2015.)
⊢ TopSep = {𝑗 ∈ Top ∣ ∃𝑥 ∈ 𝒫 ∪ 𝑗(𝑥 ≼ ω ∧ ((cls‘𝑗)‘𝑥) = ∪ 𝑗)}
Definition	df-toplnd 41944*	A topology is Lindelöf iff every open cover has a countable subcover. (Contributed by Stefan O'Rear, 8-Jan-2015.)
⊢ TopLnd = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ 𝒫 𝑥(𝑧 ≼ ω ∧ ∪ 𝑥 = ∪ 𝑧))}
21.32  Mathbox for Noam Pasman
Theorem	r1sssucd 41945	Deductive form of r1sssuc 9775. (Contributed by Noam Pasman, 19-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ On)    ⇒   ⊢ (𝜑 → (𝑅1‘𝐴) ⊆ (𝑅1‘suc 𝐴))
21.33  Mathbox for Jon Pennant
Theorem	iocunico 41946	Split an open interval into two pieces at point B, Co-author TA. (Contributed by Jon Pennant, 8-Jun-2019.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → ((𝐴(,]𝐵) ∪ (𝐵[,)𝐶)) = (𝐴(,)𝐶))
Theorem	iocinico 41947	The intersection of two sets that meet at a point is that point. (Contributed by Jon Pennant, 12-Jun-2019.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → ((𝐴(,]𝐵) ∩ (𝐵[,)𝐶)) = {𝐵})
Theorem	iocmbl 41948	An open-below, closed-above real interval is measurable. (Contributed by Jon Pennant, 12-Jun-2019.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → (𝐴(,]𝐵) ∈ dom vol)
Theorem	cnioobibld 41949*	A bounded, continuous function on an open bounded interval is integrable. The function must be bounded. For a counterexample, consider 𝐹 = (𝑥 ∈ (0(,)1) ↦ (1 / 𝑥)). See cniccibl 25350 for closed bounded intervals. (Contributed by Jon Pennant, 31-May-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)    ⇒   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)
Theorem	arearect 41950	The area of a rectangle whose sides are parallel to the coordinate axes in (ℝ × ℝ) is its width multiplied by its height. (Contributed by Jon Pennant, 19-Mar-2019.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    &   ⊢ 𝐷 ∈ ℝ    &   ⊢ 𝐴 ≤ 𝐵    &   ⊢ 𝐶 ≤ 𝐷    &   ⊢ 𝑆 = ((𝐴[,]𝐵) × (𝐶[,]𝐷))    ⇒   ⊢ (area‘𝑆) = ((𝐵 − 𝐴) · (𝐷 − 𝐶))
Theorem	areaquad 41951*	The area of a quadrilateral with two sides which are parallel to the y-axis in (ℝ × ℝ) is its width multiplied by the average height of its higher edge minus the average height of its lower edge. Co-author TA. (Contributed by Jon Pennant, 31-May-2019.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    &   ⊢ 𝐷 ∈ ℝ    &   ⊢ 𝐸 ∈ ℝ    &   ⊢ 𝐹 ∈ ℝ    &   ⊢ 𝐴 < 𝐵    &   ⊢ 𝐶 ≤ 𝐸    &   ⊢ 𝐷 ≤ 𝐹    &   ⊢ 𝑈 = (𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)))    &   ⊢ 𝑉 = (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)))    &   ⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))}    ⇒   ⊢ (area‘𝑆) = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵 − 𝐴))
21.34  Mathbox for Richard Penner
21.34.1  Set Theory and Ordinal Numbers
Theorem	uniel 41952*	Two ways to say a union is an element of a class. (Contributed by RP, 27-Jan-2025.)
⊢ (∪ 𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝑦))
Theorem	unielss 41953*	Two ways to say the union of a class is an element of a subclass. (Contributed by RP, 29-Jan-2025.)
⊢ (𝐴 ⊆ 𝐵 → (∪ 𝐵 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥))
Theorem	unielid 41954*	Two ways to say the union of a class is an element of that class. (Contributed by RP, 27-Jan-2025.)
⊢ (∪ 𝐴 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥)
Theorem	ssunib 41955*	Two ways to say a class is a subclass of a union. (Contributed by RP, 27-Jan-2025.)
⊢ (𝐴 ⊆ ∪ 𝐵 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ∈ 𝑦)
Theorem	rp-intrabeq 41956*	Equality theorem for supremum of sets of ordinals. (Contributed by RP, 23-Jan-2025.)
⊢ (𝐴 = 𝐵 → ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥} = ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥})
Theorem	rp-unirabeq 41957*	Equality theorem for infimum of non-empty classes of ordinals. (Contributed by RP, 23-Jan-2025.)
⊢ (𝐴 = 𝐵 → ∪ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} = ∪ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦})
Theorem	onmaxnelsup 41958*	Two ways to say the maximum element of a class of ordinals is also the supremum of that class. (Contributed by RP, 27-Jan-2025.)
⊢ (𝐴 ⊆ On → (¬ 𝐴 ⊆ ∪ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥))
Theorem	onsupneqmaxlim0 41959	If the supremum of a class of ordinals is not in that class, then the supremum is a limit ordinal or empty. (Contributed by RP, 27-Jan-2025.)
⊢ (𝐴 ⊆ On → (𝐴 ⊆ ∪ 𝐴 → ∪ 𝐴 = ∪ ∪ 𝐴))
Theorem	onsupcl2 41960	The supremum of a set of ordinals is an ordinal. (Contributed by RP, 23-Jan-2025.)
⊢ (𝐴 ∈ 𝒫 On → ∪ 𝐴 ∈ On)
Theorem	onuniintrab 41961*	The union of a set of ordinals is the intersection of every ordinal greater-than-or-equal to every member of the set. Closed form of uniordint 7786. (Contributed by RP, 28-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) → ∪ 𝐴 = ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥})
Theorem	onintunirab 41962*	The intersection of a non-empty class of ordinals is the union of every ordinal less-than-or-equal to every element of that class. (Contributed by RP, 29-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∩ 𝐴 = ∪ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦})
Theorem	onsupnmax 41963	If the union of a class of ordinals is not the maximum element of that class, then the union is a limit ordinal or empty. But this isn't a biconditional since 𝐴 could be a non-empty set where a limit ordinal or the empty set happens to be the largest element. (Contributed by RP, 27-Jan-2025.)
⊢ (𝐴 ⊆ On → (¬ ∪ 𝐴 ∈ 𝐴 → ∪ 𝐴 = ∪ ∪ 𝐴))
Theorem	onsupuni 41964	The supremum of a set of ordinals is the union of that set. Lemma 2.10 of [Schloeder] p. 5. (Contributed by RP, 19-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) → sup(𝐴, On, E ) = ∪ 𝐴)
Theorem	onsupuni2 41965	The supremum of a set of ordinals is the union of that set. (Contributed by RP, 22-Jan-2025.)
⊢ (𝐴 ∈ 𝒫 On → sup(𝐴, On, E ) = ∪ 𝐴)
Theorem	onsupintrab 41966*	The supremum of a set of ordinals is the intersection of every ordinal greater-than-or-equal to every member of the set. Definition 2.9 of [Schloeder] p. 5. (Contributed by RP, 23-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) → sup(𝐴, On, E ) = ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥})
Theorem	onsupintrab2 41967*	The supremum of a set of ordinals is the intersection of every ordinal greater-than-or-equal to every member of the set. (Contributed by RP, 23-Jan-2025.)
⊢ (𝐴 ∈ 𝒫 On → sup(𝐴, On, E ) = ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥})
Theorem	onsupcl3 41968*	The supremum of a set of ordinals is an ordinal. (Contributed by RP, 23-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) → ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥} ∈ On)
Theorem	onsupex3 41969*	The supremum of a set of ordinals exists. (Contributed by RP, 23-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) → ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥} ∈ V)
Theorem	onuniintrab2 41970*	The union of a set of ordinals is the intersection of every ordinal greater-than-or-equal to every member of the set. (Contributed by RP, 23-Jan-2025.)
⊢ (𝐴 ∈ 𝒫 On → ∪ 𝐴 = ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥})
Theorem	oninfint 41971	The infimum of a non-empty class of ordinals is the intersection of that class. (Contributed by RP, 23-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → inf(𝐴, On, E ) = ∩ 𝐴)
Theorem	oninfunirab 41972*	The infimum of a non-empty class of ordinals is the union of every ordinal less-than-or-equal to every element of that class. (Contributed by RP, 23-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → inf(𝐴, On, E ) = ∪ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦})
Theorem	oninfcl2 41973*	The infimum of a non-empty class of ordinals is an ordinal. (Contributed by RP, 23-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∪ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ∈ On)
Theorem	onsupmaxb 41974	The union of a class of ordinals is an element is an element of that class if and only if there is a maximum element of that class under the epsilon relation, which is to say that the domain of the restricted epsilon relation is not the whole class. (Contributed by RP, 25-Jan-2025.)
⊢ (𝐴 ⊆ On → (dom ( E ∩ (𝐴 × 𝐴)) = 𝐴 ↔ ¬ ∪ 𝐴 ∈ 𝐴))
Theorem	onexgt 41975*	For any ordinal, there is always a larger ordinal. (Contributed by RP, 1-Feb-2025.)
⊢ (𝐴 ∈ On → ∃𝑥 ∈ On 𝐴 ∈ 𝑥)
Theorem	onexomgt 41976*	For any ordinal, there is always a larger product of omega. (Contributed by RP, 1-Feb-2025.)
⊢ (𝐴 ∈ On → ∃𝑥 ∈ On 𝐴 ∈ (ω ·o 𝑥))
Theorem	omlimcl2 41977	The product of a limit ordinal with any nonzero ordinal is a limit ordinal. (Contributed by RP, 8-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → Lim (𝐵 ·o 𝐴))
Theorem	onexlimgt 41978*	For any ordinal, there is always a larger limit ordinal. (Contributed by RP, 1-Feb-2025.)
⊢ (𝐴 ∈ On → ∃𝑥 ∈ On (Lim 𝑥 ∧ 𝐴 ∈ 𝑥))
Theorem	onexoegt 41979*	For any ordinal, there is always a larger power of omega. (Contributed by RP, 1-Feb-2025.)
⊢ (𝐴 ∈ On → ∃𝑥 ∈ On 𝐴 ∈ (ω ↑o 𝑥))
Theorem	oninfex2 41980*	The infimum of a non-empty class of ordinals exists. (Contributed by RP, 23-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∪ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ∈ V)
Theorem	onsupeqmax 41981*	Condition when the supremum of a set of ordinals is the maximum element of that set. (Contributed by RP, 24-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 ↔ ∪ 𝐴 ∈ 𝐴))
Theorem	onsupeqnmax 41982*	Condition when the supremum of a class of ordinals is not the maximum element of that class. (Contributed by RP, 27-Jan-2025.)
⊢ (𝐴 ⊆ On → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ↔ (∪ 𝐴 = ∪ ∪ 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴)))
Theorem	onsuplub 41983*	The supremum of a set of ordinals is the least upper bound. (Contributed by RP, 27-Jan-2025.)
⊢ (((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) ∧ 𝐵 ∈ On) → (𝐵 ∈ ∪ 𝐴 ↔ ∃𝑧 ∈ 𝐴 𝐵 ∈ 𝑧))
Theorem	onsupnub 41984*	An upper bound of a set of ordinals is not less than the supremum. (Contributed by RP, 27-Jan-2025.)
⊢ (((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ On ∧ ∀𝑧 ∈ 𝐴 𝑧 ⊆ 𝐵)) → ∪ 𝐴 ⊆ 𝐵)
Theorem	onfisupcl 41985	Sufficient condition when the supremum of a set of ordinals is the maximum element of that set. See ordunifi 9290. (Contributed by RP, 27-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) → ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∪ 𝐴 ∈ 𝐴))
Theorem	onelord 41986	Every element of a ordinal is an ordinal. Lemma 1.3 of [Schloeder] p. 1. Based on onelon 6387 and eloni 6372. (Contributed by RP, 15-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → Ord 𝐵)
Theorem	onepsuc 41987	Every ordinal is less than its successor, relationship version. Lemma 1.7 of [Schloeder] p. 1. (Contributed by RP, 15-Jan-2025.)
⊢ (𝐴 ∈ On → 𝐴 E suc 𝐴)
Theorem	epsoon 41988	The ordinals are strictly and completely (linearly) ordered. Theorem 1.9 of [Schloeder] p. 1. Based on epweon 7759 and weso 5667. (Contributed by RP, 15-Jan-2025.)
⊢ E Or On
Theorem	epirron 41989	The strict order on the ordinals is irreflexive. Theorem 1.9(i) of [Schloeder] p. 1. (Contributed by RP, 15-Jan-2025.)
⊢ (𝐴 ∈ On → ¬ 𝐴 E 𝐴)
Theorem	oneptr 41990	The strict order on the ordinals is transitive. Theorem 1.9(ii) of [Schloeder] p. 1. (Contributed by RP, 15-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 E 𝐵 ∧ 𝐵 E 𝐶) → 𝐴 E 𝐶))
Theorem	oneltr 41991	The elementhood relation on the ordinals is transitive. Theorem 1.9(ii) of [Schloeder] p. 1. See ontr1 6408. (Contributed by RP, 15-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))
Theorem	oneptri 41992	The strict, complete (linear) order on the ordinals is complete. Theorem 1.9(iii) of [Schloeder] p. 1. (Contributed by RP, 15-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 E 𝐵 ∨ 𝐵 E 𝐴 ∨ 𝐴 = 𝐵))
Theorem	oneltri 41993	The elementhood relation on the ordinals is complete, so we have triality. Theorem 1.9(iii) of [Schloeder] p. 1. See ordtri3or 6394. (Contributed by RP, 15-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∈ 𝐵 ∨ 𝐵 ∈ 𝐴 ∨ 𝐴 = 𝐵))
Theorem	ordeldif 41994	Membership in the difference of ordinals. (Contributed by RP, 15-Jan-2025.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐶 ∈ (𝐴 ∖ 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐵 ⊆ 𝐶)))
Theorem	ordeldifsucon 41995	Membership in the difference of ordinal and successor ordinal. (Contributed by RP, 16-Jan-2025.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ On) → (𝐶 ∈ (𝐴 ∖ suc 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶)))
Theorem	ordeldif1o 41996	Membership in the difference of ordinal and ordinal one. (Contributed by RP, 16-Jan-2025.)
⊢ (Ord 𝐴 → (𝐵 ∈ (𝐴 ∖ 1o) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 ≠ ∅)))
Theorem	ordne0gt0 41997	Ordinal zero is less than every non-zero ordinal. Theorem 1.10 of [Schloeder] p. 2. Closely related to ord0eln0 6417. (Contributed by RP, 16-Jan-2025.)
⊢ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) → ∅ ∈ 𝐴)
Theorem	ondif1i 41998	Ordinal zero is less than every non-zero ordinal, class difference version. Theorem 1.10 of [Schloeder] p. 2. See ondif1 8498. (Contributed by RP, 16-Jan-2025.)
⊢ (𝐴 ∈ (On ∖ 1o) → ∅ ∈ 𝐴)
Theorem	onsucelab 41999*	The successor of every ordinal is an element of the class of successor ordinals. Definition 1.11 of [Schloeder] p. 2. (Contributed by RP, 16-Jan-2025.)
⊢ (𝐴 ∈ On → suc 𝐴 ∈ {𝑎 ∈ On ∣ ∃𝑏 ∈ On 𝑎 = suc 𝑏})
Theorem	dflim6 42000*	A limit ordinal is a non-zero ordinal which is not a succesor ordinal. Definition 1.11 of [Schloeder] p. 2. (Contributed by RP, 16-Jan-2025.)
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ ¬ ∃𝑏 ∈ On 𝐴 = suc 𝑏))