![]() |
Metamath
Proof Explorer Theorem List (p. 96 of 485) | < 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-30800) |
![]() (30801-32323) |
![]() (32324-48421) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | infeq1 9501 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)) | ||
Theorem | infeq1d 9502 | Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)) | ||
Theorem | infeq1i 9503 | Equality inference for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ 𝐵 = 𝐶 ⇒ ⊢ inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅) | ||
Theorem | infeq2 9504 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝐵 = 𝐶 → inf(𝐴, 𝐵, 𝑅) = inf(𝐴, 𝐶, 𝑅)) | ||
Theorem | infeq3 9505 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝑅 = 𝑆 → inf(𝐴, 𝐵, 𝑅) = inf(𝐴, 𝐵, 𝑆)) | ||
Theorem | infeq123d 9506 | Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝜑 → 𝐴 = 𝐷) & ⊢ (𝜑 → 𝐵 = 𝐸) & ⊢ (𝜑 → 𝐶 = 𝐹) ⇒ ⊢ (𝜑 → inf(𝐴, 𝐵, 𝐶) = inf(𝐷, 𝐸, 𝐹)) | ||
Theorem | nfinf 9507 | Hypothesis builder for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝑅 ⇒ ⊢ Ⅎ𝑥inf(𝐴, 𝐵, 𝑅) | ||
Theorem | infexd 9508 | An infimum is a set. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) ∈ V) | ||
Theorem | eqinf 9509* | Sufficient condition for an element to be equal to the infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝐶 ∧ ∀𝑦 ∈ 𝐴 (𝐶𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)) → inf(𝐵, 𝐴, 𝑅) = 𝐶)) | ||
Theorem | eqinfd 9510* | Sufficient condition for an element to be equal to the infimum. (Contributed by AV, 3-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ¬ 𝑦𝑅𝐶) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝐶𝑅𝑦)) → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦) ⇒ ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = 𝐶) | ||
Theorem | infval 9511* | Alternate expression for the infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = (℩𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))) | ||
Theorem | infcllem 9512* | Lemma for infcl 9513, inflb 9514, infglb 9515, etc. (Contributed by AV, 3-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦◡𝑅𝑧))) | ||
Theorem | infcl 9513* | An infimum belongs to its base class (closure law). See also inflb 9514 and infglb 9515. (Contributed by AV, 3-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) ∈ 𝐴) | ||
Theorem | inflb 9514* | An infimum is a lower bound. See also infcl 9513 and infglb 9515. (Contributed by AV, 3-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → (𝐶 ∈ 𝐵 → ¬ 𝐶𝑅inf(𝐵, 𝐴, 𝑅))) | ||
Theorem | infglb 9515* | An infimum is the greatest lower bound. See also infcl 9513 and inflb 9514. (Contributed by AV, 3-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ inf(𝐵, 𝐴, 𝑅)𝑅𝐶) → ∃𝑧 ∈ 𝐵 𝑧𝑅𝐶)) | ||
Theorem | infglbb 9516* | Bidirectional form of infglb 9515. (Contributed by AV, 3-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (inf(𝐵, 𝐴, 𝑅)𝑅𝐶 ↔ ∃𝑧 ∈ 𝐵 𝑧𝑅𝐶)) | ||
Theorem | infnlb 9517* | A lower bound is not greater than the infimum. (Contributed by AV, 3-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑧 ∈ 𝐵 ¬ 𝑧𝑅𝐶) → ¬ inf(𝐵, 𝐴, 𝑅)𝑅𝐶)) | ||
Theorem | infex 9518 | An infimum is a set. (Contributed by AV, 3-Sep-2020.) |
⊢ 𝑅 Or 𝐴 ⇒ ⊢ inf(𝐵, 𝐴, 𝑅) ∈ V | ||
Theorem | infmin 9519* | 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 9520* | Any class 𝐵 has at most one infimum in 𝐴 (where 𝑅 is interpreted as 'less than'). (Contributed by AV, 6-Oct-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → ∃*𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) | ||
Theorem | infeu 9521* | An infimum is unique. (Contributed by AV, 6-Oct-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → ∃!𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) | ||
Theorem | fimin2g 9522* | A finite set has a minimum under a total order. (Contributed by AV, 6-Oct-2020.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑦𝑅𝑥) | ||
Theorem | fiming 9523* | A finite set has a minimum under a total order. (Contributed by AV, 6-Oct-2020.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → 𝑥𝑅𝑦)) | ||
Theorem | fiinfg 9524* | Lemma showing existence and closure of infimum of a finite set. (Contributed by AV, 6-Oct-2020.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐴 𝑧𝑅𝑦))) | ||
Theorem | fiinf2g 9525* | A finite set satisfies the conditions to have an infimum. (Contributed by AV, 6-Oct-2020.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴)) → ∃𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) | ||
Theorem | fiinfcl 9526 | A nonempty finite set contains its infimum. (Contributed by AV, 3-Sep-2020.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴)) → inf(𝐵, 𝐴, 𝑅) ∈ 𝐵) | ||
Theorem | infltoreq 9527 | 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 9528 | The infimum of a pair. (Contributed by AV, 4-Sep-2020.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → inf({𝐵, 𝐶}, 𝐴, 𝑅) = if(𝐵𝑅𝐶, 𝐵, 𝐶)) | ||
Theorem | infsupprpr 9529 | 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 9530 | The infimum of a singleton. (Contributed by NM, 2-Oct-2007.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → inf({𝐵}, 𝐴, 𝑅) = 𝐵) | ||
Theorem | inf00 9531 | The infimum regarding an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020.) |
⊢ inf(𝐵, ∅, 𝑅) = ∅ | ||
Theorem | infempty 9532* | 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 9533* | Image of an infimum under an isomorphism. (Contributed by AV, 4-Sep-2020.) |
⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐶 𝑧𝑅𝑦))) & ⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → inf((𝐹 “ 𝐶), 𝐵, 𝑆) = (𝐹‘inf(𝐶, 𝐴, 𝑅))) | ||
Syntax | coi 9534 | Extend class definition to include the canonical order isomorphism to an ordinal. |
class OrdIso(𝑅, 𝐴) | ||
Definition | df-oi 9535* | 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 9536* | Rewrite df-oi 9535 with abbreviations. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} & ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) & ⊢ 𝐹 = recs(𝐺) ⇒ ⊢ OrdIso(𝑅, 𝐴) = if((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴), (𝐹 ↾ {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}), ∅) | ||
Theorem | oieq1 9537 | Equality theorem for ordinal isomorphism. (Contributed by Mario Carneiro, 23-May-2015.) |
⊢ (𝑅 = 𝑆 → OrdIso(𝑅, 𝐴) = OrdIso(𝑆, 𝐴)) | ||
Theorem | oieq2 9538 | Equality theorem for ordinal isomorphism. (Contributed by Mario Carneiro, 23-May-2015.) |
⊢ (𝐴 = 𝐵 → OrdIso(𝑅, 𝐴) = OrdIso(𝑅, 𝐵)) | ||
Theorem | nfoi 9539 | Hypothesis builder for ordinal isomorphism. (Contributed by Mario Carneiro, 23-May-2015.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥OrdIso(𝑅, 𝐴) | ||
Theorem | ordiso2 9540 | Generalize ordiso 9541 to proper classes. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐴 = 𝐵) | ||
Theorem | ordiso 9541* | 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 9542* | Lemma for ordtype 9557. (Contributed by Mario Carneiro, 26-Jun-2015.) |
⊢ 𝐹 = recs(𝐺) & ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} & ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) ⇒ ⊢ recs((𝑓 ∈ V ↦ (℩𝑠 ∈ {𝑦 ∈ 𝐴 ∣ ∀𝑖 ∈ ran 𝑓 𝑖𝑅𝑦}∀𝑟 ∈ {𝑦 ∈ 𝐴 ∣ ∀𝑖 ∈ ran 𝑓 𝑖𝑅𝑦} ¬ 𝑟𝑅𝑠))) = 𝐹 | ||
Theorem | ordtypelem1 9543* | Lemma for ordtype 9557. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ 𝐹 = recs(𝐺) & ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} & ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) & ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} & ⊢ 𝑂 = OrdIso(𝑅, 𝐴) & ⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) ⇒ ⊢ (𝜑 → 𝑂 = (𝐹 ↾ 𝑇)) | ||
Theorem | ordtypelem2 9544* | Lemma for ordtype 9557. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ 𝐹 = recs(𝐺) & ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} & ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) & ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} & ⊢ 𝑂 = OrdIso(𝑅, 𝐴) & ⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) ⇒ ⊢ (𝜑 → Ord 𝑇) | ||
Theorem | ordtypelem3 9545* | Lemma for ordtype 9557. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ 𝐹 = recs(𝐺) & ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} & ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) & ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} & ⊢ 𝑂 = OrdIso(𝑅, 𝐴) & ⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → (𝐹‘𝑀) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣}) | ||
Theorem | ordtypelem4 9546* | Lemma for ordtype 9557. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ 𝐹 = recs(𝐺) & ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} & ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) & ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} & ⊢ 𝑂 = OrdIso(𝑅, 𝐴) & ⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) ⇒ ⊢ (𝜑 → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴) | ||
Theorem | ordtypelem5 9547* | Lemma for ordtype 9557. (Contributed by Mario Carneiro, 25-Jun-2015.) |
⊢ 𝐹 = recs(𝐺) & ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} & ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) & ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} & ⊢ 𝑂 = OrdIso(𝑅, 𝐴) & ⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) ⇒ ⊢ (𝜑 → (Ord dom 𝑂 ∧ 𝑂:dom 𝑂⟶𝐴)) | ||
Theorem | ordtypelem6 9548* | Lemma for ordtype 9557. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ 𝐹 = recs(𝐺) & ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} & ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) & ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} & ⊢ 𝑂 = OrdIso(𝑅, 𝐴) & ⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝑀 ∈ dom 𝑂) → (𝑁 ∈ 𝑀 → (𝑂‘𝑁)𝑅(𝑂‘𝑀))) | ||
Theorem | ordtypelem7 9549* | Lemma for ordtype 9557. 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 9550* | Lemma for ordtype 9557. (Contributed by Mario Carneiro, 25-Jun-2015.) |
⊢ 𝐹 = recs(𝐺) & ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} & ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) & ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} & ⊢ 𝑂 = OrdIso(𝑅, 𝐴) & ⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) ⇒ ⊢ (𝜑 → 𝑂 Isom E , 𝑅 (dom 𝑂, ran 𝑂)) | ||
Theorem | ordtypelem9 9551* | Lemma for ordtype 9557. Either the function OrdIso is an isomorphism onto all of 𝐴, or OrdIso is not a set, which by oif 9555 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 9552* | Lemma for ordtype 9557. Using ax-rep 5286, 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 9553 | Definition of the ordinal isomorphism when its arguments are not meaningful. (Contributed by Mario Carneiro, 25-Jun-2015.) |
⊢ 𝐹 = OrdIso(𝑅, 𝐴) ⇒ ⊢ (¬ (𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → 𝐹 = ∅) | ||
Theorem | oicl 9554 | 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 9555 | The order isomorphism of the well-order 𝑅 on 𝐴 is a function. (Contributed by Mario Carneiro, 23-May-2015.) |
⊢ 𝐹 = OrdIso(𝑅, 𝐴) ⇒ ⊢ 𝐹:dom 𝐹⟶𝐴 | ||
Theorem | oiiso2 9556 | The order isomorphism of the well-order 𝑅 on 𝐴 is an isomorphism onto ran 𝑂 (which is a subset of 𝐴 by oif 9555). (Contributed by Mario Carneiro, 25-Jun-2015.) |
⊢ 𝐹 = OrdIso(𝑅, 𝐴) ⇒ ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → 𝐹 Isom E , 𝑅 (dom 𝐹, ran 𝐹)) | ||
Theorem | ordtype 9557 | 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 9558 | ran 𝐹 is an initial segment of 𝐴 under the well-order 𝑅. (Contributed by Mario Carneiro, 26-Jun-2015.) |
⊢ 𝐹 = OrdIso(𝑅, 𝐴) ⇒ ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑁 ∈ 𝐴 ∧ 𝑀 ∈ dom 𝐹)) → ((𝐹‘𝑀)𝑅𝑁 ∨ 𝑁 ∈ ran 𝐹)) | ||
Theorem | ordtype2 9559 | 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 9557 does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 25-Jun-2015.) |
⊢ 𝐹 = OrdIso(𝑅, 𝐴) ⇒ ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 ∈ V) → 𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴)) | ||
Theorem | oiexg 9560 | The order isomorphism on a set is a set. (Contributed by Mario Carneiro, 25-Jun-2015.) |
⊢ 𝐹 = OrdIso(𝑅, 𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐹 ∈ V) | ||
Theorem | oion 9561 | 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 9562 | 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 9563 | 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 9564 | 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 9565 | 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 5286 (the second statement is trivial under ax-rep 5286). (Contributed by Mario Carneiro, 26-Jun-2015.) |
⊢ 𝐹 = OrdIso( E , 𝐴) ⇒ ⊢ (𝐴 ⊆ On → (Smo 𝐹 ∧ ran 𝐹 = 𝐴)) | ||
Theorem | oiid 9566 | 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 9567* | Lemma for hartogs 9569. (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 9568* | Lemma for hartogs 9569. (Contributed by Mario Carneiro, 14-Jan-2013.) |
⊢ 𝐹 = {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} & ⊢ 𝑅 = {〈𝑠, 𝑡〉 ∣ ∃𝑤 ∈ 𝑦 ∃𝑧 ∈ 𝑦 ((𝑠 = (𝑓‘𝑤) ∧ 𝑡 = (𝑓‘𝑧)) ∧ 𝑤 E 𝑧)} ⇒ ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ V) | ||
Theorem | hartogs 9569* | The class of ordinals dominated by a given set is an ordinal. A shorter (when taking into account lemmas hartogslem1 9567 and hartogslem2 9568) proof can be given using the axiom of choice, see ondomon 10588. As its label indicates, this result is used to justify the definition of the Hartogs function df-har 9582. (Contributed by Jeff Hankins, 22-Oct-2009.) (Revised by Mario Carneiro, 15-May-2015.) |
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ On) | ||
Theorem | wofib 9570 | 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 9571* | Value of the lexicographic order on a sequence space. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} ⇒ ⊢ ((𝑃 ∈ 𝑉 ∧ 𝑄 ∈ 𝑊) → (𝑃𝑇𝑄 ↔ ∃𝑎 ∈ 𝐴 ((𝑃‘𝑎)𝑆(𝑄‘𝑎) ∧ ∀𝑏 ∈ 𝐴 (𝑏𝑅𝑎 → (𝑃‘𝑏) = (𝑄‘𝑏))))) | ||
Theorem | wemaplem2 9572* | Lemma for wemapso 9576. Transitivity. (Contributed by Stefan O'Rear, 17-Jan-2015.) (Revised by AV, 21-Jul-2024.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ (𝜑 → 𝑃 ∈ (𝐵 ↑m 𝐴)) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m 𝐴)) & ⊢ (𝜑 → 𝑄 ∈ (𝐵 ↑m 𝐴)) & ⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝑆 Po 𝐵) & ⊢ (𝜑 → 𝑎 ∈ 𝐴) & ⊢ (𝜑 → (𝑃‘𝑎)𝑆(𝑋‘𝑎)) & ⊢ (𝜑 → ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑎 → (𝑃‘𝑐) = (𝑋‘𝑐))) & ⊢ (𝜑 → 𝑏 ∈ 𝐴) & ⊢ (𝜑 → (𝑋‘𝑏)𝑆(𝑄‘𝑏)) & ⊢ (𝜑 → ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝑋‘𝑐) = (𝑄‘𝑐))) ⇒ ⊢ (𝜑 → 𝑃𝑇𝑄) | ||
Theorem | wemaplem3 9573* | Lemma for wemapso 9576. Transitivity. (Contributed by Stefan O'Rear, 17-Jan-2015.) (Revised by AV, 21-Jul-2024.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ (𝜑 → 𝑃 ∈ (𝐵 ↑m 𝐴)) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m 𝐴)) & ⊢ (𝜑 → 𝑄 ∈ (𝐵 ↑m 𝐴)) & ⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝑆 Po 𝐵) & ⊢ (𝜑 → 𝑃𝑇𝑋) & ⊢ (𝜑 → 𝑋𝑇𝑄) ⇒ ⊢ (𝜑 → 𝑃𝑇𝑄) | ||
Theorem | wemappo 9574* |
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 9575* | Lemma for wemapso 9576. (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 9576* | 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 9577* | Lemma for wemapso2 9578. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 1-Jul-2019.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ 𝑈 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍} ⇒ ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) → 𝑇 Or 𝑈) | ||
Theorem | wemapso2 9578* | An alternative to having a well-order on 𝑅 in wemapso 9576 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 9579* | The alternate definition of the cardinal of a set given in cardval2 10016 always gives a set, and indeed an ordinal. (Contributed by Mario Carneiro, 14-Jan-2013.) |
⊢ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ∈ On | ||
Theorem | card2inf 9580* | The alternate definition of the cardinal of a set given in cardval2 10016 has the curious property that for non-numerable sets (for which ndmfv 6931 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 9581 | Class symbol for the Hartogs function. |
class har | ||
Definition | df-har 9582* |
Define the Hartogs function as mapping a set to the class of ordinals it
dominates. That class is an ordinal by hartogs 9569, which is used in
harf 9583.
The Hartogs number of a set is the least ordinal not dominated by that set. Theorem harval2 10022 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 10023. 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 9965. 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 9583 | Functionality of the Hartogs function. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ har:V⟶On | ||
Theorem | harcl 9584 | 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 9585* | Function value of the Hartogs function. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ (𝑋 ∈ 𝑉 → (har‘𝑋) = {𝑦 ∈ On ∣ 𝑦 ≼ 𝑋}) | ||
Theorem | elharval 9586 | The Hartogs number of a set contains exactly the ordinals that set dominates. Combined with harcl 9584, 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 9587 | 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 9588 | Weak ordering property of the Hartogs function. (Contributed by Stefan O'Rear, 14-Feb-2015.) |
⊢ (𝑋 ≼ 𝑌 → (har‘𝑋) ⊆ (har‘𝑌)) | ||
Syntax | cwdom 9589 | Class symbol for the weak dominance relation. |
class ≼* | ||
Definition | df-wdom 9590* | A set is weakly dominated by a "larger" set if the "larger" set can be mapped onto the "smaller" set or the smaller set is empty, or equivalently, if the smaller set can be placed into bijection with some partition of the larger set. Dominance (df-dom 8966) implies weak dominance (over ZF). The principle asserting the converse is known as the partition principle and is independent of ZF. Theorem fodom 10548 proves that the axiom of choice implies the partition principle (over ZF). It is not known whether the partition principle is equivalent to the axiom of choice (over ZF), although it is know to imply dependent choice. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ ≼* = {〈𝑥, 𝑦〉 ∣ (𝑥 = ∅ ∨ ∃𝑧 𝑧:𝑦–onto→𝑥)} | ||
Theorem | relwdom 9591 | Weak dominance is a relation. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ Rel ≼* | ||
Theorem | brwdom 9592* | Property of weak dominance (definitional form). (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ (𝑌 ∈ 𝑉 → (𝑋 ≼* 𝑌 ↔ (𝑋 = ∅ ∨ ∃𝑧 𝑧:𝑌–onto→𝑋))) | ||
Theorem | brwdomi 9593* | Property of weak dominance, forward direction only. (Contributed by Mario Carneiro, 5-May-2015.) |
⊢ (𝑋 ≼* 𝑌 → (𝑋 = ∅ ∨ ∃𝑧 𝑧:𝑌–onto→𝑋)) | ||
Theorem | brwdomn0 9594* | Weak dominance over nonempty sets. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
⊢ (𝑋 ≠ ∅ → (𝑋 ≼* 𝑌 ↔ ∃𝑧 𝑧:𝑌–onto→𝑋)) | ||
Theorem | 0wdom 9595 | Any set weakly dominates the empty set. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ (𝑋 ∈ 𝑉 → ∅ ≼* 𝑋) | ||
Theorem | fowdom 9596 | An onto function implies weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝑌–onto→𝑋) → 𝑋 ≼* 𝑌) | ||
Theorem | wdomref 9597 | Reflexivity of weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ (𝑋 ∈ 𝑉 → 𝑋 ≼* 𝑋) | ||
Theorem | brwdom2 9598* | Alternate characterization of the weak dominance predicate which does not require special treatment of the empty set. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ (𝑌 ∈ 𝑉 → (𝑋 ≼* 𝑌 ↔ ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋)) | ||
Theorem | domwdom 9599 | Weak dominance is implied by dominance in the usual sense. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ (𝑋 ≼ 𝑌 → 𝑋 ≼* 𝑌) | ||
Theorem | wdomtr 9600 | Transitivity of weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
⊢ ((𝑋 ≼* 𝑌 ∧ 𝑌 ≼* 𝑍) → 𝑋 ≼* 𝑍) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |