Metamath Proof Explorer


Theorem cofcutr1d

Description: If X is the cut of A and B , then A is cofinal with ( _LeftX ) . 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