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 | |- ( ph -> A < |
|
| cofcut2d.2 | |- ( ph -> C e. ~P No ) |
||
| cofcut2d.3 | |- ( ph -> D e. ~P No ) |
||
| cofcut2d.4 | |- ( ph -> A. x e. A E. y e. C x <_s y ) |
||
| cofcut2d.5 | |- ( ph -> A. z e. B E. w e. D w <_s z ) |
||
| cofcut2d.6 | |- ( ph -> A. t e. C E. u e. A t <_s u ) |
||
| cofcut2d.7 | |- ( ph -> A. r e. D E. s e. B s <_s r ) |
||
| Assertion | cofcut2d | |- ( ph -> ( A |s B ) = ( C |s D ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cofcut2d.1 | |- ( ph -> A < |
|
| 2 | cofcut2d.2 | |- ( ph -> C e. ~P No ) |
|
| 3 | cofcut2d.3 | |- ( ph -> D e. ~P No ) |
|
| 4 | cofcut2d.4 | |- ( ph -> A. x e. A E. y e. C x <_s y ) |
|
| 5 | cofcut2d.5 | |- ( ph -> A. z e. B E. w e. D w <_s z ) |
|
| 6 | cofcut2d.6 | |- ( ph -> A. t e. C E. u e. A t <_s u ) |
|
| 7 | cofcut2d.7 | |- ( ph -> A. r e. D E. s e. B s <_s r ) |
|
| 8 | cofcut2 | |- ( ( ( A < |
|
| 9 | 1 2 3 4 5 6 7 8 | syl322anc | |- ( ph -> ( A |s B ) = ( C |s D ) ) |