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	$$⊢\phi \to \forall x\in A\exists y\in L\left(X\right)x{\le }_{s}y$$

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	$$⊢\left(A\cup B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\wedge A{\ll }_{s}B\wedge X=A{|}_{s}B\right)\to \left(\forall x\in A\exists y\in L\left(X\right)x{\le }_{s}y\wedge \forall z\in B\exists w\in R\left(X\right)w{\le }_{s}z\right)$$
5	1 2 3 4	syl3anc	$$⊢\phi \to \left(\forall x\in A\exists y\in L\left(X\right)x{\le }_{s}y\wedge \forall z\in B\exists w\in R\left(X\right)w{\le }_{s}z\right)$$
6	5	simpld	$$⊢\phi \to \forall x\in A\exists y\in L\left(X\right)x{\le }_{s}y$$