P. 330 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32901-33000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	wrdres 32901	Condition for the restriction of a word to be a word itself. (Contributed by Thierry Arnoux, 5-Oct-2018.)
⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝑊 ↾ (0..^𝑁)) ∈ Word 𝑆)
Theorem	wrdsplex 32902*	Existence of a split of a word at a given index. (Contributed by Thierry Arnoux, 11-Oct-2018.) (Proof shortened by AV, 3-Nov-2022.)
⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ∃𝑣 ∈ Word 𝑆𝑊 = ((𝑊 ↾ (0..^𝑁)) ++ 𝑣))
Theorem	wrdfsupp 32903	A word has finite support. (Contributed by Thierry Arnoux, 27-May-2025.)
⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑆)    ⇒   ⊢ (𝜑 → 𝑊 finSupp 𝑍)
Theorem	wrdpmcl 32904	Closure of a word with permuted symbols. (Contributed by Thierry Arnoux, 27-May-2025.)
⊢ 𝐽 = (0..^(♯‘𝑊))    &   ⊢ (𝜑 → 𝐸:𝐽–1-1-onto→𝐽)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑆)    ⇒   ⊢ (𝜑 → (𝑊 ∘ 𝐸) ∈ Word 𝑆)
Theorem	pfx1s2 32905	The prefix of length 1 of a length 2 word. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (⟨“𝐴𝐵”⟩ prefix 1) = ⟨“𝐴”⟩)
Theorem	pfxrn2 32906	The range of a prefix of a word is a subset of the range of that word. Stronger version of pfxrn 14733. (Contributed by Thierry Arnoux, 12-Dec-2023.)
⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ran (𝑊 prefix 𝐿) ⊆ ran 𝑊)
Theorem	pfxrn3 32907	Express the range of a prefix of a word. Stronger version of pfxrn2 32906. (Contributed by Thierry Arnoux, 13-Dec-2023.)
⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ran (𝑊 prefix 𝐿) = (𝑊 “ (0..^𝐿)))
Theorem	pfxf1 32908	Condition for a prefix to be injective. (Contributed by Thierry Arnoux, 13-Dec-2023.)
⊢ (𝜑 → 𝑊 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝑆)    &   ⊢ (𝜑 → 𝐿 ∈ (0...(♯‘𝑊)))    ⇒   ⊢ (𝜑 → (𝑊 prefix 𝐿):dom (𝑊 prefix 𝐿)–1-1→𝑆)
Theorem	s1f1 32909	Conditions for a length 1 string to be a one-to-one function. (Contributed by Thierry Arnoux, 11-Dec-2023.)
⊢ (𝜑 → 𝐼 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ⟨“𝐼”⟩:dom ⟨“𝐼”⟩–1-1→𝐷)
Theorem	s2rnOLD 32910	Obsolete version of s2rn 15012 as of 1-Aug-2025. Range of a length 2 string. (Contributed by Thierry Arnoux, 19-Sep-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ran ⟨“𝐼𝐽”⟩ = {𝐼, 𝐽})
Theorem	s2f1 32911	Conditions for a length 2 string to be a one-to-one function. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    ⇒   ⊢ (𝜑 → ⟨“𝐼𝐽”⟩:dom ⟨“𝐼𝐽”⟩–1-1→𝐷)
Theorem	s3rnOLD 32912	Obsolete version of s2rn 15012 as of 1-Aug-2025. Range of a length 3 string. (Contributed by Thierry Arnoux, 19-Sep-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ran ⟨“𝐼𝐽𝐾”⟩ = {𝐼, 𝐽, 𝐾})
Theorem	s3f1 32913	Conditions for a length 3 string to be a one-to-one function. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → 𝐾 ≠ 𝐼)    ⇒   ⊢ (𝜑 → ⟨“𝐼𝐽𝐾”⟩:dom ⟨“𝐼𝐽𝐾”⟩–1-1→𝐷)
Theorem	s3clhash 32914	Closure of the words of length 3 in a preimage using the hash function. (Contributed by Thierry Arnoux, 27-Sep-2023.)
⊢ ⟨“𝐼𝐽𝐾”⟩ ∈ (◡♯ “ {3})
Theorem	ccatf1 32915	Conditions for a concatenation to be injective. (Contributed by Thierry Arnoux, 11-Dec-2023.)
⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝐴:dom 𝐴–1-1→𝑆)    &   ⊢ (𝜑 → 𝐵:dom 𝐵–1-1→𝑆)    &   ⊢ (𝜑 → (ran 𝐴 ∩ ran 𝐵) = ∅)    ⇒   ⊢ (𝜑 → (𝐴 ++ 𝐵):dom (𝐴 ++ 𝐵)–1-1→𝑆)
Theorem	ccatdmss 32916	The domain of a concatenated word is a superset of the domain of the first word. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝜑 → 𝐴 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ Word 𝑆)    ⇒   ⊢ (𝜑 → dom 𝐴 ⊆ dom (𝐴 ++ 𝐵))
Theorem	pfxlsw2ccat 32917	Reconstruct a word from its prefix and its last two symbols. (Contributed by Thierry Arnoux, 26-Sep-2023.)
⊢ 𝑁 = (♯‘𝑊)    ⇒   ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → 𝑊 = ((𝑊 prefix (𝑁 − 2)) ++ ⟨“(𝑊‘(𝑁 − 2))(𝑊‘(𝑁 − 1))”⟩))
Theorem	ccatws1f1o 32918	Conditions for the concatenation of a word and a singleton word to be bijective. (Contributed by Thierry Arnoux, 27-May-2025.)
⊢ 𝑁 = (♯‘𝑇)    &   ⊢ 𝐽 = (0..^(𝑁 + 1))    &   ⊢ (𝜑 → 𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁))    ⇒   ⊢ (𝜑 → (𝑇 ++ ⟨“𝑁”⟩):𝐽–1-1-onto→𝐽)
Theorem	ccatws1f1olast 32919	Two ways to reorder symbols in a word 𝑊 according to permutation 𝑇, and add a last symbol 𝑋. (Contributed by Thierry Arnoux, 27-May-2025.)
⊢ 𝑁 = (♯‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁))    ⇒   ⊢ (𝜑 → ((𝑊 ++ ⟨“𝑋”⟩) ∘ (𝑇 ++ ⟨“𝑁”⟩)) = ((𝑊 ∘ 𝑇) ++ ⟨“𝑋”⟩))
Theorem	wrdt2ind 32920*	Perform an induction over the structure of a word of even length. (Contributed by Thierry Arnoux, 26-Sep-2023.)
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 ++ ⟨“𝑖𝑗”⟩) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ ((𝑦 ∈ Word 𝐵 ∧ 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵) → (𝜒 → 𝜃))    ⇒   ⊢ ((𝐴 ∈ Word 𝐵 ∧ 2 ∥ (♯‘𝐴)) → 𝜏)
Theorem	swrdrn2 32921	The range of a subword is a subset of the range of that word. Stronger version of swrdrn 14700. (Contributed by Thierry Arnoux, 12-Dec-2023.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ran (𝑊 substr ⟨𝑀, 𝑁⟩) ⊆ ran 𝑊)
Theorem	swrdrn3 32922	Express the range of a subword. Stronger version of swrdrn2 32921. (Contributed by Thierry Arnoux, 13-Dec-2023.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ran (𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑊 “ (𝑀..^𝑁)))
Theorem	swrdf1 32923	Condition for a subword to be injective. (Contributed by Thierry Arnoux, 12-Dec-2023.)
⊢ (𝜑 → 𝑊 ∈ Word 𝐷)    &   ⊢ (𝜑 → 𝑀 ∈ (0...𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ (0...(♯‘𝑊)))    &   ⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷)    ⇒   ⊢ (𝜑 → (𝑊 substr ⟨𝑀, 𝑁⟩):dom (𝑊 substr ⟨𝑀, 𝑁⟩)–1-1→𝐷)
Theorem	swrdrndisj 32924	Condition for the range of two subwords of an injective word to be disjoint. (Contributed by Thierry Arnoux, 13-Dec-2023.)
⊢ (𝜑 → 𝑊 ∈ Word 𝐷)    &   ⊢ (𝜑 → 𝑀 ∈ (0...𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ (0...(♯‘𝑊)))    &   ⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷)    &   ⊢ (𝜑 → 𝑂 ∈ (𝑁...𝑃))    &   ⊢ (𝜑 → 𝑃 ∈ (𝑁...(♯‘𝑊)))    ⇒   ⊢ (𝜑 → (ran (𝑊 substr ⟨𝑀, 𝑁⟩) ∩ ran (𝑊 substr ⟨𝑂, 𝑃⟩)) = ∅)
21.3.7.1  Splicing words (substring replacement)
Theorem	splfv3 32925	Symbols to the right of a splice are unaffected. (Contributed by Thierry Arnoux, 14-Dec-2023.)
⊢ (𝜑 → 𝑆 ∈ Word 𝐴)    &   ⊢ (𝜑 → 𝐹 ∈ (0...𝑇))    &   ⊢ (𝜑 → 𝑇 ∈ (0...(♯‘𝑆)))    &   ⊢ (𝜑 → 𝑅 ∈ Word 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ (0..^((♯‘𝑆) − 𝑇)))    &   ⊢ (𝜑 → 𝐾 = (𝐹 + (♯‘𝑅)))    ⇒   ⊢ (𝜑 → ((𝑆 splice ⟨𝐹, 𝑇, 𝑅⟩)‘(𝑋 + 𝐾)) = (𝑆‘(𝑋 + 𝑇)))
21.3.7.2  Cyclic shift of words
Theorem	1cshid 32926	Cyclically shifting a single letter word keeps it unchanged. (Contributed by Thierry Arnoux, 21-Nov-2023.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ (♯‘𝑊) = 1) → (𝑊 cyclShift 𝑁) = 𝑊)
Theorem	cshw1s2 32927	Cyclically shifting a length 2 word swaps its symbols. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (⟨“𝐴𝐵”⟩ cyclShift 1) = ⟨“𝐵𝐴”⟩)
Theorem	cshwrnid 32928	Cyclically shifting a word preserves its range. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → ran (𝑊 cyclShift 𝑁) = ran 𝑊)
Theorem	cshf1o 32929	Condition for the cyclic shift to be a bijection. (Contributed by Thierry Arnoux, 4-Oct-2023.)
⊢ ((𝑊 ∈ Word 𝐷 ∧ 𝑊:dom 𝑊–1-1→𝐷 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁):dom 𝑊–1-1-onto→ran 𝑊)
21.3.8  Extensible Structures
21.3.8.1  Structure restriction operator
Theorem	ressplusf 32930	The group operation function +𝑓 of a structure's restriction is the operation function's restriction to the new base. (Contributed by Thierry Arnoux, 26-Mar-2017.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ ⨣ = (+g‘𝐺)    &   ⊢ ⨣ Fn (𝐵 × 𝐵)    &   ⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ (+𝑓‘𝐻) = ( ⨣ ↾ (𝐴 × 𝐴))
Theorem	ressnm 32931	The norm in a restricted structure. (Contributed by Thierry Arnoux, 8-Oct-2017.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑁 = (norm‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵) → (𝑁 ↾ 𝐴) = (norm‘𝐻))
Theorem	abvpropd2 32932	Weaker version of abvpropd 20858. (Contributed by Thierry Arnoux, 8-Nov-2017.)
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿))    &   ⊢ (𝜑 → (+g‘𝐾) = (+g‘𝐿))    &   ⊢ (𝜑 → (.r‘𝐾) = (.r‘𝐿))    ⇒   ⊢ (𝜑 → (AbsVal‘𝐾) = (AbsVal‘𝐿))
21.3.8.2  The opposite group
Theorem	oppgle 32933	less-than relation of an opposite group. (Contributed by Thierry Arnoux, 13-Apr-2018.)
⊢ 𝑂 = (oppg‘𝑅)    &   ⊢ ≤ = (le‘𝑅)    ⇒   ⊢ ≤ = (le‘𝑂)
Theorem	oppgleOLD 32934	Obsolete version of oppgle 32933 as of 27-Oct-2024. less-than relation of an opposite group. (Contributed by Thierry Arnoux, 13-Apr-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑂 = (oppg‘𝑅)    &   ⊢ ≤ = (le‘𝑅)    ⇒   ⊢ ≤ = (le‘𝑂)
Theorem	oppglt 32935	less-than relation of an opposite group. (Contributed by Thierry Arnoux, 13-Apr-2018.)
⊢ 𝑂 = (oppg‘𝑅)    &   ⊢ < = (lt‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → < = (lt‘𝑂))
21.3.8.3  Posets
Theorem	ressprs 32936	The restriction of a proset is a proset. (Contributed by Thierry Arnoux, 11-Sep-2015.)
⊢ 𝐵 = (Base‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → (𝐾 ↾s 𝐴) ∈ Proset )
Theorem	oduprs 32937	Being a proset is a self-dual property. (Contributed by Thierry Arnoux, 13-Sep-2018.)
⊢ 𝐷 = (ODual‘𝐾)    ⇒   ⊢ (𝐾 ∈ Proset → 𝐷 ∈ Proset )
Theorem	posrasymb 32938	A poset ordering is asymetric. (Contributed by Thierry Arnoux, 13-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) ↔ 𝑋 = 𝑌))
Theorem	resspos 32939	The restriction of a Poset is a Poset. (Contributed by Thierry Arnoux, 20-Jan-2018.)
⊢ ((𝐹 ∈ Poset ∧ 𝐴 ∈ 𝑉) → (𝐹 ↾s 𝐴) ∈ Poset)
Theorem	resstos 32940	The restriction of a Toset is a Toset. (Contributed by Thierry Arnoux, 20-Jan-2018.)
⊢ ((𝐹 ∈ Toset ∧ 𝐴 ∈ 𝑉) → (𝐹 ↾s 𝐴) ∈ Toset)
Theorem	odutos 32941	Being a toset is a self-dual property. (Contributed by Thierry Arnoux, 13-Sep-2018.)
⊢ 𝐷 = (ODual‘𝐾)    ⇒   ⊢ (𝐾 ∈ Toset → 𝐷 ∈ Toset)
Theorem	tlt2 32942	In a Toset, two elements must compare. (Contributed by Thierry Arnoux, 13-Apr-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ∨ 𝑌 < 𝑋))
Theorem	tlt3 32943	In a Toset, two elements must compare strictly, or be equal. (Contributed by Thierry Arnoux, 13-Apr-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 = 𝑌 ∨ 𝑋 < 𝑌 ∨ 𝑌 < 𝑋))
Theorem	trleile 32944	In a Toset, two elements must compare. (Contributed by Thierry Arnoux, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    ⇒   ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ∨ 𝑌 ≤ 𝑋))
Theorem	toslublem 32945*	Lemma for toslub 32946 and xrsclat 32994. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by NM, 15-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ Toset)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑎 ∧ ∀𝑐 ∈ 𝐵 (∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐)) ↔ (∀𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏 ∧ ∀𝑏 ∈ 𝐵 (𝑏 < 𝑎 → ∃𝑑 ∈ 𝐴 𝑏 < 𝑑))))
Theorem	toslub 32946	In a toset, the lowest upper bound lub, defined for partial orders is the supremum, sup(𝐴, 𝐵, < ), defined for total orders. (these are the set.mm definitions: lowest upper bound and supremum are normally synonymous). Note that those two values are also equal if such a supremum does not exist: in that case, both are equal to the empty set. (Contributed by Thierry Arnoux, 15-Feb-2018.) (Revised by Thierry Arnoux, 24-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ Toset)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → ((lub‘𝐾)‘𝐴) = sup(𝐴, 𝐵, < ))
Theorem	tosglblem 32947*	Lemma for tosglb 32948 and xrsclat 32994. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by NM, 15-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ Toset)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((∀𝑏 ∈ 𝐴 𝑎 ≤ 𝑏 ∧ ∀𝑐 ∈ 𝐵 (∀𝑏 ∈ 𝐴 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎)) ↔ (∀𝑏 ∈ 𝐴 ¬ 𝑎◡ < 𝑏 ∧ ∀𝑏 ∈ 𝐵 (𝑏◡ < 𝑎 → ∃𝑑 ∈ 𝐴 𝑏◡ < 𝑑))))
Theorem	tosglb 32948	Same theorem as toslub 32946, for infinimum. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by AV, 28-Sep-2020.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ Toset)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → ((glb‘𝐾)‘𝐴) = inf(𝐴, 𝐵, < ))
21.3.8.4  Complete lattices
Theorem	clatp0cl 32949	The poset zero of a complete lattice belongs to its base. (Contributed by Thierry Arnoux, 17-Feb-2018.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 0 = (0.‘𝑊)    ⇒   ⊢ (𝑊 ∈ CLat → 0 ∈ 𝐵)
Theorem	clatp1cl 32950	The poset one of a complete lattice belongs to its base. (Contributed by Thierry Arnoux, 17-Feb-2018.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 1 = (1.‘𝑊)    ⇒   ⊢ (𝑊 ∈ CLat → 1 ∈ 𝐵)
21.3.8.5  Order Theory
Syntax	cmnt 32951	Extend class notation with monotone functions.
class Monot
Syntax	cmgc 32952	Extend class notation with the monotone Galois connection.
class MGalConn
Definition	df-mnt 32953*	Define a monotone function between two ordered sets. (Contributed by Thierry Arnoux, 20-Apr-2024.)
⊢ Monot = (𝑣 ∈ V, 𝑤 ∈ V ↦ ⦋(Base‘𝑣) / 𝑎⦌{𝑓 ∈ ((Base‘𝑤) ↑m 𝑎) ∣ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑎 (𝑥(le‘𝑣)𝑦 → (𝑓‘𝑥)(le‘𝑤)(𝑓‘𝑦))})
Definition	df-mgc 32954*	Define monotone Galois connections. See mgcval 32960 for an expanded version. (Contributed by Thierry Arnoux, 20-Apr-2024.)
⊢ MGalConn = (𝑣 ∈ V, 𝑤 ∈ V ↦ ⦋(Base‘𝑣) / 𝑎⦌⦋(Base‘𝑤) / 𝑏⦌{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑏 ↑m 𝑎) ∧ 𝑔 ∈ (𝑎 ↑m 𝑏)) ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 ((𝑓‘𝑥)(le‘𝑤)𝑦 ↔ 𝑥(le‘𝑣)(𝑔‘𝑦)))})
Theorem	mntoval 32955*	Operation value of the monotone function. (Contributed by Thierry Arnoux, 23-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝑉Monot𝑊) = {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝑓‘𝑥) ≲ (𝑓‘𝑦))})
Theorem	ismnt 32956*	Express the statement "𝐹 is monotone". (Contributed by Thierry Arnoux, 23-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝐹 ∈ (𝑉Monot𝑊) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))))
Theorem	ismntd 32957	Property of being a monotone increasing function, deduction version. (Contributed by Thierry Arnoux, 24-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑉Monot𝑊))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    ⇒   ⊢ (𝜑 → (𝐹‘𝑋) ≲ (𝐹‘𝑌))
Theorem	mntf 32958	A monotone function is a function. (Contributed by Thierry Arnoux, 24-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ∧ 𝐹 ∈ (𝑉Monot𝑊)) → 𝐹:𝐴⟶𝐵)
Theorem	mgcoval 32959*	Operation value of the monotone Galois connection. (Contributed by Thierry Arnoux, 23-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝑉MGalConn𝑊) = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐵 ↑m 𝐴) ∧ 𝑔 ∈ (𝐴 ↑m 𝐵)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝑓‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝑔‘𝑦)))})
Theorem	mgcval 32960*	Monotone Galois connection between two functions 𝐹 and 𝐺. If this relation is satisfied, 𝐹 is called the lower adjoint of 𝐺, and 𝐺 is called the upper adjoint of 𝐹. Technically, this is implemented as an operation taking a pair of structures 𝑉 and 𝑊, expected to be posets, which gives a relation between pairs of functions 𝐹 and 𝐺. If such a relation exists, it can be proven to be unique. Galois connections generalize the fundamental theorem of Galois theory about the correspondence between subgroups and subfields. (Contributed by Thierry Arnoux, 23-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    ⇒   ⊢ (𝜑 → (𝐹𝐻𝐺 ↔ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝐹‘𝑥) ≲ 𝑦 ↔ 𝑥 ≤ (𝐺‘𝑦)))))
Theorem	mgcf1 32961	The lower adjoint 𝐹 of a Galois connection is a function. (Contributed by Thierry Arnoux, 24-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    ⇒   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
Theorem	mgcf2 32962	The upper adjoint 𝐺 of a Galois connection is a function. (Contributed by Thierry Arnoux, 24-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    ⇒   ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)
Theorem	mgccole1 32963	An inequality for the kernel operator 𝐺 ∘ 𝐹. (Contributed by Thierry Arnoux, 26-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝑋 ≤ (𝐺‘(𝐹‘𝑋)))
Theorem	mgccole2 32964	Inequality for the closure operator (𝐹 ∘ 𝐺) of the Galois connection 𝐻. (Contributed by Thierry Arnoux, 26-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹‘(𝐺‘𝑌)) ≲ 𝑌)
Theorem	mgcmnt1 32965	The lower adjoint 𝐹 of a Galois connection is monotonically increasing. (Contributed by Thierry Arnoux, 26-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    ⇒   ⊢ (𝜑 → (𝐹‘𝑋) ≲ (𝐹‘𝑌))
Theorem	mgcmnt2 32966	The upper adjoint 𝐺 of a Galois connection is monotonically increasing. (Contributed by Thierry Arnoux, 26-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≲ 𝑌)    ⇒   ⊢ (𝜑 → (𝐺‘𝑋) ≤ (𝐺‘𝑌))
Theorem	mgcmntco 32967*	A Galois connection like statement, for two functions with same range. (Contributed by Thierry Arnoux, 26-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    &   ⊢ 𝐶 = (Base‘𝑋)    &   ⊢ < = (le‘𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ Proset )    &   ⊢ (𝜑 → 𝐾 ∈ (𝑉Monot𝑋))    &   ⊢ (𝜑 → 𝐿 ∈ (𝑊Monot𝑋))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (𝐾‘𝑥) < (𝐿‘(𝐹‘𝑥)) ↔ ∀𝑦 ∈ 𝐵 (𝐾‘(𝐺‘𝑦)) < (𝐿‘𝑦)))
Theorem	dfmgc2lem 32968*	Lemma for dfmgc2, backwards direction. (Contributed by Thierry Arnoux, 26-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)))    &   ⊢ (𝜑 → ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ≤ (𝐺‘(𝐹‘𝑥)))    &   ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) → (𝐹‘(𝐺‘𝑢)) ≲ 𝑢)    ⇒   ⊢ (𝜑 → 𝐹𝐻𝐺)
Theorem	dfmgc2 32969*	Alternate definition of the monotone Galois connection. (Contributed by Thierry Arnoux, 26-Apr-2024.)
⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    ⇒   ⊢ (𝜑 → (𝐹𝐻𝐺 ↔ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≲ (𝐹‘𝑦)) ∧ ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 ≲ 𝑣 → (𝐺‘𝑢) ≤ (𝐺‘𝑣))) ∧ (∀𝑢 ∈ 𝐵 (𝐹‘(𝐺‘𝑢)) ≲ 𝑢 ∧ ∀𝑥 ∈ 𝐴 𝑥 ≤ (𝐺‘(𝐹‘𝑥)))))))
Theorem	mgcmnt1d 32970	Galois connection implies monotonicity of the left adjoint. (Contributed by Thierry Arnoux, 21-Jul-2024.)
⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑉Monot𝑊))
Theorem	mgcmnt2d 32971	Galois connection implies monotonicity of the right adjoint. (Contributed by Thierry Arnoux, 21-Jul-2024.)
⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Proset )    &   ⊢ (𝜑 → 𝑊 ∈ Proset )    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    ⇒   ⊢ (𝜑 → 𝐺 ∈ (𝑊Monot𝑉))
Theorem	mgccnv 32972	The inverse Galois connection is the Galois connection of the dual orders. (Contributed by Thierry Arnoux, 26-Apr-2024.)
⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ 𝑀 = ((ODual‘𝑊)MGalConn(ODual‘𝑉))    ⇒   ⊢ ((𝑉 ∈ Proset ∧ 𝑊 ∈ Proset ) → (𝐹𝐻𝐺 ↔ 𝐺𝑀𝐹))
Theorem	pwrssmgc 32973*	Given a function 𝐹, exhibit a Galois connection between subsets of its domain and subsets of its range. (Contributed by Thierry Arnoux, 26-Apr-2024.)
⊢ 𝐺 = (𝑛 ∈ 𝒫 𝑌 ↦ (◡𝐹 “ 𝑛))    &   ⊢ 𝐻 = (𝑚 ∈ 𝒫 𝑋 ↦ {𝑦 ∈ 𝑌 ∣ (◡𝐹 “ {𝑦}) ⊆ 𝑚})    &   ⊢ 𝑉 = (toInc‘𝒫 𝑌)    &   ⊢ 𝑊 = (toInc‘𝒫 𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹:𝑋⟶𝑌)    ⇒   ⊢ (𝜑 → 𝐺(𝑉MGalConn𝑊)𝐻)
Theorem	mgcf1olem1 32974	Property of a Galois connection, lemma for mgcf1o 32976. (Contributed by Thierry Arnoux, 26-Jul-2024.)
⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Poset)    &   ⊢ (𝜑 → 𝑊 ∈ Poset)    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝐹‘(𝐺‘(𝐹‘𝑋))) = (𝐹‘𝑋))
Theorem	mgcf1olem2 32975	Property of a Galois connection, lemma for mgcf1o 32976. (Contributed by Thierry Arnoux, 26-Jul-2024.)
⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Poset)    &   ⊢ (𝜑 → 𝑊 ∈ Poset)    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺‘(𝐹‘(𝐺‘𝑌))) = (𝐺‘𝑌))
Theorem	mgcf1o 32976	Given a Galois connection, exhibit an order isomorphism. (Contributed by Thierry Arnoux, 26-Jul-2024.)
⊢ 𝐻 = (𝑉MGalConn𝑊)    &   ⊢ 𝐴 = (Base‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ ≤ = (le‘𝑉)    &   ⊢ ≲ = (le‘𝑊)    &   ⊢ (𝜑 → 𝑉 ∈ Poset)    &   ⊢ (𝜑 → 𝑊 ∈ Poset)    &   ⊢ (𝜑 → 𝐹𝐻𝐺)    ⇒   ⊢ (𝜑 → (𝐹 ↾ ran 𝐺) Isom ≤ , ≲ (ran 𝐺, ran 𝐹))
21.3.8.6  Chains
Syntax	cchn 32977	Extend class notation with the class of (finite) chains.
class ( < Chain𝐴)
Definition	df-chn 32978*	Define the class of (finite) chains. A chain is defined to be a sequence of objects, where each object is less than the next one in the sequence. The term "chain" is usually used in order theory. In the context of algebra, chains are often called "towers", for example for fields, or "series", for example for subgroup or subnormal series. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ ( < Chain𝐴) = {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}
Theorem	ischn 32979*	Property of being a chain. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝐶 ∈ ( < Chain𝐴) ↔ (𝐶 ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑛 − 1)) < (𝐶‘𝑛)))
Theorem	chnwrd 32980	A chain is an ordered sequence, i.e. a word. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝜑 → 𝐶 ∈ ( < Chain𝐴))    ⇒   ⊢ (𝜑 → 𝐶 ∈ Word 𝐴)
Theorem	chnltm1 32981	Basic property of a chain. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝜑 → 𝐶 ∈ ( < Chain𝐴))    &   ⊢ (𝜑 → 𝑁 ∈ (dom 𝐶 ∖ {0}))    ⇒   ⊢ (𝜑 → (𝐶‘(𝑁 − 1)) < (𝐶‘𝑁))
Theorem	pfxchn 32982	A prefix of a chain is still a chain. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝜑 → 𝐶 ∈ ( < Chain𝐴))    &   ⊢ (𝜑 → 𝐿 ∈ (0...(♯‘𝐶)))    ⇒   ⊢ (𝜑 → (𝐶 prefix 𝐿) ∈ ( < Chain𝐴))
Theorem	chnind 32983*	Induction over a chain. See nnind 12311 for an explanation about the hypotheses. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝑐 = ∅ → (𝜓 ↔ 𝜒))    &   ⊢ (𝑐 = 𝑑 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (𝜓 ↔ 𝜏))    &   ⊢ (𝑐 = 𝐶 → (𝜓 ↔ 𝜂))    &   ⊢ (𝜑 → 𝐶 ∈ ( < Chain𝐴))    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	chnub 32984	In a chain, the last element is an upper bound. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝜑 → < Po 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ ( < Chain𝐴))    &   ⊢ (𝜑 → 𝐼 ∈ (0..^((♯‘𝐶) − 1)))    ⇒   ⊢ (𝜑 → (𝐶‘𝐼) < (lastS‘𝐶))
Theorem	chnlt 32985	Compare any two elements in a chain. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝜑 → < Po 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ ( < Chain𝐴))    &   ⊢ (𝜑 → 𝐽 ∈ (0..^(♯‘𝐶)))    &   ⊢ (𝜑 → 𝐼 ∈ (0..^𝐽))    ⇒   ⊢ (𝜑 → (𝐶‘𝐼) < (𝐶‘𝐽))
Theorem	chnso 32986	A chain induces a total order. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain𝐴)) → < Or ran 𝐶)
21.3.8.7  Extended reals Structure - misc additions
Axiom	ax-xrssca 32987	Assume the scalar component of the extended real structure is the field of the real numbers (this has to be defined in the main body of set.mm). (Contributed by Thierry Arnoux, 22-Oct-2017.)
⊢ ℝfld = (Scalar‘ℝ*𝑠)
Axiom	ax-xrsvsca 32988	Assume the scalar product of the extended real structure is the extended real number multiplication operation (this has to be defined in the main body of set.mm). (Contributed by Thierry Arnoux, 22-Oct-2017.)
⊢ ·e = ( ·𝑠 ‘ℝ*𝑠)
Theorem	xrs0 32989	The zero of the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass 13311 and df-xrs 17562), however it has a zero. (Contributed by Thierry Arnoux, 13-Jun-2017.)
⊢ 0 = (0g‘ℝ*𝑠)
Theorem	xrslt 32990	The "strictly less than" relation for the extended real structure. (Contributed by Thierry Arnoux, 30-Jan-2018.)
⊢ < = (lt‘ℝ*𝑠)
Theorem	xrsinvgval 32991	The inversion operation in the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass 13311 and df-xrs 17562), however it has an inversion operation. (Contributed by Thierry Arnoux, 13-Jun-2017.)
⊢ (𝐵 ∈ ℝ* → ((invg‘ℝ*𝑠)‘𝐵) = -𝑒𝐵)
Theorem	xrsmulgzz 32992	The "multiple" function in the extended real numbers structure. (Contributed by Thierry Arnoux, 14-Jun-2017.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ*) → (𝐴(.g‘ℝ*𝑠)𝐵) = (𝐴 ·e 𝐵))
Theorem	xrstos 32993	The extended real numbers form a toset. (Contributed by Thierry Arnoux, 15-Feb-2018.)
⊢ ℝ*𝑠 ∈ Toset
Theorem	xrsclat 32994	The extended real numbers form a complete lattice. (Contributed by Thierry Arnoux, 15-Feb-2018.)
⊢ ℝ*𝑠 ∈ CLat
Theorem	xrsp0 32995	The poset 0 of the extended real numbers is minus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.) (Proof shortened by AV, 28-Sep-2020.)
⊢ -∞ = (0.‘ℝ*𝑠)
Theorem	xrsp1 32996	The poset 1 of the extended real numbers is plus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.)
⊢ +∞ = (1.‘ℝ*𝑠)
21.3.8.8  The extended nonnegative real numbers commutative monoid
Theorem	xrge0base 32997	The base of the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 30-Jan-2017.)
⊢ (0[,]+∞) = (Base‘(ℝ*𝑠 ↾s (0[,]+∞)))
Theorem	xrge00 32998	The zero of the extended nonnegative real numbers monoid. (Contributed by Thierry Arnoux, 30-Jan-2017.)
⊢ 0 = (0g‘(ℝ*𝑠 ↾s (0[,]+∞)))
Theorem	xrge0plusg 32999	The additive law of the extended nonnegative real numbers monoid is the addition in the extended real numbers. (Contributed by Thierry Arnoux, 20-Mar-2017.)
⊢ +𝑒 = (+g‘(ℝ*𝑠 ↾s (0[,]+∞)))
Theorem	xrge0le 33000	The "less than or equal to" relation in the extended real numbers. (Contributed by Thierry Arnoux, 14-Mar-2018.)
⊢ ≤ = (le‘(ℝ*𝑠 ↾s (0[,]+∞)))