Metamath Proof Explorer


Theorem cofcutr2d

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