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 | ⊢ ( 𝜑 → 𝐴 <<s 𝐵 ) | |
| cofcut1d.2 | ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ) | ||
| cofcut1d.3 | ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) | ||
| cofcut1d.4 | ⊢ ( 𝜑 → 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ) | ||
| cofcut1d.5 | ⊢ ( 𝜑 → { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) | ||
| Assertion | cofcut1d | ⊢ ( 𝜑 → ( 𝐴 |s 𝐵 ) = ( 𝐶 |s 𝐷 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cofcut1d.1 | ⊢ ( 𝜑 → 𝐴 <<s 𝐵 ) | |
| 2 | cofcut1d.2 | ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ) | |
| 3 | cofcut1d.3 | ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) | |
| 4 | cofcut1d.4 | ⊢ ( 𝜑 → 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ) | |
| 5 | cofcut1d.5 | ⊢ ( 𝜑 → { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) | |
| 6 | cofcut1 | ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) → ( 𝐴 |s 𝐵 ) = ( 𝐶 |s 𝐷 ) ) | |
| 7 | 1 2 3 4 5 6 | syl122anc | ⊢ ( 𝜑 → ( 𝐴 |s 𝐵 ) = ( 𝐶 |s 𝐷 ) ) |