Metamath Proof Explorer


Theorem cofcut2

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, 25-Sep-2024)

Ref Expression
Assertion cofcut2 AsBC𝒫NoD𝒫NoxAyCxsyzBwDwsztCuAtsurDsBssrA|sB=C|sD

Proof

Step Hyp Ref Expression
1 simp11 AsBC𝒫NoD𝒫NoxAyCxsyzBwDwsztCuAtsurDsBssrAsB
2 simp2 AsBC𝒫NoD𝒫NoxAyCxsyzBwDwsztCuAtsurDsBssrxAyCxsyzBwDwsz
3 simp12 AsBC𝒫NoD𝒫NoxAyCxsyzBwDwsztCuAtsurDsBssrC𝒫No
4 simp3l AsBC𝒫NoD𝒫NoxAyCxsyzBwDwsztCuAtsurDsBssrtCuAtsu
5 scutcut AsBA|sBNoAsA|sBA|sBsB
6 1 5 syl AsBC𝒫NoD𝒫NoxAyCxsyzBwDwsztCuAtsurDsBssrA|sBNoAsA|sBA|sBsB
7 6 simp2d AsBC𝒫NoD𝒫NoxAyCxsyzBwDwsztCuAtsurDsBssrAsA|sB
8 cofsslt C𝒫NotCuAtsuAsA|sBCsA|sB
9 3 4 7 8 syl3anc AsBC𝒫NoD𝒫NoxAyCxsyzBwDwsztCuAtsurDsBssrCsA|sB
10 simp13 AsBC𝒫NoD𝒫NoxAyCxsyzBwDwsztCuAtsurDsBssrD𝒫No
11 simp3r AsBC𝒫NoD𝒫NoxAyCxsyzBwDwsztCuAtsurDsBssrrDsBssr
12 6 simp3d AsBC𝒫NoD𝒫NoxAyCxsyzBwDwsztCuAtsurDsBssrA|sBsB
13 coinitsslt D𝒫NorDsBssrA|sBsBA|sBsD
14 10 11 12 13 syl3anc AsBC𝒫NoD𝒫NoxAyCxsyzBwDwsztCuAtsurDsBssrA|sBsD
15 cofcut1 AsBxAyCxsyzBwDwszCsA|sBA|sBsDA|sB=C|sD
16 1 2 9 14 15 syl112anc AsBC𝒫NoD𝒫NoxAyCxsyzBwDwsztCuAtsurDsBssrA|sB=C|sD