P. 96 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 9501-9600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	suplub2 9501*	Bidirectional form of suplub 9500. (Contributed by Mario Carneiro, 6-Sep-2014.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐶𝑅sup(𝐵, 𝐴, 𝑅) ↔ ∃𝑧 ∈ 𝐵 𝐶𝑅𝑧))
Theorem	supnub 9502*	An upper bound is not less than the supremum. (Contributed by NM, 13-Oct-2004.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))    ⇒   ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑧 ∈ 𝐵 ¬ 𝐶𝑅𝑧) → ¬ 𝐶𝑅sup(𝐵, 𝐴, 𝑅)))
Theorem	supex 9503	A supremum is a set. (Contributed by NM, 22-May-1999.)
⊢ 𝑅 Or 𝐴    ⇒   ⊢ sup(𝐵, 𝐴, 𝑅) ∈ V
Theorem	sup00 9504	The supremum under an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020.)
⊢ sup(𝐵, ∅, 𝑅) = ∅
Theorem	sup0riota 9505*	The supremum of an empty set is the smallest element of the base set. (Contributed by AV, 4-Sep-2020.)
⊢ (𝑅 Or 𝐴 → sup(∅, 𝐴, 𝑅) = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑦𝑅𝑥))
Theorem	sup0 9506*	The supremum of an empty set under a base set which has a unique smallest element is the smallest element of the base set. (Contributed by AV, 4-Sep-2020.)
⊢ ((𝑅 Or 𝐴 ∧ (𝑋 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑦𝑅𝑋) ∧ ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑦𝑅𝑥) → sup(∅, 𝐴, 𝑅) = 𝑋)
Theorem	supmax 9507*	The greatest element of a set is its supremum. Note that the converse is not true; the supremum might not be an element of the set considered. (Contributed by Jeff Hoffman, 17-Jun-2008.) (Proof shortened by OpenAI, 30-Mar-2020.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ¬ 𝐶𝑅𝑦)    ⇒   ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = 𝐶)
Theorem	fisup2g 9508*	A finite set satisfies the conditions to have a supremum. (Contributed by Mario Carneiro, 28-Apr-2015.)
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴)) → ∃𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))
Theorem	fisupcl 9509	A nonempty finite set contains its supremum. (Contributed by Jeff Madsen, 9-May-2011.)
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴)) → sup(𝐵, 𝐴, 𝑅) ∈ 𝐵)
Theorem	supgtoreq 9510	The supremum of a finite set is greater than or equal to all the elements of the set. (Contributed by AV, 1-Oct-2019.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 = sup(𝐵, 𝐴, 𝑅))    ⇒   ⊢ (𝜑 → (𝐶𝑅𝑆 ∨ 𝐶 = 𝑆))
Theorem	suppr 9511	The supremum of a pair. (Contributed by NM, 17-Jun-2007.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → sup({𝐵, 𝐶}, 𝐴, 𝑅) = if(𝐶𝑅𝐵, 𝐵, 𝐶))
Theorem	supsn 9512	The supremum of a singleton. (Contributed by NM, 2-Oct-2007.)
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → sup({𝐵}, 𝐴, 𝑅) = 𝐵)
Theorem	supisolem 9513*	Lemma for supiso 9515. (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵))    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝐷 ∈ 𝐴) → ((∀𝑦 ∈ 𝐶 ¬ 𝐷𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝐷 → ∃𝑧 ∈ 𝐶 𝑦𝑅𝑧)) ↔ (∀𝑤 ∈ (𝐹 “ 𝐶) ¬ (𝐹‘𝐷)𝑆𝑤 ∧ ∀𝑤 ∈ 𝐵 (𝑤𝑆(𝐹‘𝐷) → ∃𝑣 ∈ (𝐹 “ 𝐶)𝑤𝑆𝑣))))
Theorem	supisoex 9514*	Lemma for supiso 9515. (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵))    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐶 𝑦𝑅𝑧)))    ⇒   ⊢ (𝜑 → ∃𝑢 ∈ 𝐵 (∀𝑤 ∈ (𝐹 “ 𝐶) ¬ 𝑢𝑆𝑤 ∧ ∀𝑤 ∈ 𝐵 (𝑤𝑆𝑢 → ∃𝑣 ∈ (𝐹 “ 𝐶)𝑤𝑆𝑣)))
Theorem	supiso 9515*	Image of a supremum under an isomorphism. (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵))    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐶 𝑦𝑅𝑧)))    &   ⊢ (𝜑 → 𝑅 Or 𝐴)    ⇒   ⊢ (𝜑 → sup((𝐹 “ 𝐶), 𝐵, 𝑆) = (𝐹‘sup(𝐶, 𝐴, 𝑅)))
Theorem	infeq1 9516	Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.)
⊢ (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))
Theorem	infeq1d 9517	Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))
Theorem	infeq1i 9518	Equality inference for infimum. (Contributed by AV, 2-Sep-2020.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)
Theorem	infeq2 9519	Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.)
⊢ (𝐵 = 𝐶 → inf(𝐴, 𝐵, 𝑅) = inf(𝐴, 𝐶, 𝑅))
Theorem	infeq3 9520	Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.)
⊢ (𝑅 = 𝑆 → inf(𝐴, 𝐵, 𝑅) = inf(𝐴, 𝐵, 𝑆))
Theorem	infeq123d 9521	Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.)
⊢ (𝜑 → 𝐴 = 𝐷)    &   ⊢ (𝜑 → 𝐵 = 𝐸)    &   ⊢ (𝜑 → 𝐶 = 𝐹)    ⇒   ⊢ (𝜑 → inf(𝐴, 𝐵, 𝐶) = inf(𝐷, 𝐸, 𝐹))
Theorem	nfinf 9522	Hypothesis builder for infimum. (Contributed by AV, 2-Sep-2020.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝑅    ⇒   ⊢ Ⅎ𝑥inf(𝐴, 𝐵, 𝑅)
Theorem	infexd 9523	An infimum is a set. (Contributed by AV, 2-Sep-2020.)
⊢ (𝜑 → 𝑅 Or 𝐴)    ⇒   ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) ∈ V)
Theorem	eqinf 9524*	Sufficient condition for an element to be equal to the infimum. (Contributed by AV, 2-Sep-2020.)
⊢ (𝜑 → 𝑅 Or 𝐴)    ⇒   ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝐶 ∧ ∀𝑦 ∈ 𝐴 (𝐶𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)) → inf(𝐵, 𝐴, 𝑅) = 𝐶))
Theorem	eqinfd 9525*	Sufficient condition for an element to be equal to the infimum. (Contributed by AV, 3-Sep-2020.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ¬ 𝑦𝑅𝐶)    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝐶𝑅𝑦)) → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)    ⇒   ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = 𝐶)
Theorem	infval 9526*	Alternate expression for the infimum. (Contributed by AV, 2-Sep-2020.)
⊢ (𝜑 → 𝑅 Or 𝐴)    ⇒   ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = (℩𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))))
Theorem	infcllem 9527*	Lemma for infcl 9528, inflb 9529, infglb 9530, etc. (Contributed by AV, 3-Sep-2020.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦◡𝑅𝑧)))
Theorem	infcl 9528*	An infimum belongs to its base class (closure law). See also inflb 9529 and infglb 9530. (Contributed by AV, 3-Sep-2020.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))    ⇒   ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) ∈ 𝐴)
Theorem	inflb 9529*	An infimum is a lower bound. See also infcl 9528 and infglb 9530. (Contributed by AV, 3-Sep-2020.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))    ⇒   ⊢ (𝜑 → (𝐶 ∈ 𝐵 → ¬ 𝐶𝑅inf(𝐵, 𝐴, 𝑅)))
Theorem	infglb 9530*	An infimum is the greatest lower bound. See also infcl 9528 and inflb 9529. (Contributed by AV, 3-Sep-2020.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))    ⇒   ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ inf(𝐵, 𝐴, 𝑅)𝑅𝐶) → ∃𝑧 ∈ 𝐵 𝑧𝑅𝐶))
Theorem	infglbb 9531*	Bidirectional form of infglb 9530. (Contributed by AV, 3-Sep-2020.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (inf(𝐵, 𝐴, 𝑅)𝑅𝐶 ↔ ∃𝑧 ∈ 𝐵 𝑧𝑅𝐶))
Theorem	infnlb 9532*	A lower bound is not greater than the infimum. (Contributed by AV, 3-Sep-2020.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))    ⇒   ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑧 ∈ 𝐵 ¬ 𝑧𝑅𝐶) → ¬ inf(𝐵, 𝐴, 𝑅)𝑅𝐶))
Theorem	infex 9533	An infimum is a set. (Contributed by AV, 3-Sep-2020.)
⊢ 𝑅 Or 𝐴    ⇒   ⊢ inf(𝐵, 𝐴, 𝑅) ∈ V
Theorem	infmin 9534*	The smallest element of a set is its infimum. Note that the converse is not true; the infimum might not be an element of the set considered. (Contributed by AV, 3-Sep-2020.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ¬ 𝑦𝑅𝐶)    ⇒   ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = 𝐶)
Theorem	infmo 9535*	Any class 𝐵 has at most one infimum in 𝐴 (where 𝑅 is interpreted as 'less than'). (Contributed by AV, 6-Oct-2020.)
⊢ (𝜑 → 𝑅 Or 𝐴)    ⇒   ⊢ (𝜑 → ∃*𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))
Theorem	infeu 9536*	An infimum is unique. (Contributed by AV, 6-Oct-2020.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))
Theorem	fimin2g 9537*	A finite set has a minimum under a total order. (Contributed by AV, 6-Oct-2020.)
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑦𝑅𝑥)
Theorem	fiming 9538*	A finite set has a minimum under a total order. (Contributed by AV, 6-Oct-2020.)
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → 𝑥𝑅𝑦))
Theorem	fiinfg 9539*	Lemma showing existence and closure of infimum of a finite set. (Contributed by AV, 6-Oct-2020.)
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐴 𝑧𝑅𝑦)))
Theorem	fiinf2g 9540*	A finite set satisfies the conditions to have an infimum. (Contributed by AV, 6-Oct-2020.)
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴)) → ∃𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))
Theorem	fiinfcl 9541	A nonempty finite set contains its infimum. (Contributed by AV, 3-Sep-2020.)
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴)) → inf(𝐵, 𝐴, 𝑅) ∈ 𝐵)
Theorem	infltoreq 9542	The infimum of a finite set is less than or equal to all the elements of the set. (Contributed by AV, 4-Sep-2020.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 = inf(𝐵, 𝐴, 𝑅))    ⇒   ⊢ (𝜑 → (𝑆𝑅𝐶 ∨ 𝐶 = 𝑆))
Theorem	infpr 9543	The infimum of a pair. (Contributed by AV, 4-Sep-2020.)
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → inf({𝐵, 𝐶}, 𝐴, 𝑅) = if(𝐵𝑅𝐶, 𝐵, 𝐶))
Theorem	infsupprpr 9544	The infimum of a proper pair is less than the supremum of this pair. (Contributed by AV, 13-Mar-2023.)
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶)) → inf({𝐵, 𝐶}, 𝐴, 𝑅)𝑅sup({𝐵, 𝐶}, 𝐴, 𝑅))
Theorem	infsn 9545	The infimum of a singleton. (Contributed by NM, 2-Oct-2007.)
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → inf({𝐵}, 𝐴, 𝑅) = 𝐵)
Theorem	inf00 9546	The infimum regarding an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020.)
⊢ inf(𝐵, ∅, 𝑅) = ∅
Theorem	infempty 9547*	The infimum of an empty set under a base set which has a unique greatest element is the greatest element of the base set. (Contributed by AV, 4-Sep-2020.)
⊢ ((𝑅 Or 𝐴 ∧ (𝑋 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑋𝑅𝑦) ∧ ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦) → inf(∅, 𝐴, 𝑅) = 𝑋)
Theorem	infiso 9548*	Image of an infimum under an isomorphism. (Contributed by AV, 4-Sep-2020.)
⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵))    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐶 𝑧𝑅𝑦)))    &   ⊢ (𝜑 → 𝑅 Or 𝐴)    ⇒   ⊢ (𝜑 → inf((𝐹 “ 𝐶), 𝐵, 𝑆) = (𝐹‘inf(𝐶, 𝐴, 𝑅)))
2.4.39  Ordinal isomorphism, Hartogs's theorem
Syntax	coi 9549	Extend class definition to include the canonical order isomorphism to an ordinal.
class OrdIso(𝑅, 𝐴)
Definition	df-oi 9550*	Define the canonical order isomorphism from the well-order 𝑅 on 𝐴 to an ordinal. (Contributed by Mario Carneiro, 23-May-2015.)
⊢ OrdIso(𝑅, 𝐴) = if((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴), (recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) ↾ {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡}), ∅)
Theorem	dfoi 9551*	Rewrite df-oi 9550 with abbreviations. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}    &   ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))    &   ⊢ 𝐹 = recs(𝐺)    ⇒   ⊢ OrdIso(𝑅, 𝐴) = if((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴), (𝐹 ↾ {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}), ∅)
Theorem	oieq1 9552	Equality theorem for ordinal isomorphism. (Contributed by Mario Carneiro, 23-May-2015.)
⊢ (𝑅 = 𝑆 → OrdIso(𝑅, 𝐴) = OrdIso(𝑆, 𝐴))
Theorem	oieq2 9553	Equality theorem for ordinal isomorphism. (Contributed by Mario Carneiro, 23-May-2015.)
⊢ (𝐴 = 𝐵 → OrdIso(𝑅, 𝐴) = OrdIso(𝑅, 𝐵))
Theorem	nfoi 9554	Hypothesis builder for ordinal isomorphism. (Contributed by Mario Carneiro, 23-May-2015.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥OrdIso(𝑅, 𝐴)
Theorem	ordiso2 9555	Generalize ordiso 9556 to proper classes. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐴 = 𝐵)
Theorem	ordiso 9556*	Order-isomorphic ordinal numbers are equal. (Contributed by Jeff Hankins, 16-Oct-2009.) (Proof shortened by Mario Carneiro, 24-Jun-2015.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 = 𝐵 ↔ ∃𝑓 𝑓 Isom E , E (𝐴, 𝐵)))
Theorem	ordtypecbv 9557*	Lemma for ordtype 9572. (Contributed by Mario Carneiro, 26-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}    &   ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))    ⇒   ⊢ recs((𝑓 ∈ V ↦ (℩𝑠 ∈ {𝑦 ∈ 𝐴 ∣ ∀𝑖 ∈ ran 𝑓 𝑖𝑅𝑦}∀𝑟 ∈ {𝑦 ∈ 𝐴 ∣ ∀𝑖 ∈ ran 𝑓 𝑖𝑅𝑦} ¬ 𝑟𝑅𝑠))) = 𝐹
Theorem	ordtypelem1 9558*	Lemma for ordtype 9572. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}    &   ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))    &   ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}    &   ⊢ 𝑂 = OrdIso(𝑅, 𝐴)    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    ⇒   ⊢ (𝜑 → 𝑂 = (𝐹 ↾ 𝑇))
Theorem	ordtypelem2 9559*	Lemma for ordtype 9572. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}    &   ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))    &   ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}    &   ⊢ 𝑂 = OrdIso(𝑅, 𝐴)    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    ⇒   ⊢ (𝜑 → Ord 𝑇)
Theorem	ordtypelem3 9560*	Lemma for ordtype 9572. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}    &   ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))    &   ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}    &   ⊢ 𝑂 = OrdIso(𝑅, 𝐴)    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → (𝐹‘𝑀) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣})
Theorem	ordtypelem4 9561*	Lemma for ordtype 9572. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}    &   ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))    &   ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}    &   ⊢ 𝑂 = OrdIso(𝑅, 𝐴)    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    ⇒   ⊢ (𝜑 → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴)
Theorem	ordtypelem5 9562*	Lemma for ordtype 9572. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}    &   ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))    &   ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}    &   ⊢ 𝑂 = OrdIso(𝑅, 𝐴)    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    ⇒   ⊢ (𝜑 → (Ord dom 𝑂 ∧ 𝑂:dom 𝑂⟶𝐴))
Theorem	ordtypelem6 9563*	Lemma for ordtype 9572. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}    &   ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))    &   ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}    &   ⊢ 𝑂 = OrdIso(𝑅, 𝐴)    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝑀 ∈ dom 𝑂) → (𝑁 ∈ 𝑀 → (𝑂‘𝑁)𝑅(𝑂‘𝑀)))
Theorem	ordtypelem7 9564*	Lemma for ordtype 9572. ran 𝑂 is an initial segment of 𝐴 under the well-order 𝑅. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}    &   ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))    &   ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}    &   ⊢ 𝑂 = OrdIso(𝑅, 𝐴)    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    ⇒   ⊢ (((𝜑 ∧ 𝑁 ∈ 𝐴) ∧ 𝑀 ∈ dom 𝑂) → ((𝑂‘𝑀)𝑅𝑁 ∨ 𝑁 ∈ ran 𝑂))
Theorem	ordtypelem8 9565*	Lemma for ordtype 9572. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}    &   ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))    &   ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}    &   ⊢ 𝑂 = OrdIso(𝑅, 𝐴)    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    ⇒   ⊢ (𝜑 → 𝑂 Isom E , 𝑅 (dom 𝑂, ran 𝑂))
Theorem	ordtypelem9 9566*	Lemma for ordtype 9572. Either the function OrdIso is an isomorphism onto all of 𝐴, or OrdIso is not a set, which by oif 9570 implies that either ran 𝑂 ⊆ 𝐴 is a proper class or dom 𝑂 = On. (Contributed by Mario Carneiro, 25-Jun-2015.) (Revised by AV, 28-Jul-2024.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}    &   ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))    &   ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}    &   ⊢ 𝑂 = OrdIso(𝑅, 𝐴)    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴))
Theorem	ordtypelem10 9567*	Lemma for ordtype 9572. Using ax-rep 5279, exclude the possibility that 𝑂 is a proper class and does not enumerate all of 𝐴. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}    &   ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))    &   ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}    &   ⊢ 𝑂 = OrdIso(𝑅, 𝐴)    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    ⇒   ⊢ (𝜑 → 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴))
Theorem	oi0 9568	Definition of the ordinal isomorphism when its arguments are not meaningful. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ (¬ (𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → 𝐹 = ∅)
Theorem	oicl 9569	The order type of the well-order 𝑅 on 𝐴 is an ordinal. (Contributed by Mario Carneiro, 23-May-2015.) (Revised by Mario Carneiro, 25-Jun-2015.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ Ord dom 𝐹
Theorem	oif 9570	The order isomorphism of the well-order 𝑅 on 𝐴 is a function. (Contributed by Mario Carneiro, 23-May-2015.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ 𝐹:dom 𝐹⟶𝐴
Theorem	oiiso2 9571	The order isomorphism of the well-order 𝑅 on 𝐴 is an isomorphism onto ran 𝑂 (which is a subset of 𝐴 by oif 9570). (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → 𝐹 Isom E , 𝑅 (dom 𝐹, ran 𝐹))
Theorem	ordtype 9572	For any set-like well-ordered class, there is an isomorphic ordinal number called its order type. (Contributed by Jeff Hankins, 17-Oct-2009.) (Revised by Mario Carneiro, 25-Jun-2015.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → 𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴))
Theorem	oiiniseg 9573	ran 𝐹 is an initial segment of 𝐴 under the well-order 𝑅. (Contributed by Mario Carneiro, 26-Jun-2015.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑁 ∈ 𝐴 ∧ 𝑀 ∈ dom 𝐹)) → ((𝐹‘𝑀)𝑅𝑁 ∨ 𝑁 ∈ ran 𝐹))
Theorem	ordtype2 9574	For any set-like well-ordered class, if the order isomorphism exists (is a set), then it maps some ordinal onto 𝐴 isomorphically. Otherwise, 𝐹 is a proper class, which implies that either ran 𝐹 ⊆ 𝐴 is a proper class or dom 𝐹 = On. This weak version of ordtype 9572 does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 ∈ V) → 𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴))
Theorem	oiexg 9575	The order isomorphism on a set is a set. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐹 ∈ V)
Theorem	oion 9576	The order type of the well-order 𝑅 on 𝐴 is an ordinal. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 23-May-2015.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑉 → dom 𝐹 ∈ On)
Theorem	oiiso 9577	The order isomorphism of the well-order 𝑅 on 𝐴 is an isomorphism. (Contributed by Mario Carneiro, 23-May-2015.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 We 𝐴) → 𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴))
Theorem	oien 9578	The order type of a well-ordered set is equinumerous to the set. (Contributed by Mario Carneiro, 23-May-2015.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 We 𝐴) → dom 𝐹 ≈ 𝐴)
Theorem	oieu 9579	Uniqueness of the unique ordinal isomorphism. (Contributed by Mario Carneiro, 23-May-2015.) (Revised by Mario Carneiro, 25-Jun-2015.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → ((Ord 𝐵 ∧ 𝐺 Isom E , 𝑅 (𝐵, 𝐴)) ↔ (𝐵 = dom 𝐹 ∧ 𝐺 = 𝐹)))
Theorem	oismo 9580	When 𝐴 is a subclass of On, 𝐹 is a strictly monotone ordinal functions, and it is also complete (it is an isomorphism onto all of 𝐴). The proof avoids ax-rep 5279 (the second statement is trivial under ax-rep 5279). (Contributed by Mario Carneiro, 26-Jun-2015.)
⊢ 𝐹 = OrdIso( E , 𝐴)    ⇒   ⊢ (𝐴 ⊆ On → (Smo 𝐹 ∧ ran 𝐹 = 𝐴))
Theorem	oiid 9581	The order type of an ordinal under the ∈ order is itself, and the order isomorphism is the identity function. (Contributed by Mario Carneiro, 26-Jun-2015.)
⊢ (Ord 𝐴 → OrdIso( E , 𝐴) = ( I ↾ 𝐴))
Theorem	hartogslem1 9582*	Lemma for hartogs 9584. (Contributed by Mario Carneiro, 14-Jan-2013.) (Revised by Mario Carneiro, 15-May-2015.)
⊢ 𝐹 = {⟨𝑟, 𝑦⟩ ∣ (((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}    &   ⊢ 𝑅 = {⟨𝑠, 𝑡⟩ ∣ ∃𝑤 ∈ 𝑦 ∃𝑧 ∈ 𝑦 ((𝑠 = (𝑓‘𝑤) ∧ 𝑡 = (𝑓‘𝑧)) ∧ 𝑤 E 𝑧)}    ⇒   ⊢ (dom 𝐹 ⊆ 𝒫 (𝐴 × 𝐴) ∧ Fun 𝐹 ∧ (𝐴 ∈ 𝑉 → ran 𝐹 = {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴}))
Theorem	hartogslem2 9583*	Lemma for hartogs 9584. (Contributed by Mario Carneiro, 14-Jan-2013.)
⊢ 𝐹 = {⟨𝑟, 𝑦⟩ ∣ (((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}    &   ⊢ 𝑅 = {⟨𝑠, 𝑡⟩ ∣ ∃𝑤 ∈ 𝑦 ∃𝑧 ∈ 𝑦 ((𝑠 = (𝑓‘𝑤) ∧ 𝑡 = (𝑓‘𝑧)) ∧ 𝑤 E 𝑧)}    ⇒   ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ V)
Theorem	hartogs 9584*	The class of ordinals dominated by a given set is an ordinal. A shorter (when taking into account lemmas hartogslem1 9582 and hartogslem2 9583) proof can be given using the axiom of choice, see ondomon 10603. As its label indicates, this result is used to justify the definition of the Hartogs function df-har 9597. (Contributed by Jeff Hankins, 22-Oct-2009.) (Revised by Mario Carneiro, 15-May-2015.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ On)
Theorem	wofib 9585	The only sets which are well-ordered forwards and backwards are finite sets. (Contributed by Mario Carneiro, 30-Jan-2014.) (Revised by Mario Carneiro, 23-May-2015.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) ↔ (𝑅 We 𝐴 ∧ ◡𝑅 We 𝐴))
Theorem	wemaplem1 9586*	Value of the lexicographic order on a sequence space. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    ⇒   ⊢ ((𝑃 ∈ 𝑉 ∧ 𝑄 ∈ 𝑊) → (𝑃𝑇𝑄 ↔ ∃𝑎 ∈ 𝐴 ((𝑃‘𝑎)𝑆(𝑄‘𝑎) ∧ ∀𝑏 ∈ 𝐴 (𝑏𝑅𝑎 → (𝑃‘𝑏) = (𝑄‘𝑏)))))
Theorem	wemaplem2 9587*	Lemma for wemapso 9591. Transitivity. (Contributed by Stefan O'Rear, 17-Jan-2015.) (Revised by AV, 21-Jul-2024.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝑃 ∈ (𝐵 ↑m 𝐴))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m 𝐴))    &   ⊢ (𝜑 → 𝑄 ∈ (𝐵 ↑m 𝐴))    &   ⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝑆 Po 𝐵)    &   ⊢ (𝜑 → 𝑎 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑃‘𝑎)𝑆(𝑋‘𝑎))    &   ⊢ (𝜑 → ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑎 → (𝑃‘𝑐) = (𝑋‘𝑐)))    &   ⊢ (𝜑 → 𝑏 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑋‘𝑏)𝑆(𝑄‘𝑏))    &   ⊢ (𝜑 → ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝑋‘𝑐) = (𝑄‘𝑐)))    ⇒   ⊢ (𝜑 → 𝑃𝑇𝑄)
Theorem	wemaplem3 9588*	Lemma for wemapso 9591. Transitivity. (Contributed by Stefan O'Rear, 17-Jan-2015.) (Revised by AV, 21-Jul-2024.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝑃 ∈ (𝐵 ↑m 𝐴))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m 𝐴))    &   ⊢ (𝜑 → 𝑄 ∈ (𝐵 ↑m 𝐴))    &   ⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝑆 Po 𝐵)    &   ⊢ (𝜑 → 𝑃𝑇𝑋)    &   ⊢ (𝜑 → 𝑋𝑇𝑄)    ⇒   ⊢ (𝜑 → 𝑃𝑇𝑄)
Theorem	wemappo 9589*	Construct lexicographic order on a function space based on a well-ordering of the indices and a total ordering of the values. Without totality on the values or least differing indices, the best we can prove here is a partial order. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by AV, 21-Jul-2024.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    ⇒   ⊢ ((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) → 𝑇 Po (𝐵 ↑m 𝐴))
Theorem	wemapsolem 9590*	Lemma for wemapso 9591. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 21-Jul-2024.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ 𝑈 ⊆ (𝐵 ↑m 𝐴)    &   ⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝑆 Or 𝐵)    &   ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ∃𝑐 ∈ dom (𝑎 ∖ 𝑏)∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐)    ⇒   ⊢ (𝜑 → 𝑇 Or 𝑈)
Theorem	wemapso 9591*	Construct lexicographic order on a function space based on a well-ordering of the indices and a total ordering of the values. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 21-Jul-2024.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) → 𝑇 Or (𝐵 ↑m 𝐴))
Theorem	wemapso2lem 9592*	Lemma for wemapso2 9593. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 1-Jul-2019.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ 𝑈 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍}    ⇒   ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) → 𝑇 Or 𝑈)
Theorem	wemapso2 9593*	An alternative to having a well-order on 𝑅 in wemapso 9591 is to restrict the function set to finitely-supported functions. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 1-Jul-2019.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ 𝑈 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → 𝑇 Or 𝑈)
Theorem	card2on 9594*	The alternate definition of the cardinal of a set given in cardval2 10031 always gives a set, and indeed an ordinal. (Contributed by Mario Carneiro, 14-Jan-2013.)
⊢ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ∈ On
Theorem	card2inf 9595*	The alternate definition of the cardinal of a set given in cardval2 10031 has the curious property that for non-numerable sets (for which ndmfv 6941 yields ∅), it still evaluates to a nonempty set, and indeed it contains ω. (Contributed by Mario Carneiro, 15-Jan-2013.) (Revised by Mario Carneiro, 27-Apr-2015.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (¬ ∃𝑦 ∈ On 𝑦 ≈ 𝐴 → ω ⊆ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴})
2.4.40  Hartogs function
Syntax	char 9596	Class symbol for the Hartogs function.
class har
Definition	df-har 9597*	Define the Hartogs function as mapping a set to the class of ordinals it dominates. That class is an ordinal by hartogs 9584, which is used in harf 9598. The Hartogs number of a set is the least ordinal not dominated by that set. Theorem harval2 10037 proves that the Hartogs function actually gives the Hartogs number for well-orderable sets. The Hartogs number of an ordinal is its cardinal successor. This is proved for finite ordinal in harsucnn 10038. Traditionally, the Hartogs number of a set 𝑋 is written ℵ(𝑋), and its cardinal successor, 𝑋 +; we use functional notation for this, and cannot use the aleph symbol because it is taken for the enumerating function of the infinite initial ordinals df-aleph 9980. Some authors define the Hartogs number of a set to be the least *infinite* ordinal which does not inject into it, thus causing the range to consist only of alephs. We use the simpler definition where the value can be any successor cardinal. (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ har = (𝑥 ∈ V ↦ {𝑦 ∈ On ∣ 𝑦 ≼ 𝑥})
Theorem	harf 9598	Functionality of the Hartogs function. (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ har:V⟶On
Theorem	harcl 9599	Values of the Hartogs function are ordinals (closure of the Hartogs function in the ordinals). (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ (har‘𝑋) ∈ On
Theorem	harval 9600*	Function value of the Hartogs function. (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ (𝑋 ∈ 𝑉 → (har‘𝑋) = {𝑦 ∈ On ∣ 𝑦 ≼ 𝑋})