![]() |
Metamath
Proof Explorer Theorem List (p. 95 of 473) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-29860) |
![]() (29861-31383) |
![]() (31384-47242) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sup0riota 9401* | The supremum of an empty set is the smallest element of the base set. (Contributed by AV, 4-Sep-2020.) |
⊢ (𝑅 Or 𝐴 → sup(∅, 𝐴, 𝑅) = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑦𝑅𝑥)) | ||
Theorem | sup0 9402* | 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 9403* | 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 9404* | A finite set satisfies the conditions to have a supremum. (Contributed by Mario Carneiro, 28-Apr-2015.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴)) → ∃𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) | ||
Theorem | fisupcl 9405 | A nonempty finite set contains its supremum. (Contributed by Jeff Madsen, 9-May-2011.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴)) → sup(𝐵, 𝐴, 𝑅) ∈ 𝐵) | ||
Theorem | supgtoreq 9406 | 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 9407 | The supremum of a pair. (Contributed by NM, 17-Jun-2007.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → sup({𝐵, 𝐶}, 𝐴, 𝑅) = if(𝐶𝑅𝐵, 𝐵, 𝐶)) | ||
Theorem | supsn 9408 | The supremum of a singleton. (Contributed by NM, 2-Oct-2007.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → sup({𝐵}, 𝐴, 𝑅) = 𝐵) | ||
Theorem | supisolem 9409* | Lemma for supiso 9411. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝐷 ∈ 𝐴) → ((∀𝑦 ∈ 𝐶 ¬ 𝐷𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝐷 → ∃𝑧 ∈ 𝐶 𝑦𝑅𝑧)) ↔ (∀𝑤 ∈ (𝐹 “ 𝐶) ¬ (𝐹‘𝐷)𝑆𝑤 ∧ ∀𝑤 ∈ 𝐵 (𝑤𝑆(𝐹‘𝐷) → ∃𝑣 ∈ (𝐹 “ 𝐶)𝑤𝑆𝑣)))) | ||
Theorem | supisoex 9410* | Lemma for supiso 9411. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐶 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → ∃𝑢 ∈ 𝐵 (∀𝑤 ∈ (𝐹 “ 𝐶) ¬ 𝑢𝑆𝑤 ∧ ∀𝑤 ∈ 𝐵 (𝑤𝑆𝑢 → ∃𝑣 ∈ (𝐹 “ 𝐶)𝑤𝑆𝑣))) | ||
Theorem | supiso 9411* | Image of a supremum under an isomorphism. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐶 𝑦𝑅𝑧))) & ⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → sup((𝐹 “ 𝐶), 𝐵, 𝑆) = (𝐹‘sup(𝐶, 𝐴, 𝑅))) | ||
Theorem | infeq1 9412 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)) | ||
Theorem | infeq1d 9413 | Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)) | ||
Theorem | infeq1i 9414 | Equality inference for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ 𝐵 = 𝐶 ⇒ ⊢ inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅) | ||
Theorem | infeq2 9415 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝐵 = 𝐶 → inf(𝐴, 𝐵, 𝑅) = inf(𝐴, 𝐶, 𝑅)) | ||
Theorem | infeq3 9416 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝑅 = 𝑆 → inf(𝐴, 𝐵, 𝑅) = inf(𝐴, 𝐵, 𝑆)) | ||
Theorem | infeq123d 9417 | Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝜑 → 𝐴 = 𝐷) & ⊢ (𝜑 → 𝐵 = 𝐸) & ⊢ (𝜑 → 𝐶 = 𝐹) ⇒ ⊢ (𝜑 → inf(𝐴, 𝐵, 𝐶) = inf(𝐷, 𝐸, 𝐹)) | ||
Theorem | nfinf 9418 | Hypothesis builder for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝑅 ⇒ ⊢ Ⅎ𝑥inf(𝐴, 𝐵, 𝑅) | ||
Theorem | infexd 9419 | An infimum is a set. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) ∈ V) | ||
Theorem | eqinf 9420* | Sufficient condition for an element to be equal to the infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝐶 ∧ ∀𝑦 ∈ 𝐴 (𝐶𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)) → inf(𝐵, 𝐴, 𝑅) = 𝐶)) | ||
Theorem | eqinfd 9421* | Sufficient condition for an element to be equal to the infimum. (Contributed by AV, 3-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ¬ 𝑦𝑅𝐶) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝐶𝑅𝑦)) → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦) ⇒ ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = 𝐶) | ||
Theorem | infval 9422* | Alternate expression for the infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = (℩𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))) | ||
Theorem | infcllem 9423* | Lemma for infcl 9424, inflb 9425, infglb 9426, etc. (Contributed by AV, 3-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦◡𝑅𝑧))) | ||
Theorem | infcl 9424* | An infimum belongs to its base class (closure law). See also inflb 9425 and infglb 9426. (Contributed by AV, 3-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) ∈ 𝐴) | ||
Theorem | inflb 9425* | An infimum is a lower bound. See also infcl 9424 and infglb 9426. (Contributed by AV, 3-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → (𝐶 ∈ 𝐵 → ¬ 𝐶𝑅inf(𝐵, 𝐴, 𝑅))) | ||
Theorem | infglb 9426* | An infimum is the greatest lower bound. See also infcl 9424 and inflb 9425. (Contributed by AV, 3-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ inf(𝐵, 𝐴, 𝑅)𝑅𝐶) → ∃𝑧 ∈ 𝐵 𝑧𝑅𝐶)) | ||
Theorem | infglbb 9427* | Bidirectional form of infglb 9426. (Contributed by AV, 3-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (inf(𝐵, 𝐴, 𝑅)𝑅𝐶 ↔ ∃𝑧 ∈ 𝐵 𝑧𝑅𝐶)) | ||
Theorem | infnlb 9428* | A lower bound is not greater than the infimum. (Contributed by AV, 3-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑧 ∈ 𝐵 ¬ 𝑧𝑅𝐶) → ¬ inf(𝐵, 𝐴, 𝑅)𝑅𝐶)) | ||
Theorem | infex 9429 | An infimum is a set. (Contributed by AV, 3-Sep-2020.) |
⊢ 𝑅 Or 𝐴 ⇒ ⊢ inf(𝐵, 𝐴, 𝑅) ∈ V | ||
Theorem | infmin 9430* | 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 9431* | Any class 𝐵 has at most one infimum in 𝐴 (where 𝑅 is interpreted as 'less than'). (Contributed by AV, 6-Oct-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → ∃*𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) | ||
Theorem | infeu 9432* | An infimum is unique. (Contributed by AV, 6-Oct-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → ∃!𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) | ||
Theorem | fimin2g 9433* | A finite set has a minimum under a total order. (Contributed by AV, 6-Oct-2020.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑦𝑅𝑥) | ||
Theorem | fiming 9434* | A finite set has a minimum under a total order. (Contributed by AV, 6-Oct-2020.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → 𝑥𝑅𝑦)) | ||
Theorem | fiinfg 9435* | Lemma showing existence and closure of infimum of a finite set. (Contributed by AV, 6-Oct-2020.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐴 𝑧𝑅𝑦))) | ||
Theorem | fiinf2g 9436* | A finite set satisfies the conditions to have an infimum. (Contributed by AV, 6-Oct-2020.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴)) → ∃𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) | ||
Theorem | fiinfcl 9437 | A nonempty finite set contains its infimum. (Contributed by AV, 3-Sep-2020.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴)) → inf(𝐵, 𝐴, 𝑅) ∈ 𝐵) | ||
Theorem | infltoreq 9438 | 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 9439 | The infimum of a pair. (Contributed by AV, 4-Sep-2020.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → inf({𝐵, 𝐶}, 𝐴, 𝑅) = if(𝐵𝑅𝐶, 𝐵, 𝐶)) | ||
Theorem | infsupprpr 9440 | 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 9441 | The infimum of a singleton. (Contributed by NM, 2-Oct-2007.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → inf({𝐵}, 𝐴, 𝑅) = 𝐵) | ||
Theorem | inf00 9442 | The infimum regarding an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020.) |
⊢ inf(𝐵, ∅, 𝑅) = ∅ | ||
Theorem | infempty 9443* | 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 9444* | Image of an infimum under an isomorphism. (Contributed by AV, 4-Sep-2020.) |
⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐶 𝑧𝑅𝑦))) & ⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → inf((𝐹 “ 𝐶), 𝐵, 𝑆) = (𝐹‘inf(𝐶, 𝐴, 𝑅))) | ||
Syntax | coi 9445 | Extend class definition to include the canonical order isomorphism to an ordinal. |
class OrdIso(𝑅, 𝐴) | ||
Definition | df-oi 9446* | 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 9447* | Rewrite df-oi 9446 with abbreviations. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} & ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) & ⊢ 𝐹 = recs(𝐺) ⇒ ⊢ OrdIso(𝑅, 𝐴) = if((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴), (𝐹 ↾ {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}), ∅) | ||
Theorem | oieq1 9448 | Equality theorem for ordinal isomorphism. (Contributed by Mario Carneiro, 23-May-2015.) |
⊢ (𝑅 = 𝑆 → OrdIso(𝑅, 𝐴) = OrdIso(𝑆, 𝐴)) | ||
Theorem | oieq2 9449 | Equality theorem for ordinal isomorphism. (Contributed by Mario Carneiro, 23-May-2015.) |
⊢ (𝐴 = 𝐵 → OrdIso(𝑅, 𝐴) = OrdIso(𝑅, 𝐵)) | ||
Theorem | nfoi 9450 | Hypothesis builder for ordinal isomorphism. (Contributed by Mario Carneiro, 23-May-2015.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥OrdIso(𝑅, 𝐴) | ||
Theorem | ordiso2 9451 | Generalize ordiso 9452 to proper classes. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐴 = 𝐵) | ||
Theorem | ordiso 9452* | 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 9453* | Lemma for ordtype 9468. (Contributed by Mario Carneiro, 26-Jun-2015.) |
⊢ 𝐹 = recs(𝐺) & ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} & ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) ⇒ ⊢ recs((𝑓 ∈ V ↦ (℩𝑠 ∈ {𝑦 ∈ 𝐴 ∣ ∀𝑖 ∈ ran 𝑓 𝑖𝑅𝑦}∀𝑟 ∈ {𝑦 ∈ 𝐴 ∣ ∀𝑖 ∈ ran 𝑓 𝑖𝑅𝑦} ¬ 𝑟𝑅𝑠))) = 𝐹 | ||
Theorem | ordtypelem1 9454* | Lemma for ordtype 9468. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ 𝐹 = recs(𝐺) & ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} & ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) & ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} & ⊢ 𝑂 = OrdIso(𝑅, 𝐴) & ⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) ⇒ ⊢ (𝜑 → 𝑂 = (𝐹 ↾ 𝑇)) | ||
Theorem | ordtypelem2 9455* | Lemma for ordtype 9468. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ 𝐹 = recs(𝐺) & ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} & ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) & ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} & ⊢ 𝑂 = OrdIso(𝑅, 𝐴) & ⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) ⇒ ⊢ (𝜑 → Ord 𝑇) | ||
Theorem | ordtypelem3 9456* | Lemma for ordtype 9468. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ 𝐹 = recs(𝐺) & ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} & ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) & ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} & ⊢ 𝑂 = OrdIso(𝑅, 𝐴) & ⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → (𝐹‘𝑀) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣}) | ||
Theorem | ordtypelem4 9457* | Lemma for ordtype 9468. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ 𝐹 = recs(𝐺) & ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} & ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) & ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} & ⊢ 𝑂 = OrdIso(𝑅, 𝐴) & ⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) ⇒ ⊢ (𝜑 → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴) | ||
Theorem | ordtypelem5 9458* | Lemma for ordtype 9468. (Contributed by Mario Carneiro, 25-Jun-2015.) |
⊢ 𝐹 = recs(𝐺) & ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} & ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) & ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} & ⊢ 𝑂 = OrdIso(𝑅, 𝐴) & ⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) ⇒ ⊢ (𝜑 → (Ord dom 𝑂 ∧ 𝑂:dom 𝑂⟶𝐴)) | ||
Theorem | ordtypelem6 9459* | Lemma for ordtype 9468. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ 𝐹 = recs(𝐺) & ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} & ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) & ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} & ⊢ 𝑂 = OrdIso(𝑅, 𝐴) & ⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝑀 ∈ dom 𝑂) → (𝑁 ∈ 𝑀 → (𝑂‘𝑁)𝑅(𝑂‘𝑀))) | ||
Theorem | ordtypelem7 9460* | Lemma for ordtype 9468. 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 9461* | Lemma for ordtype 9468. (Contributed by Mario Carneiro, 25-Jun-2015.) |
⊢ 𝐹 = recs(𝐺) & ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} & ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) & ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} & ⊢ 𝑂 = OrdIso(𝑅, 𝐴) & ⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) ⇒ ⊢ (𝜑 → 𝑂 Isom E , 𝑅 (dom 𝑂, ran 𝑂)) | ||
Theorem | ordtypelem9 9462* | Lemma for ordtype 9468. Either the function OrdIso is an isomorphism onto all of 𝐴, or OrdIso is not a set, which by oif 9466 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 9463* | Lemma for ordtype 9468. Using ax-rep 5242, 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 9464 | Definition of the ordinal isomorphism when its arguments are not meaningful. (Contributed by Mario Carneiro, 25-Jun-2015.) |
⊢ 𝐹 = OrdIso(𝑅, 𝐴) ⇒ ⊢ (¬ (𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → 𝐹 = ∅) | ||
Theorem | oicl 9465 | 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 9466 | The order isomorphism of the well-order 𝑅 on 𝐴 is a function. (Contributed by Mario Carneiro, 23-May-2015.) |
⊢ 𝐹 = OrdIso(𝑅, 𝐴) ⇒ ⊢ 𝐹:dom 𝐹⟶𝐴 | ||
Theorem | oiiso2 9467 | The order isomorphism of the well-order 𝑅 on 𝐴 is an isomorphism onto ran 𝑂 (which is a subset of 𝐴 by oif 9466). (Contributed by Mario Carneiro, 25-Jun-2015.) |
⊢ 𝐹 = OrdIso(𝑅, 𝐴) ⇒ ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → 𝐹 Isom E , 𝑅 (dom 𝐹, ran 𝐹)) | ||
Theorem | ordtype 9468 | 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 9469 | ran 𝐹 is an initial segment of 𝐴 under the well-order 𝑅. (Contributed by Mario Carneiro, 26-Jun-2015.) |
⊢ 𝐹 = OrdIso(𝑅, 𝐴) ⇒ ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑁 ∈ 𝐴 ∧ 𝑀 ∈ dom 𝐹)) → ((𝐹‘𝑀)𝑅𝑁 ∨ 𝑁 ∈ ran 𝐹)) | ||
Theorem | ordtype2 9470 | 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 9468 does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 25-Jun-2015.) |
⊢ 𝐹 = OrdIso(𝑅, 𝐴) ⇒ ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 ∈ V) → 𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴)) | ||
Theorem | oiexg 9471 | The order isomorphism on a set is a set. (Contributed by Mario Carneiro, 25-Jun-2015.) |
⊢ 𝐹 = OrdIso(𝑅, 𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐹 ∈ V) | ||
Theorem | oion 9472 | 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 9473 | 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 9474 | 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 9475 | 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 9476 | 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 5242 (the second statement is trivial under ax-rep 5242). (Contributed by Mario Carneiro, 26-Jun-2015.) |
⊢ 𝐹 = OrdIso( E , 𝐴) ⇒ ⊢ (𝐴 ⊆ On → (Smo 𝐹 ∧ ran 𝐹 = 𝐴)) | ||
Theorem | oiid 9477 | 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 9478* | Lemma for hartogs 9480. (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 9479* | Lemma for hartogs 9480. (Contributed by Mario Carneiro, 14-Jan-2013.) |
⊢ 𝐹 = {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} & ⊢ 𝑅 = {〈𝑠, 𝑡〉 ∣ ∃𝑤 ∈ 𝑦 ∃𝑧 ∈ 𝑦 ((𝑠 = (𝑓‘𝑤) ∧ 𝑡 = (𝑓‘𝑧)) ∧ 𝑤 E 𝑧)} ⇒ ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ V) | ||
Theorem | hartogs 9480* | The class of ordinals dominated by a given set is an ordinal. A shorter (when taking into account lemmas hartogslem1 9478 and hartogslem2 9479) proof can be given using the axiom of choice, see ondomon 10499. As its label indicates, this result is used to justify the definition of the Hartogs function df-har 9493. (Contributed by Jeff Hankins, 22-Oct-2009.) (Revised by Mario Carneiro, 15-May-2015.) |
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ On) | ||
Theorem | wofib 9481 | 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 9482* | Value of the lexicographic order on a sequence space. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} ⇒ ⊢ ((𝑃 ∈ 𝑉 ∧ 𝑄 ∈ 𝑊) → (𝑃𝑇𝑄 ↔ ∃𝑎 ∈ 𝐴 ((𝑃‘𝑎)𝑆(𝑄‘𝑎) ∧ ∀𝑏 ∈ 𝐴 (𝑏𝑅𝑎 → (𝑃‘𝑏) = (𝑄‘𝑏))))) | ||
Theorem | wemaplem2 9483* | Lemma for wemapso 9487. Transitivity. (Contributed by Stefan O'Rear, 17-Jan-2015.) (Revised by AV, 21-Jul-2024.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ (𝜑 → 𝑃 ∈ (𝐵 ↑m 𝐴)) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m 𝐴)) & ⊢ (𝜑 → 𝑄 ∈ (𝐵 ↑m 𝐴)) & ⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝑆 Po 𝐵) & ⊢ (𝜑 → 𝑎 ∈ 𝐴) & ⊢ (𝜑 → (𝑃‘𝑎)𝑆(𝑋‘𝑎)) & ⊢ (𝜑 → ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑎 → (𝑃‘𝑐) = (𝑋‘𝑐))) & ⊢ (𝜑 → 𝑏 ∈ 𝐴) & ⊢ (𝜑 → (𝑋‘𝑏)𝑆(𝑄‘𝑏)) & ⊢ (𝜑 → ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝑋‘𝑐) = (𝑄‘𝑐))) ⇒ ⊢ (𝜑 → 𝑃𝑇𝑄) | ||
Theorem | wemaplem3 9484* | Lemma for wemapso 9487. Transitivity. (Contributed by Stefan O'Rear, 17-Jan-2015.) (Revised by AV, 21-Jul-2024.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ (𝜑 → 𝑃 ∈ (𝐵 ↑m 𝐴)) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m 𝐴)) & ⊢ (𝜑 → 𝑄 ∈ (𝐵 ↑m 𝐴)) & ⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝑆 Po 𝐵) & ⊢ (𝜑 → 𝑃𝑇𝑋) & ⊢ (𝜑 → 𝑋𝑇𝑄) ⇒ ⊢ (𝜑 → 𝑃𝑇𝑄) | ||
Theorem | wemappo 9485* |
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 9486* | Lemma for wemapso 9487. (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 9487* | 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 9488* | Lemma for wemapso2 9489. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 1-Jul-2019.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ 𝑈 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍} ⇒ ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) → 𝑇 Or 𝑈) | ||
Theorem | wemapso2 9489* | An alternative to having a well-order on 𝑅 in wemapso 9487 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 9490* | The alternate definition of the cardinal of a set given in cardval2 9927 always gives a set, and indeed an ordinal. (Contributed by Mario Carneiro, 14-Jan-2013.) |
⊢ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ∈ On | ||
Theorem | card2inf 9491* | The alternate definition of the cardinal of a set given in cardval2 9927 has the curious property that for non-numerable sets (for which ndmfv 6877 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 ∣ 𝑥 ≺ 𝐴}) | ||
Syntax | char 9492 | Class symbol for the Hartogs function. |
class har | ||
Definition | df-har 9493* |
Define the Hartogs function as mapping a set to the class of ordinals it
dominates. That class is an ordinal by hartogs 9480, which is used in
harf 9494.
The Hartogs number of a set is the least ordinal not dominated by that set. Theorem harval2 9933 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 9934. 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 9876. 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 9494 | Functionality of the Hartogs function. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ har:V⟶On | ||
Theorem | harcl 9495 | 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 9496* | Function value of the Hartogs function. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ (𝑋 ∈ 𝑉 → (har‘𝑋) = {𝑦 ∈ On ∣ 𝑦 ≼ 𝑋}) | ||
Theorem | elharval 9497 | The Hartogs number of a set contains exactly the ordinals that set dominates. Combined with harcl 9495, this implies that the Hartogs number of a set is greater than all ordinals that set dominates. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 15-May-2015.) |
⊢ (𝑌 ∈ (har‘𝑋) ↔ (𝑌 ∈ On ∧ 𝑌 ≼ 𝑋)) | ||
Theorem | harndom 9498 | The Hartogs number of a set does not inject into that set. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 15-May-2015.) |
⊢ ¬ (har‘𝑋) ≼ 𝑋 | ||
Theorem | harword 9499 | Weak ordering property of the Hartogs function. (Contributed by Stefan O'Rear, 14-Feb-2015.) |
⊢ (𝑋 ≼ 𝑌 → (har‘𝑋) ⊆ (har‘𝑌)) | ||
Syntax | cwdom 9500 | Class symbol for the weak dominance relation. |
class ≼* |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |