Metamath Proof Explorer


Theorem cofcutrtime1d

Description: If X is a timely cut of A and B , then ( _LeftX ) is cofinal with A . (Contributed by Scott Fenton, 23-Jan-2025)

Ref Expression
Hypotheses cofcutrtimed.1 φ A B Old bday X
cofcutrtimed.2 φ A s B
cofcutrtimed.3 φ X = A | s B
Assertion cofcutrtime1d φ x A y L X x s y

Proof

Step Hyp Ref Expression
1 cofcutrtimed.1 φ A B Old bday X
2 cofcutrtimed.2 φ A s B
3 cofcutrtimed.3 φ X = A | s B
4 cofcutrtime A B Old bday X A s B X = A | s B x A y L X x s y z B w R X w s z
5 1 2 3 4 syl3anc φ x A y L X x s y z B w R X w s z
6 5 simpld φ x A y L X x s y