HomeTheorem List (p. 339 of 466)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 339 of 466) | < 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: | Metamath Proof Explorer
(1-29289) |
Hilbert Space Explorer
(29290-30812) |
Users' Mathboxes
(30813-46532) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | xpord2pred 33801* | Calculate the predecessor class in frxp2 33800. (Contributed by Scott Fenton, 22-Aug-2024.) |
| ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥)𝑆(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))} ⇒ ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) ∖ {⟨𝑋, 𝑌⟩})) | ||
| Theorem | sexp2 33802* | Condition for the relationship in frxp2 33800 to be set-like. (Contributed by Scott Fenton, 19-Aug-2024.) |
| ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥)𝑆(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))} & ⊢ (𝜑 → 𝑅 Se 𝐴) & ⊢ (𝜑 → 𝑆 Se 𝐵) ⇒ ⊢ (𝜑 → 𝑇 Se (𝐴 × 𝐵)) | ||
| Theorem | xpord2ind 33803* | Induction over the cross product ordering. Note that the substitutions cover all possible cases of membership in the predecessor class. (Contributed by Scott Fenton, 22-Aug-2024.) |
| ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥)𝑆(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))} & ⊢ 𝑅 Fr 𝐴 & ⊢ 𝑅 Po 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝑆 Fr 𝐵 & ⊢ 𝑆 Po 𝐵 & ⊢ 𝑆 Se 𝐵 & ⊢ (𝑎 = 𝑐 → (𝜑 ↔ 𝜓)) & ⊢ (𝑏 = 𝑑 → (𝜓 ↔ 𝜒)) & ⊢ (𝑎 = 𝑐 → (𝜃 ↔ 𝜒)) & ⊢ (𝑎 = 𝑋 → (𝜑 ↔ 𝜏)) & ⊢ (𝑏 = 𝑌 → (𝜏 ↔ 𝜂)) & ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ((∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒 ∧ ∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓 ∧ ∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)𝜃) → 𝜑)) ⇒ ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → 𝜂) | ||
| Theorem | xpord3lem 33804* | Lemma for triple ordering. Calculate the value of the relationship. (Contributed by Scott Fenton, 21-Aug-2024.) |
| ⊢ 𝑈 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st ‘(1st ‘𝑥))𝑅(1st ‘(1st ‘𝑦)) ∨ (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑦))) ∧ ((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st ‘𝑦)) ∨ (2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘𝑦))) ∧ ((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦))} ⇒ ⊢ (⟨⟨𝑎, 𝑏⟩, 𝑐⟩𝑈⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)))) | ||
| Theorem | poxp3 33805* | Triple cross product partial ordering. (Contributed by Scott Fenton, 21-Aug-2024.) |
| ⊢ 𝑈 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st ‘(1st ‘𝑥))𝑅(1st ‘(1st ‘𝑦)) ∨ (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑦))) ∧ ((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st ‘𝑦)) ∨ (2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘𝑦))) ∧ ((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦))} & ⊢ (𝜑 → 𝑅 Po 𝐴) & ⊢ (𝜑 → 𝑆 Po 𝐵) & ⊢ (𝜑 → 𝑇 Po 𝐶) ⇒ ⊢ (𝜑 → 𝑈 Po ((𝐴 × 𝐵) × 𝐶)) | ||
| Theorem | frxp3 33806* | Give foundedness over a triple cross product. (Contributed by Scott Fenton, 21-Aug-2024.) |
| ⊢ 𝑈 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st ‘(1st ‘𝑥))𝑅(1st ‘(1st ‘𝑦)) ∨ (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑦))) ∧ ((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st ‘𝑦)) ∨ (2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘𝑦))) ∧ ((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦))} & ⊢ (𝜑 → 𝑅 Fr 𝐴) & ⊢ (𝜑 → 𝑆 Fr 𝐵) & ⊢ (𝜑 → 𝑇 Fr 𝐶) ⇒ ⊢ (𝜑 → 𝑈 Fr ((𝐴 × 𝐵) × 𝐶)) | ||
| Theorem | xpord3pred 33807* | Calculate the predecsessor class for the triple order. (Contributed by Scott Fenton, 21-Aug-2024.) |
| ⊢ 𝑈 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st ‘(1st ‘𝑥))𝑅(1st ‘(1st ‘𝑦)) ∨ (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑦))) ∧ ((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st ‘𝑦)) ∨ (2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘𝑦))) ∧ ((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦))} ⇒ ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑌⟩, 𝑍⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {⟨⟨𝑋, 𝑌⟩, 𝑍⟩})) | ||
| Theorem | sexp3 33808* | Show that the triple order is set-like. (Contributed by Scott Fenton, 21-Aug-2024.) |
| ⊢ 𝑈 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st ‘(1st ‘𝑥))𝑅(1st ‘(1st ‘𝑦)) ∨ (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑦))) ∧ ((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st ‘𝑦)) ∨ (2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘𝑦))) ∧ ((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦))} & ⊢ (𝜑 → 𝑅 Se 𝐴) & ⊢ (𝜑 → 𝑆 Se 𝐵) & ⊢ (𝜑 → 𝑇 Se 𝐶) ⇒ ⊢ (𝜑 → 𝑈 Se ((𝐴 × 𝐵) × 𝐶)) | ||
| Theorem | xpord3ind 33809* | Induction over the triple cross product ordering. Note that the substitutions cover all possible cases of membership in the predecessor class. (Contributed by Scott Fenton, 4-Sep-2024.) |
| ⊢ 𝑈 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st ‘(1st ‘𝑥))𝑅(1st ‘(1st ‘𝑦)) ∨ (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑦))) ∧ ((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st ‘𝑦)) ∨ (2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘𝑦))) ∧ ((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦))} & ⊢ 𝑅 Fr 𝐴 & ⊢ 𝑅 Po 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝑆 Fr 𝐵 & ⊢ 𝑆 Po 𝐵 & ⊢ 𝑆 Se 𝐵 & ⊢ 𝑇 Fr 𝐶 & ⊢ 𝑇 Po 𝐶 & ⊢ 𝑇 Se 𝐶 & ⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜓)) & ⊢ (𝑏 = 𝑒 → (𝜓 ↔ 𝜒)) & ⊢ (𝑐 = 𝑓 → (𝜒 ↔ 𝜃)) & ⊢ (𝑎 = 𝑑 → (𝜏 ↔ 𝜃)) & ⊢ (𝑏 = 𝑒 → (𝜂 ↔ 𝜏)) & ⊢ (𝑏 = 𝑒 → (𝜁 ↔ 𝜃)) & ⊢ (𝑐 = 𝑓 → (𝜎 ↔ 𝜏)) & ⊢ (𝑎 = 𝑋 → (𝜑 ↔ 𝜌)) & ⊢ (𝑏 = 𝑌 → (𝜌 ↔ 𝜇)) & ⊢ (𝑐 = 𝑍 → (𝜇 ↔ 𝜆)) & ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (((∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁) ∧ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎) ∧ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂) → 𝜑)) ⇒ ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶) → 𝜆) | ||
| Theorem | orderseqlem 33810* | Lemma for poseq 33811 and soseq 33812. The function value of a sequene is either in 𝐴 or null. (Contributed by Scott Fenton, 8-Jun-2011.) |
| ⊢ 𝐹 = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶𝐴} ⇒ ⊢ (𝐺 ∈ 𝐹 → (𝐺‘𝑋) ∈ (𝐴 ∪ {∅})) | ||
| Theorem | poseq 33811* | A partial ordering of sequences of ordinals. (Contributed by Scott Fenton, 8-Jun-2011.) |
| ⊢ 𝑅 Po (𝐴 ∪ {∅}) & ⊢ 𝐹 = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶𝐴} & ⊢ 𝑆 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)))} ⇒ ⊢ 𝑆 Po 𝐹 | ||
| Theorem | soseq 33812* | A linear ordering of sequences of ordinals. (Contributed by Scott Fenton, 8-Jun-2011.) |
| ⊢ 𝑅 Or (𝐴 ∪ {∅}) & ⊢ 𝐹 = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶𝐴} & ⊢ 𝑆 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)))} & ⊢ ¬ ∅ ∈ 𝐴 ⇒ ⊢ 𝑆 Or 𝐹 | ||
| Syntax | cwsuc 33813 | Declare the syntax for well-founded successor. |
| class wsuc(𝑅, 𝐴, 𝑋) | ||
| Syntax | cwlim 33814 | Declare the syntax for well-founded limit class. |
| class WLim(𝑅, 𝐴) | ||
| Definition | df-wsuc 33815 | Define the concept of a successor in a well-founded set. (Contributed by Scott Fenton, 13-Jun-2018.) (Revised by AV, 10-Oct-2021.) |
| ⊢ wsuc(𝑅, 𝐴, 𝑋) = inf(Pred(◡𝑅, 𝐴, 𝑋), 𝐴, 𝑅) | ||
| Definition | df-wlim 33816* | Define the class of limit points of a well-founded set. (Contributed by Scott Fenton, 15-Jun-2018.) (Revised by AV, 10-Oct-2021.) |
| ⊢ WLim(𝑅, 𝐴) = {𝑥 ∈ 𝐴 ∣ (𝑥 ≠ inf(𝐴, 𝐴, 𝑅) ∧ 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅))} | ||
| Theorem | wsuceq123 33817 | Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
| ⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝑋 = 𝑌) → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑆, 𝐵, 𝑌)) | ||
| Theorem | wsuceq1 33818 | Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) |
| ⊢ (𝑅 = 𝑆 → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑆, 𝐴, 𝑋)) | ||
| Theorem | wsuceq2 33819 | Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) |
| ⊢ (𝐴 = 𝐵 → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑅, 𝐵, 𝑋)) | ||
| Theorem | wsuceq3 33820 | Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) |
| ⊢ (𝑋 = 𝑌 → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑅, 𝐴, 𝑌)) | ||
| Theorem | nfwsuc 33821 | Bound-variable hypothesis builder for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
| ⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝑋 ⇒ ⊢ Ⅎ𝑥wsuc(𝑅, 𝐴, 𝑋) | ||
| Theorem | wlimeq12 33822 | Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
| ⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵) → WLim(𝑅, 𝐴) = WLim(𝑆, 𝐵)) | ||
| Theorem | wlimeq1 33823 | Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) |
| ⊢ (𝑅 = 𝑆 → WLim(𝑅, 𝐴) = WLim(𝑆, 𝐴)) | ||
| Theorem | wlimeq2 33824 | Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) |
| ⊢ (𝐴 = 𝐵 → WLim(𝑅, 𝐴) = WLim(𝑅, 𝐵)) | ||
| Theorem | nfwlim 33825 | Bound-variable hypothesis builder for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
| ⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥WLim(𝑅, 𝐴) | ||
| Theorem | elwlim 33826 | Membership in the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Revised by AV, 10-Oct-2021.) |
| ⊢ (𝑋 ∈ WLim(𝑅, 𝐴) ↔ (𝑋 ∈ 𝐴 ∧ 𝑋 ≠ inf(𝐴, 𝐴, 𝑅) ∧ 𝑋 = sup(Pred(𝑅, 𝐴, 𝑋), 𝐴, 𝑅))) | ||
| Theorem | wzel 33827 | The zero of a well-founded set is a member of that set. (Contributed by Scott Fenton, 13-Jun-2018.) (Revised by AV, 10-Oct-2021.) |
| ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐴 ≠ ∅) → inf(𝐴, 𝐴, 𝑅) ∈ 𝐴) | ||
| Theorem | wsuclem 33828* | Lemma for the supremum properties of well-founded successor. (Contributed by Scott Fenton, 15-Jun-2018.) (Revised by AV, 10-Oct-2021.) |
| ⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ∃𝑤 ∈ 𝐴 𝑋𝑅𝑤) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ Pred (◡𝑅, 𝐴, 𝑋) ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ Pred (◡𝑅, 𝐴, 𝑋)𝑧𝑅𝑦))) | ||
| Theorem | wsucex 33829 | Existence theorem for well-founded successor. (Contributed by Scott Fenton, 16-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
| ⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → wsuc(𝑅, 𝐴, 𝑋) ∈ V) | ||
| Theorem | wsuccl 33830* | If 𝑋 is a set with an 𝑅 successor in 𝐴, then its well-founded successor is a member of 𝐴. (Contributed by Scott Fenton, 15-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
| ⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ∃𝑦 ∈ 𝐴 𝑋𝑅𝑦) ⇒ ⊢ (𝜑 → wsuc(𝑅, 𝐴, 𝑋) ∈ 𝐴) | ||
| Theorem | wsuclb 33831 | A well-founded successor is a lower bound on points after 𝑋. (Contributed by Scott Fenton, 16-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
| ⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝑋𝑅𝑌) ⇒ ⊢ (𝜑 → ¬ 𝑌𝑅wsuc(𝑅, 𝐴, 𝑋)) | ||
| Theorem | wlimss 33832 | The class of limit points is a subclass of the base class. (Contributed by Scott Fenton, 16-Jun-2018.) |
| ⊢ WLim(𝑅, 𝐴) ⊆ 𝐴 | ||
| Syntax | cnadd 33833 | Declare the syntax for natural ordinal addition. See df-nadd 33834. |
| class +no | ||
| Definition | df-nadd 33834* | Define natural ordinal addition. This is a commutative form of addition over the ordinals. (Contributed by Scott Fenton, 26-Aug-2024.) |
| ⊢ +no = frecs({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥) E (2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}, (On × On), (𝑧 ∈ V, 𝑎 ∈ V ↦ ∩ {𝑤 ∈ On ∣ ((𝑎 “ ({(1st ‘𝑧)} × (2nd ‘𝑧))) ⊆ 𝑤 ∧ (𝑎 “ ((1st ‘𝑧) × {(2nd ‘𝑧)})) ⊆ 𝑤)})) | ||
| Theorem | on2recsfn 33835* | Show that double recursion over ordinals yields a function over pairs of ordinals. (Contributed by Scott Fenton, 3-Sep-2024.) |
| ⊢ 𝐹 = frecs({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥) E (2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}, (On × On), 𝐺) ⇒ ⊢ 𝐹 Fn (On × On) | ||
| Theorem | on2recsov 33836* | Calculate the value of the double ordinal recursion operator. (Contributed by Scott Fenton, 3-Sep-2024.) |
| ⊢ 𝐹 = frecs({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥) E (2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}, (On × On), 𝐺) ⇒ ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴𝐹𝐵) = (⟨𝐴, 𝐵⟩𝐺(𝐹 ↾ ((suc 𝐴 × suc 𝐵) ∖ {⟨𝐴, 𝐵⟩})))) | ||
| Theorem | on2ind 33837* | Double induction over ordinal numbers. (Contributed by Scott Fenton, 26-Aug-2024.) |
| ⊢ (𝑎 = 𝑐 → (𝜑 ↔ 𝜓)) & ⊢ (𝑏 = 𝑑 → (𝜓 ↔ 𝜒)) & ⊢ (𝑎 = 𝑐 → (𝜃 ↔ 𝜒)) & ⊢ (𝑎 = 𝑋 → (𝜑 ↔ 𝜏)) & ⊢ (𝑏 = 𝑌 → (𝜏 ↔ 𝜂)) & ⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) → ((∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑏 𝜒 ∧ ∀𝑐 ∈ 𝑎 𝜓 ∧ ∀𝑑 ∈ 𝑏 𝜃) → 𝜑)) ⇒ ⊢ ((𝑋 ∈ On ∧ 𝑌 ∈ On) → 𝜂) | ||
| Theorem | on3ind 33838* | Triple induction over ordinals. (Contributed by Scott Fenton, 4-Sep-2024.) |
| ⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜓)) & ⊢ (𝑏 = 𝑒 → (𝜓 ↔ 𝜒)) & ⊢ (𝑐 = 𝑓 → (𝜒 ↔ 𝜃)) & ⊢ (𝑎 = 𝑑 → (𝜏 ↔ 𝜃)) & ⊢ (𝑏 = 𝑒 → (𝜂 ↔ 𝜏)) & ⊢ (𝑏 = 𝑒 → (𝜁 ↔ 𝜃)) & ⊢ (𝑐 = 𝑓 → (𝜎 ↔ 𝜏)) & ⊢ (𝑎 = 𝑋 → (𝜑 ↔ 𝜌)) & ⊢ (𝑏 = 𝑌 → (𝜌 ↔ 𝜇)) & ⊢ (𝑐 = 𝑍 → (𝜇 ↔ 𝜆)) & ⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) → (((∀𝑑 ∈ 𝑎 ∀𝑒 ∈ 𝑏 ∀𝑓 ∈ 𝑐 𝜃 ∧ ∀𝑑 ∈ 𝑎 ∀𝑒 ∈ 𝑏 𝜒 ∧ ∀𝑑 ∈ 𝑎 ∀𝑓 ∈ 𝑐 𝜁) ∧ (∀𝑑 ∈ 𝑎 𝜓 ∧ ∀𝑒 ∈ 𝑏 ∀𝑓 ∈ 𝑐 𝜏 ∧ ∀𝑒 ∈ 𝑏 𝜎) ∧ ∀𝑓 ∈ 𝑐 𝜂) → 𝜑)) ⇒ ⊢ ((𝑋 ∈ On ∧ 𝑌 ∈ On ∧ 𝑍 ∈ On) → 𝜆) | ||
| Theorem | naddfn 33839 | Natural addition is a function over pairs of ordinals. (Contributed by Scott Fenton, 26-Aug-2024.) |
| ⊢ +no Fn (On × On) | ||
| Theorem | naddcllem 33840* | Lemma for ordinal addition closure. (Contributed by Scott Fenton, 26-Aug-2024.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +no 𝐵) ∈ On ∧ (𝐴 +no 𝐵) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)})) | ||
| Theorem | naddcl 33841 | Closure law for natural addition. (Contributed by Scott Fenton, 26-Aug-2024.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +no 𝐵) ∈ On) | ||
| Theorem | naddov 33842* | The value of natural addition. (Contributed by Scott Fenton, 26-Aug-2024.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +no 𝐵) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)}) | ||
| Theorem | naddov2 33843* | Alternate expression for natural addition. (Contributed by Scott Fenton, 26-Aug-2024.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +no 𝐵) = ∩ {𝑥 ∈ On ∣ (∀𝑦 ∈ 𝐵 (𝐴 +no 𝑦) ∈ 𝑥 ∧ ∀𝑧 ∈ 𝐴 (𝑧 +no 𝐵) ∈ 𝑥)}) | ||
| Theorem | naddcom 33844 | Natural addition commutes. (Contributed by Scott Fenton, 26-Aug-2024.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +no 𝐵) = (𝐵 +no 𝐴)) | ||
| Theorem | naddid1 33845 | Ordinal zero is the additive identity for natural addition. (Contributed by Scott Fenton, 26-Aug-2024.) |
| ⊢ (𝐴 ∈ On → (𝐴 +no ∅) = 𝐴) | ||
| Theorem | naddssim 33846 | Ordinal less-than-or-equal is preserved by natural addition. (Contributed by Scott Fenton, 7-Sep-2024.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ⊆ 𝐵 → (𝐴 +no 𝐶) ⊆ (𝐵 +no 𝐶))) | ||
| Theorem | naddelim 33847 | Ordinal less-than is preserved by natural addition. (Contributed by Scott Fenton, 9-Sep-2024.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → (𝐴 +no 𝐶) ∈ (𝐵 +no 𝐶))) | ||
| Theorem | naddel1 33848 | Ordinal less-than is not affected by natural addition. (Contributed by Scott Fenton, 9-Sep-2024.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 ↔ (𝐴 +no 𝐶) ∈ (𝐵 +no 𝐶))) | ||
| Theorem | naddel2 33849 | Ordinal less-than is not affected by natural addition. (Contributed by Scott Fenton, 9-Sep-2024.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 ↔ (𝐶 +no 𝐴) ∈ (𝐶 +no 𝐵))) | ||
| Theorem | naddss1 33850 | Ordinal less-than-or-equal is not affected by natural addition. (Contributed by Scott Fenton, 9-Sep-2024.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ⊆ 𝐵 ↔ (𝐴 +no 𝐶) ⊆ (𝐵 +no 𝐶))) | ||
| Theorem | naddss2 33851 | Ordinal less-than-or-equal is not affected by natural addition. (Contributed by Scott Fenton, 9-Sep-2024.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ⊆ 𝐵 ↔ (𝐶 +no 𝐴) ⊆ (𝐶 +no 𝐵))) | ||
| Syntax | csur 33852 | Declare the class of all surreal numbers (see df-no 33855). |
| class No | ||
| Syntax | cslt 33853 | Declare the less than relationship over surreal numbers (see df-slt 33856). |
| class <s | ||
| Syntax | cbday 33854 | Declare the birthday function for surreal numbers (see df-bday 33857). |
| class bday | ||
| Definition | df-no 33855* |
Define the class of surreal numbers. The surreal numbers are a proper
class of numbers developed by John H. Conway and introduced by Donald
Knuth in 1975. They form a proper class into which all ordered fields
can be embedded. The approach we take to defining them was first
introduced by Hary Gonshor, and is based on the conception of a
"sign
expansion" of a surreal number. We define the surreals as
ordinal-indexed sequences of 1o and
2o, analagous to Gonshor's
( − ) and ( + ).
After introducing this definition, we will abstract away from it using axioms that Norman Alling developed in "Foundations of Analysis over Surreal Number Fields." This is done in an effort to be agnostic towards the exact implementation of surreals. (Contributed by Scott Fenton, 9-Jun-2011.) |
| ⊢ No = {𝑓 ∣ ∃𝑎 ∈ On 𝑓:𝑎⟶{1o, 2o}} | ||
| Definition | df-slt 33856* | Next, we introduce surreal less-than, a comparison relationship over the surreals by lexicographically ordering them. (Contributed by Scott Fenton, 9-Jun-2011.) |
| ⊢ <s = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ No ∧ 𝑔 ∈ No ) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔‘𝑥)))} | ||
| Definition | df-bday 33857 | Finally, we introduce the birthday function. This function maps each surreal to an ordinal. In our implementation, this is the domain of the sign function. The important properties of this function are established later. (Contributed by Scott Fenton, 11-Jun-2011.) |
| ⊢ bday = (𝑥 ∈ No ↦ dom 𝑥) | ||
| Theorem | elno 33858* | Membership in the surreals. (Shortened proof on 2012-Apr-14, SF). (Contributed by Scott Fenton, 11-Jun-2011.) |
| ⊢ (𝐴 ∈ No ↔ ∃𝑥 ∈ On 𝐴:𝑥⟶{1o, 2o}) | ||
| Theorem | sltval 33859* | The value of the surreal less than relationship. (Contributed by Scott Fenton, 14-Jun-2011.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥)))) | ||
| Theorem | bdayval 33860 | The value of the birthday function within the surreals. (Contributed by Scott Fenton, 14-Jun-2011.) |
| ⊢ (𝐴 ∈ No → ( bday ‘𝐴) = dom 𝐴) | ||
| Theorem | nofun 33861 | A surreal is a function. (Contributed by Scott Fenton, 16-Jun-2011.) |
| ⊢ (𝐴 ∈ No → Fun 𝐴) | ||
| Theorem | nodmon 33862 | The domain of a surreal is an ordinal. (Contributed by Scott Fenton, 16-Jun-2011.) |
| ⊢ (𝐴 ∈ No → dom 𝐴 ∈ On) | ||
| Theorem | norn 33863 | The range of a surreal is a subset of the surreal signs. (Contributed by Scott Fenton, 16-Jun-2011.) |
| ⊢ (𝐴 ∈ No → ran 𝐴 ⊆ {1o, 2o}) | ||
| Theorem | nofnbday 33864 | A surreal is a function over its birthday. (Contributed by Scott Fenton, 16-Jun-2011.) |
| ⊢ (𝐴 ∈ No → 𝐴 Fn ( bday ‘𝐴)) | ||
| Theorem | nodmord 33865 | The domain of a surreal has the ordinal property. (Contributed by Scott Fenton, 16-Jun-2011.) |
| ⊢ (𝐴 ∈ No → Ord dom 𝐴) | ||
| Theorem | elno2 33866 | An alternative condition for membership in No . (Contributed by Scott Fenton, 21-Mar-2012.) |
| ⊢ (𝐴 ∈ No ↔ (Fun 𝐴 ∧ dom 𝐴 ∈ On ∧ ran 𝐴 ⊆ {1o, 2o})) | ||
| Theorem | elno3 33867 | Another condition for membership in No . (Contributed by Scott Fenton, 14-Apr-2012.) |
| ⊢ (𝐴 ∈ No ↔ (𝐴:dom 𝐴⟶{1o, 2o} ∧ dom 𝐴 ∈ On)) | ||
| Theorem | sltval2 33868* | Alternate expression for surreal less than. Two surreals obey surreal less than iff they obey the sign ordering at the first place they differ. (Contributed by Scott Fenton, 17-Jun-2011.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 ↔ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))) | ||
| Theorem | nofv 33869 | The function value of a surreal is either a sign or the empty set. (Contributed by Scott Fenton, 22-Jun-2011.) |
| ⊢ (𝐴 ∈ No → ((𝐴‘𝑋) = ∅ ∨ (𝐴‘𝑋) = 1o ∨ (𝐴‘𝑋) = 2o)) | ||
| Theorem | nosgnn0 33870 | ∅ is not a surreal sign. (Contributed by Scott Fenton, 16-Jun-2011.) |
| ⊢ ¬ ∅ ∈ {1o, 2o} | ||
| Theorem | nosgnn0i 33871 | If 𝑋 is a surreal sign, then it is not null. (Contributed by Scott Fenton, 3-Aug-2011.) |
| ⊢ 𝑋 ∈ {1o, 2o} ⇒ ⊢ ∅ ≠ 𝑋 | ||
| Theorem | noreson 33872 | The restriction of a surreal to an ordinal is still a surreal. (Contributed by Scott Fenton, 4-Sep-2011.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ On) → (𝐴 ↾ 𝐵) ∈ No ) | ||
| Theorem | sltintdifex 33873* | If 𝐴 <s 𝐵, then the intersection of all the ordinals that have differing signs in 𝐴 and 𝐵 exists. (Contributed by Scott Fenton, 22-Feb-2012.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V)) | ||
| Theorem | sltres 33874 | If the restrictions of two surreals to a given ordinal obey surreal less than, then so do the two surreals themselves. (Contributed by Scott Fenton, 4-Sep-2011.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → 𝐴 <s 𝐵)) | ||
| Theorem | noxp1o 33875 | The Cartesian product of an ordinal and {1o} is a surreal. (Contributed by Scott Fenton, 12-Jun-2011.) |
| ⊢ (𝐴 ∈ On → (𝐴 × {1o}) ∈ No ) | ||
| Theorem | noseponlem 33876* | Lemma for nosepon 33877. Consider a case of proper subset domain. (Contributed by Scott Fenton, 21-Sep-2020.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ dom 𝐴 ∈ dom 𝐵) → ¬ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥)) | ||
| Theorem | nosepon 33877* | Given two unequal surreals, the minimal ordinal at which they differ is an ordinal. (Contributed by Scott Fenton, 21-Sep-2020.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵) → ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ On) | ||
| Theorem | noextend 33878 | Extending a surreal by one sign value results in a new surreal. (Contributed by Scott Fenton, 22-Nov-2021.) |
| ⊢ 𝑋 ∈ {1o, 2o} ⇒ ⊢ (𝐴 ∈ No → (𝐴 ∪ {⟨dom 𝐴, 𝑋⟩}) ∈ No ) | ||
| Theorem | noextendseq 33879 | Extend a surreal by a sequence of ordinals. (Contributed by Scott Fenton, 30-Nov-2021.) |
| ⊢ 𝑋 ∈ {1o, 2o} ⇒ ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ On) → (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ∈ No ) | ||
| Theorem | noextenddif 33880* | Calculate the place where a surreal and its extension differ. (Contributed by Scott Fenton, 22-Nov-2021.) |
| ⊢ 𝑋 ∈ {1o, 2o} ⇒ ⊢ (𝐴 ∈ No → ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ ((𝐴 ∪ {⟨dom 𝐴, 𝑋⟩})‘𝑥)} = dom 𝐴) | ||
| Theorem | noextendlt 33881 | Extending a surreal with a negative sign results in a smaller surreal. (Contributed by Scott Fenton, 22-Nov-2021.) |
| ⊢ (𝐴 ∈ No → (𝐴 ∪ {⟨dom 𝐴, 1o⟩}) <s 𝐴) | ||
| Theorem | noextendgt 33882 | Extending a surreal with a positive sign results in a bigger surreal. (Contributed by Scott Fenton, 22-Nov-2021.) |
| ⊢ (𝐴 ∈ No → 𝐴 <s (𝐴 ∪ {⟨dom 𝐴, 2o⟩})) | ||
| Theorem | nolesgn2o 33883 | Given 𝐴 less than or equal to 𝐵, equal to 𝐵 up to 𝑋, and 𝐴(𝑋) = 2o, then 𝐵(𝑋) = 2o. (Contributed by Scott Fenton, 6-Dec-2021.) |
| ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → (𝐵‘𝑋) = 2o) | ||
| Theorem | nolesgn2ores 33884 | Given 𝐴 less than or equal to 𝐵, equal to 𝐵 up to 𝑋, and 𝐴(𝑋) = 2o, then (𝐴 ↾ suc 𝑋) = (𝐵 ↾ suc 𝑋). (Contributed by Scott Fenton, 6-Dec-2021.) |
| ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → (𝐴 ↾ suc 𝑋) = (𝐵 ↾ suc 𝑋)) | ||
| Theorem | nogesgn1o 33885 | Given 𝐴 greater than or equal to 𝐵, equal to 𝐵 up to 𝑋, and 𝐴(𝑋) = 1o, then 𝐵(𝑋) = 1o. (Contributed by Scott Fenton, 9-Aug-2024.) |
| ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 1o) ∧ ¬ 𝐴 <s 𝐵) → (𝐵‘𝑋) = 1o) | ||
| Theorem | nogesgn1ores 33886 | Given 𝐴 greater than or equal to 𝐵, equal to 𝐵 up to 𝑋, and 𝐴(𝑋) = 1o, then (𝐴 ↾ suc 𝑋) = (𝐵 ↾ suc 𝑋). (Contributed by Scott Fenton, 6-Dec-2021.) |
| ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 1o) ∧ ¬ 𝐴 <s 𝐵) → (𝐴 ↾ suc 𝑋) = (𝐵 ↾ suc 𝑋)) | ||
| Theorem | sltsolem1 33887 | Lemma for sltso 33888. The sign expansion relationship totally orders the surreal signs. (Contributed by Scott Fenton, 8-Jun-2011.) |
| ⊢ {⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} Or ({1o, 2o} ∪ {∅}) | ||
| Theorem | sltso 33888 | Surreal less than totally orders the surreals. Axiom O of [Alling] p. 184. (Contributed by Scott Fenton, 9-Jun-2011.) |
| ⊢ <s Or No | ||
| Theorem | bdayfo 33889 | The birthday function maps the surreals onto the ordinals. Axiom B of [Alling] p. 184. (Shortened proof on 2012-Apr-14, SF). (Contributed by Scott Fenton, 11-Jun-2011.) |
| ⊢ bday : No –onto→On | ||
| Theorem | fvnobday 33890 | The value of a surreal at its birthday is ∅. (Contributed by Scott Fenton, 14-Jun-2011.) (Proof shortened by SF, 14-Apr-2012.) |
| ⊢ (𝐴 ∈ No → (𝐴‘( bday ‘𝐴)) = ∅) | ||
| Theorem | nosepnelem 33891* | Lemma for nosepne 33892. (Contributed by Scott Fenton, 24-Nov-2021.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 <s 𝐵) → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)})) | ||
| Theorem | nosepne 33892* | The value of two non-equal surreals at the first place they differ is different. (Contributed by Scott Fenton, 24-Nov-2021.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵) → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)})) | ||
| Theorem | nosep1o 33893* | If the value of a surreal at a separator is 1o then the surreal is lesser. (Contributed by Scott Fenton, 7-Dec-2021.) |
| ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵) ∧ (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1o) → 𝐴 <s 𝐵) | ||
| Theorem | nosep2o 33894* | If the value of a surreal at a separator is 2o then the surreal is greater. (Contributed by Scott Fenton, 7-Dec-2021.) |
| ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵) ∧ (𝐴‘∩ {𝑥 ∈ On ∣ (𝐵‘𝑥) ≠ (𝐴‘𝑥)}) = 2o) → 𝐵 <s 𝐴) | ||
| Theorem | nosepdmlem 33895* | Lemma for nosepdm 33896. (Contributed by Scott Fenton, 24-Nov-2021.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 <s 𝐵) → ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ (dom 𝐴 ∪ dom 𝐵)) | ||
| Theorem | nosepdm 33896* | The first place two surreals differ is an element of the larger of their domains. (Contributed by Scott Fenton, 24-Nov-2021.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵) → ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ (dom 𝐴 ∪ dom 𝐵)) | ||
| Theorem | nosepeq 33897* | The values of two surreals at a point less than their separators are equal. (Contributed by Scott Fenton, 6-Dec-2021.) |
| ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵) ∧ 𝑋 ∈ ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) → (𝐴‘𝑋) = (𝐵‘𝑋)) | ||
| Theorem | nosepssdm 33898* | Given two non-equal surreals, their separator is less than or equal to the domain of one of them. Part of Lemma 2.1.1 of [Lipparini] p. 3. (Contributed by Scott Fenton, 6-Dec-2021.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵) → ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ⊆ dom 𝐴) | ||
| Theorem | nodenselem4 33899* | Lemma for nodense 33904. Show that a particular abstraction is an ordinal. (Contributed by Scott Fenton, 16-Jun-2011.) |
| ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝐴 <s 𝐵) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On) | ||
| Theorem | nodenselem5 33900* | Lemma for nodense 33904. If the birthdays of two distinct surreals are equal, then the ordinal from nodenselem4 33899 is an element of that birthday. (Contributed by Scott Fenton, 16-Jun-2011.) |
| ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (( bday ‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ ( bday ‘𝐴)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |