Database
SURREAL NUMBERS
Conway cut representation
Cofinality and coinitiality
cofcutr2d
Metamath Proof Explorer
Description: If X is the cut of A and B , then B is coinitial with
( _Right X ) . Second half of theorem 2.9 of Gonshor p. 12.
(Contributed by Scott Fenton , 25-Sep-2024)
Ref
Expression
Hypotheses
cofcutrd.1
⊢ φ → A ≪ s B
cofcutrd.2
⊢ φ → X = A | s B
Assertion
cofcutr2d
⊢ φ → ∀ z ∈ R ⁡ X ∃ w ∈ B w ≤ s z
Proof
Step
Hyp
Ref
Expression
1
cofcutrd.1
⊢ φ → A ≪ s B
2
cofcutrd.2
⊢ φ → X = A | s B
3
cofcutr
⊢ A ≪ s B ∧ X = A | s B → ∀ x ∈ L ⁡ X ∃ y ∈ A x ≤ s y ∧ ∀ z ∈ R ⁡ X ∃ w ∈ B w ≤ s z
4
1 2 3
syl2anc
⊢ φ → ∀ x ∈ L ⁡ X ∃ y ∈ A x ≤ s y ∧ ∀ z ∈ R ⁡ X ∃ w ∈ B w ≤ s z
5
4
simprd
⊢ φ → ∀ z ∈ R ⁡ X ∃ w ∈ B w ≤ s z