Theorem cofcut2d

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

	Ref	Expression
Hypotheses	cofcut2d.1	$$⊢\phi \to A{\ll }_{s}B$$
	cofcut2d.2	$$⊢\phi \to C\in 𝒫\mathrm{No}$$
	cofcut2d.3	$$⊢\phi \to D\in 𝒫\mathrm{No}$$
	cofcut2d.4	$$⊢\phi \to \forall x\in A\exists y\in Cx{\le }_{s}y$$
	cofcut2d.5	$$⊢\phi \to \forall z\in B\exists w\in Dw{\le }_{s}z$$
	cofcut2d.6	$$⊢\phi \to \forall t\in C\exists u\in At{\le }_{s}u$$
	cofcut2d.7	$$⊢\phi \to \forall r\in D\exists s\in Bs{\le }_{s}r$$
Assertion	cofcut2d	$$⊢\phi \to A{|}_{s}B=C{|}_{s}D$$

Proof

Step	Hyp	Ref	Expression
1		cofcut2d.1	$$⊢\phi \to A{\ll }_{s}B$$
2		cofcut2d.2	$$⊢\phi \to C\in 𝒫\mathrm{No}$$
3		cofcut2d.3	$$⊢\phi \to D\in 𝒫\mathrm{No}$$
4		cofcut2d.4	$$⊢\phi \to \forall x\in A\exists y\in Cx{\le }_{s}y$$
5		cofcut2d.5	$$⊢\phi \to \forall z\in B\exists w\in Dw{\le }_{s}z$$
6		cofcut2d.6	$$⊢\phi \to \forall t\in C\exists u\in At{\le }_{s}u$$
7		cofcut2d.7	$$⊢\phi \to \forall r\in D\exists s\in Bs{\le }_{s}r$$
8		cofcut2	$$⊢\left(\left(A{\ll }_{s}B\wedge C\in 𝒫\mathrm{No}\wedge D\in 𝒫\mathrm{No}\right)\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(\forall t\in C\exists u\in At{\le }_{s}u\wedge \forall r\in D\exists s\in Bs{\le }_{s}r\right)\right)\to A{|}_{s}B=C{|}_{s}D$$
9	1 2 3 4 5 6 7 8	syl322anc	$$⊢\phi \to A{|}_{s}B=C{|}_{s}D$$