Theorem cofcut1d

Description: If C is cofinal with A and D is coinitial with B and the cut of A and B lies between C and D , then the cut of C and D is equal to the cut of A and B . Theorem 2.6 of Gonshor p. 10. (Contributed by Scott Fenton, 23-Jan-2025)

	Ref	Expression
Hypotheses	cofcut1d.1	$$⊢\phi \to A{\ll }_{s}B$$
	cofcut1d.2	$$⊢\phi \to \forall x\in A\exists y\in Cx{\le }_{s}y$$
	cofcut1d.3	$$⊢\phi \to \forall z\in B\exists w\in Dw{\le }_{s}z$$
	cofcut1d.4	$$⊢\phi \to C{\ll }_s\left\{A{|}_{s}B\right\}$$
	cofcut1d.5	$$⊢\phi \to \left\{A{|}_{s}B\right\}{\ll }_{s}D$$
Assertion	cofcut1d	$$⊢\phi \to A{|}_{s}B=C{|}_{s}D$$

Proof

Step	Hyp	Ref	Expression
1		cofcut1d.1	$$⊢\phi \to A{\ll }_{s}B$$
2		cofcut1d.2	$$⊢\phi \to \forall x\in A\exists y\in Cx{\le }_{s}y$$
3		cofcut1d.3	$$⊢\phi \to \forall z\in B\exists w\in Dw{\le }_{s}z$$
4		cofcut1d.4	$$⊢\phi \to C{\ll }_s\left\{A{|}_{s}B\right\}$$
5		cofcut1d.5	$$⊢\phi \to \left\{A{|}_{s}B\right\}{\ll }_{s}D$$
6		cofcut1	$$⊢\left(A{\ll }_{s}B\wedge \left(\forall x\in A\exists y\in Cx{\le }_{s}y\wedge \forall z\in B\exists w\in Dw{\le }_{s}z\right)\wedge \left(C{\ll }_s\left\{A{|}_{s}B\right\}\wedge \left\{A{|}_{s}B\right\}{\ll }_{s}D\right)\right)\to A{|}_{s}B=C{|}_{s}D$$
7	1 2 3 4 5 6	syl122anc	$$⊢\phi \to A{|}_{s}B=C{|}_{s}D$$