Description: To get through most of the textbook defintions in surreal numbers we will need recursion on two variables. This set of theorems sets up the preconditions for double recursion. This theorem establishes the partial ordering. (Contributed by Scott Fenton, 19-Aug-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | noxpord.1 | ⊢ 𝑅 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } | |
| noxpord.2 | ⊢ 𝑆 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( No × No ) ∧ 𝑦 ∈ ( No × No ) ∧ ( ( ( 1st ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑦 ) ∨ ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ) ∧ ( ( 2nd ‘ 𝑥 ) 𝑅 ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) } | ||
| Assertion | noxpordpo | ⊢ 𝑆 Po ( No × No ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | noxpord.1 | ⊢ 𝑅 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) } | |
| 2 | noxpord.2 | ⊢ 𝑆 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( No × No ) ∧ 𝑦 ∈ ( No × No ) ∧ ( ( ( 1st ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑦 ) ∨ ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ) ∧ ( ( 2nd ‘ 𝑥 ) 𝑅 ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) } | |
| 3 | 1 | lrrecpo | ⊢ 𝑅 Po No |
| 4 | 3 | a1i | ⊢ ( ⊤ → 𝑅 Po No ) |
| 5 | 2 4 4 | poxp2 | ⊢ ( ⊤ → 𝑆 Po ( No × No ) ) |
| 6 | 5 | mptru | ⊢ 𝑆 Po ( No × No ) |