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	|- ( ( ( A < ( A |s B ) = ( C |s D ) )

Proof

Step	Hyp	Ref	Expression
1		simp11	|- ( ( ( A < A <
2		simp2	|- ( ( ( A < ( A. x e. A E. y e. C x <_s y /\ A. z e. B E. w e. D w <_s z ) )
3		simp12	|- ( ( ( A < C e. ~P No )
4		simp3l	|- ( ( ( A < A. t e. C E. u e. A t <_s u )
5		scutcut	|- ( A < ( ( A |s B ) e. No /\ A <
6	1 5	syl	|- ( ( ( A < ( ( A |s B ) e. No /\ A <
7	6	simp2d	|- ( ( ( A < A <
8		cofsslt	|- ( ( C e. ~P No /\ A. t e. C E. u e. A t <_s u /\ A < C <
9	3 4 7 8	syl3anc	|- ( ( ( A < C <
10		simp13	|- ( ( ( A < D e. ~P No )
11		simp3r	|- ( ( ( A < A. r e. D E. s e. B s <_s r )
12	6	simp3d	|- ( ( ( A < { ( A |s B ) } <
13		coinitsslt	|- ( ( D e. ~P No /\ A. r e. D E. s e. B s <_s r /\ { ( A |s B ) } < { ( A |s B ) } <
14	10 11 12 13	syl3anc	|- ( ( ( A < { ( A |s B ) } <
15		cofcut1	|- ( ( A < ( A |s B ) = ( C |s D ) )
16	1 2 9 14 15	syl112anc	|- ( ( ( A < ( A |s B ) = ( C |s D ) )