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	|- ( ph -> ( A u. B ) C_ ( _Old ` ( bday ` X ) ) )
	cofcutrtimed.2	|- ( ph -> A <
	cofcutrtimed.3	|- ( ph -> X = ( A |s B ) )
Assertion	cofcutrtime1d	|- ( ph -> A. x e. A E. y e. ( _Left ` X ) x <_s y )

Proof

Step	Hyp	Ref	Expression
1		cofcutrtimed.1	|- ( ph -> ( A u. B ) C_ ( _Old ` ( bday ` X ) ) )
2		cofcutrtimed.2	|- ( ph -> A <
3		cofcutrtimed.3	|- ( ph -> X = ( A |s B ) )
4		cofcutrtime	|- ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( A. x e. A E. y e. ( _Left ` X ) x <_s y /\ A. z e. B E. w e. ( _Right ` X ) w <_s z ) )
5	1 2 3 4	syl3anc	|- ( ph -> ( A. x e. A E. y e. ( _Left ` X ) x <_s y /\ A. z e. B E. w e. ( _Right ` X ) w <_s z ) )
6	5	simpld	|- ( ph -> A. x e. A E. y e. ( _Left ` X ) x <_s y )