Description: Closure law for surreal cuts. (Contributed by Scott Fenton, 23-Aug-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | scutcl | ⊢ ( 𝐴 <<s 𝐵 → ( 𝐴 |s 𝐵 ) ∈ No ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | scutcut | ⊢ ( 𝐴 <<s 𝐵 → ( ( 𝐴 |s 𝐵 ) ∈ No ∧ 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) ) | |
2 | 1 | simp1d | ⊢ ( 𝐴 <<s 𝐵 → ( 𝐴 |s 𝐵 ) ∈ No ) |