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 | |- ( ph -> A < |
|
| cofcut1d.2 | |- ( ph -> A. x e. A E. y e. C x <_s y ) |
||
| cofcut1d.3 | |- ( ph -> A. z e. B E. w e. D w <_s z ) |
||
| cofcut1d.4 | |- ( ph -> C < |
||
| cofcut1d.5 | |- ( ph -> { ( A |s B ) } < |
||
| Assertion | cofcut1d | |- ( ph -> ( A |s B ) = ( C |s D ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cofcut1d.1 | |- ( ph -> A < |
|
| 2 | cofcut1d.2 | |- ( ph -> A. x e. A E. y e. C x <_s y ) |
|
| 3 | cofcut1d.3 | |- ( ph -> A. z e. B E. w e. D w <_s z ) |
|
| 4 | cofcut1d.4 | |- ( ph -> C < |
|
| 5 | cofcut1d.5 | |- ( ph -> { ( A |s B ) } < |
|
| 6 | cofcut1 | |- ( ( A < |
|
| 7 | 1 2 3 4 5 6 | syl122anc | |- ( ph -> ( A |s B ) = ( C |s D ) ) |