Database
SURREAL NUMBERS
Conway cut representation
Cofinality and coinitiality
cofcutr1d
Metamath Proof Explorer
Description: If X is the cut of A and B , then A is cofinal with
( _Left X ) . First half of theorem 2.9 of Gonshor p. 12.
(Contributed by Scott Fenton , 23-Jan-2025)
Ref
Expression
Hypotheses
cofcutrd.1
⊢ φ → A ≪ s B
cofcutrd.2
⊢ φ → X = A | s B
Assertion
cofcutr1d
⊢ φ → ∀ x ∈ L ⁡ X ∃ y ∈ A x ≤ s y
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
simpld
⊢ φ → ∀ x ∈ L ⁡ X ∃ y ∈ A x ≤ s y