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	$$⊢\phi \to A\cup B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)$$
	cofcutrtimed.2	$$⊢\phi \to A{\ll }_{s}B$$
	cofcutrtimed.3	$$⊢\phi \to X=A{|}_{s}B$$
Assertion	cofcutrtime1d	Could not format assertion : No typesetting found for |- ( ph -> A. x e. A E. y e. ( _Left ` X ) x <_s y ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		cofcutrtimed.1	$$⊢\phi \to A\cup B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)$$
2		cofcutrtimed.2	$$⊢\phi \to A{\ll }_{s}B$$
3		cofcutrtimed.3	$$⊢\phi \to X=A{|}_{s}B$$
4		cofcutrtime	Could not format ( ( ( 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 ) ) : No typesetting found for |- ( ( ( 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 ) ) with typecode |-
5	1 2 3 4	syl3anc	Could not format ( 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 ) ) : No typesetting found for |- ( 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 ) ) with typecode |-
6	5	simpld	Could not format ( ph -> A. x e. A E. y e. ( _Left ` X ) x <_s y ) : No typesetting found for |- ( ph -> A. x e. A E. y e. ( _Left ` X ) x <_s y ) with typecode |-