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 | ⊢ ( 𝜑 → 𝐴 <<s 𝐵 ) | |
| cofcut2d.2 | ⊢ ( 𝜑 → 𝐶 ∈ 𝒫 No ) | ||
| cofcut2d.3 | ⊢ ( 𝜑 → 𝐷 ∈ 𝒫 No ) | ||
| cofcut2d.4 | ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ) | ||
| cofcut2d.5 | ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) | ||
| cofcut2d.6 | ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝐶 ∃ 𝑢 ∈ 𝐴 𝑡 ≤s 𝑢 ) | ||
| cofcut2d.7 | ⊢ ( 𝜑 → ∀ 𝑟 ∈ 𝐷 ∃ 𝑠 ∈ 𝐵 𝑠 ≤s 𝑟 ) | ||
| Assertion | cofcut2d | ⊢ ( 𝜑 → ( 𝐴 |s 𝐵 ) = ( 𝐶 |s 𝐷 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cofcut2d.1 | ⊢ ( 𝜑 → 𝐴 <<s 𝐵 ) | |
| 2 | cofcut2d.2 | ⊢ ( 𝜑 → 𝐶 ∈ 𝒫 No ) | |
| 3 | cofcut2d.3 | ⊢ ( 𝜑 → 𝐷 ∈ 𝒫 No ) | |
| 4 | cofcut2d.4 | ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ) | |
| 5 | cofcut2d.5 | ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) | |
| 6 | cofcut2d.6 | ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝐶 ∃ 𝑢 ∈ 𝐴 𝑡 ≤s 𝑢 ) | |
| 7 | cofcut2d.7 | ⊢ ( 𝜑 → ∀ 𝑟 ∈ 𝐷 ∃ 𝑠 ∈ 𝐵 𝑠 ≤s 𝑟 ) | |
| 8 | cofcut2 | ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ∈ 𝒫 No ∧ 𝐷 ∈ 𝒫 No ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( ∀ 𝑡 ∈ 𝐶 ∃ 𝑢 ∈ 𝐴 𝑡 ≤s 𝑢 ∧ ∀ 𝑟 ∈ 𝐷 ∃ 𝑠 ∈ 𝐵 𝑠 ≤s 𝑟 ) ) → ( 𝐴 |s 𝐵 ) = ( 𝐶 |s 𝐷 ) ) | |
| 9 | 1 2 3 4 5 6 7 8 | syl322anc | ⊢ ( 𝜑 → ( 𝐴 |s 𝐵 ) = ( 𝐶 |s 𝐷 ) ) |