P. 437 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 43601-43700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	algstr 43601	Lemma to shorten proofs of algbase 43602 through algvsca 43606. (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 43602	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 43603	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 43604	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 43605	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 43606	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 43607*	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 43608	Base set of the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.)
⊢ 𝐴 = (MEndo‘𝑀)    ⇒   ⊢ (𝑀 LMHom 𝑀) = (Base‘𝐴)
Theorem	mendplusgfval 43609*	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 43610	A specific addition in the module endomorphism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.)
⊢ 𝐴 = (MEndo‘𝑀)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ + = (+g‘𝑀)    &   ⊢ ✚ = (+g‘𝐴)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ✚ 𝑌) = (𝑋 ∘f + 𝑌))
Theorem	mendmulrfval 43611*	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 43612	A specific multiplication in the module endormoprhism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.)
⊢ 𝐴 = (MEndo‘𝑀)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = (.r‘𝐴)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) = (𝑋 ∘ 𝑌))
Theorem	mendsca 43613	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 43614*	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 43615	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 43616	The module endomorphism algebra is a ring. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐴 = (MEndo‘𝑀)    ⇒   ⊢ (𝑀 ∈ LMod → 𝐴 ∈ Ring)
Theorem	mendlmod 43617	The module endomorphism algebra is a left module. (Contributed by Mario Carneiro, 22-Sep-2015.)
⊢ 𝐴 = (MEndo‘𝑀)    &   ⊢ 𝑆 = (Scalar‘𝑀)    ⇒   ⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝐴 ∈ LMod)
Theorem	mendassa 43618	The module endomorphism algebra is an algebra. (Contributed by Mario Carneiro, 22-Sep-2015.)
⊢ 𝐴 = (MEndo‘𝑀)    &   ⊢ 𝑆 = (Scalar‘𝑀)    ⇒   ⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝐴 ∈ AssAlg)
21.33.47  Cyclic groups and order
Theorem	idomodle 43619*	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 43620	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 43621*	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 43622	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 43623	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 43624	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.33.48  Cyclotomic polynomials
Syntax	ccytp 43625	Syntax for the sequence of cyclotomic polynomials.
class CytP
Definition	df-cytp 43626*	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	mon1psubm 43627	Monic polynomials are a multiplicative submonoid. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑀 = (Monic1p‘𝑅)    &   ⊢ 𝑈 = (mulGrp‘𝑃)    ⇒   ⊢ (𝑅 ∈ NzRing → 𝑀 ∈ (SubMnd‘𝑈))
Theorem	deg1mhm 43628	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 43629	Functionality of the cyclotomic polynomial sequence. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ CytP Fn ℕ
Theorem	cytpval 43630*	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.33.49  Miscellaneous topology
Theorem	fgraphopab 43631*	Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐹‘𝑎) = 𝑏)})
Theorem	fgraphxp 43632*	Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 = {𝑥 ∈ (𝐴 × 𝐵) ∣ (𝐹‘(1st ‘𝑥)) = (2nd ‘𝑥)})
Theorem	hausgraph 43633	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 43634	The class of separable topologies.
class TopSep
Syntax	ctoplnd 43635	The class of Lindelöf topologies.
class TopLnd
Definition	df-topsep 43636*	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 43637*	A topology is Lindelöf iff every open cover has a countable subcover. (Contributed by Stefan O'Rear, 8-Jan-2015.)
⊢ TopLnd = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ 𝒫 𝑥(𝑧 ≼ ω ∧ ∪ 𝑥 = ∪ 𝑧))}
21.34  Mathbox for Noam Pasman
Theorem	r1sssucd 43638	Deductive form of r1sssuc 9707. (Contributed by Noam Pasman, 19-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ On)    ⇒   ⊢ (𝜑 → (𝑅1‘𝐴) ⊆ (𝑅1‘suc 𝐴))
21.35  Mathbox for Jon Pennant
Theorem	iocunico 43639	Split an open interval into two pieces at point B, Co-author TA. (Contributed by Jon Pennant, 8-Jun-2019.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → ((𝐴(,]𝐵) ∪ (𝐵[,)𝐶)) = (𝐴(,)𝐶))
Theorem	iocinico 43640	The intersection of two sets that meet at a point is that point. (Contributed by Jon Pennant, 12-Jun-2019.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → ((𝐴(,]𝐵) ∩ (𝐵[,)𝐶)) = {𝐵})
Theorem	iocmbl 43641	An open-below, closed-above real interval is measurable. (Contributed by Jon Pennant, 12-Jun-2019.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → (𝐴(,]𝐵) ∈ dom vol)
Theorem	cnioobibld 43642*	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 25808 for closed bounded intervals. (Contributed by Jon Pennant, 31-May-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)    ⇒   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)
Theorem	arearect 43643	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 43644*	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.36  Mathbox for Richard Penner
21.36.1  Set Theory and Ordinal Numbers
Theorem	uniel 43645*	Two ways to say a union is an element of a class. (Contributed by RP, 27-Jan-2025.)
⊢ (∪ 𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝑦))
Theorem	unielss 43646*	Two ways to say the union of a class is an element of a subclass. (Contributed by RP, 29-Jan-2025.)
⊢ (𝐴 ⊆ 𝐵 → (∪ 𝐵 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥))
Theorem	unielid 43647*	Two ways to say the union of a class is an element of that class. (Contributed by RP, 27-Jan-2025.)
⊢ (∪ 𝐴 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥)
Theorem	ssunib 43648*	Two ways to say a class is a subclass of a union. (Contributed by RP, 27-Jan-2025.)
⊢ (𝐴 ⊆ ∪ 𝐵 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ∈ 𝑦)
Theorem	rp-intrabeq 43649*	Equality theorem for supremum of sets of ordinals. (Contributed by RP, 23-Jan-2025.)
⊢ (𝐴 = 𝐵 → ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥} = ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥})
Theorem	rp-unirabeq 43650*	Equality theorem for infimum of non-empty classes of ordinals. (Contributed by RP, 23-Jan-2025.)
⊢ (𝐴 = 𝐵 → ∪ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} = ∪ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦})
Theorem	onmaxnelsup 43651*	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 43652	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 43653	The supremum of a set of ordinals is an ordinal. (Contributed by RP, 23-Jan-2025.)
⊢ (𝐴 ∈ 𝒫 On → ∪ 𝐴 ∈ On)
Theorem	onuniintrab 43654*	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 7755. (Contributed by RP, 28-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) → ∪ 𝐴 = ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥})
Theorem	onintunirab 43655*	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 43656	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 43657	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 43658	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 43659*	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 43660*	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 43661*	The supremum of a set of ordinals is an ordinal. (Contributed by RP, 23-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) → ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥} ∈ On)
Theorem	onsupex3 43662*	The supremum of a set of ordinals exists. (Contributed by RP, 23-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) → ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥} ∈ V)
Theorem	onuniintrab2 43663*	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 43664	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 43665*	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 43666*	The infimum of a non-empty class of ordinals is an ordinal. (Contributed by RP, 23-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∪ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ∈ On)
Theorem	onsupmaxb 43667	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 43668*	For any ordinal, there is always a larger ordinal. (Contributed by RP, 1-Feb-2025.)
⊢ (𝐴 ∈ On → ∃𝑥 ∈ On 𝐴 ∈ 𝑥)
Theorem	onexomgt 43669*	For any ordinal, there is always a larger product of omega. (Contributed by RP, 1-Feb-2025.)
⊢ (𝐴 ∈ On → ∃𝑥 ∈ On 𝐴 ∈ (ω ·o 𝑥))
Theorem	omlimcl2 43670	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 43671*	For any ordinal, there is always a larger limit ordinal. (Contributed by RP, 1-Feb-2025.)
⊢ (𝐴 ∈ On → ∃𝑥 ∈ On (Lim 𝑥 ∧ 𝐴 ∈ 𝑥))
Theorem	onexoegt 43672*	For any ordinal, there is always a larger power of omega. (Contributed by RP, 1-Feb-2025.)
⊢ (𝐴 ∈ On → ∃𝑥 ∈ On 𝐴 ∈ (ω ↑o 𝑥))
Theorem	oninfex2 43673*	The infimum of a non-empty class of ordinals exists. (Contributed by RP, 23-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∪ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ∈ V)
Theorem	onsupeqmax 43674*	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 43675*	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 43676*	The supremum of a set of ordinals is the least upper bound. (Contributed by RP, 27-Jan-2025.)
⊢ (((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) ∧ 𝐵 ∈ On) → (𝐵 ∈ ∪ 𝐴 ↔ ∃𝑧 ∈ 𝐴 𝐵 ∈ 𝑧))
Theorem	onsupnub 43677*	An upper bound of a set of ordinals is not less than the supremum. (Contributed by RP, 27-Jan-2025.)
⊢ (((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ On ∧ ∀𝑧 ∈ 𝐴 𝑧 ⊆ 𝐵)) → ∪ 𝐴 ⊆ 𝐵)
Theorem	onfisupcl 43678	Sufficient condition when the supremum of a set of ordinals is the maximum element of that set. See ordunifi 9200. (Contributed by RP, 27-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) → ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∪ 𝐴 ∈ 𝐴))
Theorem	onelord 43679	Every element of a ordinal is an ordinal. Lemma 1.3 of [Schloeder] p. 1. Based on onelon 6349 and eloni 6334. (Contributed by RP, 15-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → Ord 𝐵)
Theorem	onepsuc 43680	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 43681	The ordinals are strictly and completely (linearly) ordered. Theorem 1.9 of [Schloeder] p. 1. Based on epweon 7729 and weso 5622. (Contributed by RP, 15-Jan-2025.)
⊢ E Or On
Theorem	epirron 43682	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 43683	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 43684	The elementhood relation on the ordinals is transitive. Theorem 1.9(ii) of [Schloeder] p. 1. See ontr1 6371. (Contributed by RP, 15-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))
Theorem	oneptri 43685	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	ordeldif 43686	Membership in the difference of ordinals. (Contributed by RP, 15-Jan-2025.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐶 ∈ (𝐴 ∖ 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐵 ⊆ 𝐶)))
Theorem	ordeldifsucon 43687	Membership in the difference of ordinal and successor ordinal. (Contributed by RP, 16-Jan-2025.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ On) → (𝐶 ∈ (𝐴 ∖ suc 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶)))
Theorem	ordeldif1o 43688	Membership in the difference of ordinal and ordinal one. (Contributed by RP, 16-Jan-2025.)
⊢ (Ord 𝐴 → (𝐵 ∈ (𝐴 ∖ 1o) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 ≠ ∅)))
Theorem	ordne0gt0 43689	Ordinal zero is less than every nonzero ordinal. Theorem 1.10 of [Schloeder] p. 2. Closely related to ord0eln0 6380. (Contributed by RP, 16-Jan-2025.)
⊢ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) → ∅ ∈ 𝐴)
Theorem	ondif1i 43690	Ordinal zero is less than every nonzero ordinal, class difference version. Theorem 1.10 of [Schloeder] p. 2. See ondif1 8436. (Contributed by RP, 16-Jan-2025.)
⊢ (𝐴 ∈ (On ∖ 1o) → ∅ ∈ 𝐴)
Theorem	onsucelab 43691*	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 43692*	A limit ordinal is a nonzero ordinal which is not a successor ordinal. Definition 1.11 of [Schloeder] p. 2. (Contributed by RP, 16-Jan-2025.)
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ ¬ ∃𝑏 ∈ On 𝐴 = suc 𝑏))
Theorem	limnsuc 43693*	A limit ordinal is not an element of the class of successor ordinals. Definition 1.11 of [Schloeder] p. 2. (Contributed by RP, 16-Jan-2025.)
⊢ (Lim 𝐴 → ¬ 𝐴 ∈ {𝑎 ∈ On ∣ ∃𝑏 ∈ On 𝑎 = suc 𝑏})
Theorem	onsucss 43694	If one ordinal is less than another, then the successor of the first is less than or equal to the second. Lemma 1.13 of [Schloeder] p. 2. See ordsucss 7769. (Contributed by RP, 16-Jan-2025.)
⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → suc 𝐵 ⊆ 𝐴))
Theorem	ordnexbtwnsuc 43695*	For any distinct pair of ordinals, if there is no ordinal between the lesser and the greater, the greater is the successor of the lesser. Lemma 1.16 of [Schloeder] p. 2. (Contributed by RP, 16-Jan-2025.)
⊢ ((𝐴 ∈ 𝐵 ∧ Ord 𝐵) → (∀𝑐 ∈ On ¬ (𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵) → 𝐵 = suc 𝐴))
Theorem	orddif0suc 43696	For any distinct pair of ordinals, if the set difference between the greater and the successor of the lesser is empty, the greater is the successor of the lesser. Lemma 1.16 of [Schloeder] p. 2. (Contributed by RP, 17-Jan-2025.)
⊢ ((𝐴 ∈ 𝐵 ∧ Ord 𝐵) → ((𝐵 ∖ suc 𝐴) = ∅ → 𝐵 = suc 𝐴))
Theorem	onsucf1lem 43697*	For ordinals, the successor operation is injective, so there is at most one ordinal that a given ordinal could be the successor of. Lemma 1.17 of [Schloeder] p. 2. (Contributed by RP, 18-Jan-2025.)
⊢ (𝐴 ∈ On → ∃*𝑏 ∈ On 𝐴 = suc 𝑏)
Theorem	onsucf1olem 43698*	The successor operation is bijective between the ordinals and the class of successor ordinals. Lemma 1.17 of [Schloeder] p. 2. (Contributed by RP, 18-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴) → ∃!𝑏 ∈ On 𝐴 = suc 𝑏)
Theorem	onsucrn 43699*	The successor operation is surjective onto its range, the class of successor ordinals. Lemma 1.17 of [Schloeder] p. 2. (Contributed by RP, 18-Jan-2025.)
⊢ 𝐹 = (𝑥 ∈ On ↦ suc 𝑥)    ⇒   ⊢ ran 𝐹 = {𝑎 ∈ On ∣ ∃𝑏 ∈ On 𝑎 = suc 𝑏}
Theorem	onsucf1o 43700*	The successor operation is a bijective function between the ordinals and the class of successor ordinals. Lemma 1.17 of [Schloeder] p. 2. (Contributed by RP, 18-Jan-2025.)
⊢ 𝐹 = (𝑥 ∈ On ↦ suc 𝑥)    ⇒   ⊢ 𝐹:On–1-1-onto→{𝑎 ∈ On ∣ ∃𝑏 ∈ On 𝑎 = suc 𝑏}