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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp11 | |
|
2 | simp2 | |
|
3 | simp12 | |
|
4 | simp3l | |
|
5 | scutcut | |
|
6 | 1 5 | syl | |
7 | 6 | simp2d | |
8 | cofsslt | |
|
9 | 3 4 7 8 | syl3anc | |
10 | simp13 | |
|
11 | simp3r | |
|
12 | 6 | simp3d | |
13 | coinitsslt | |
|
14 | 10 11 12 13 | syl3anc | |
15 | cofcut1 | |
|
16 | 1 2 9 14 15 | syl112anc | |