Metamath Proof Explorer

Theorem scutcut

Description: Cut properties of the surreal cut operation. (Contributed by Scott Fenton, 8-Dec-2021)

Ref Expression
Assertion scutcut ⊢A≪sB→A|sB∈No∧A≪sA|sB∧A|sB≪sB

Proof

Step Hyp Ref Expression
1 scutval ⊢A≪sB→A|sB=ιx∈y∈No|A≪sy∧y≪sB|bday⁡x=⋂bdayy∈No|A≪sy∧y≪sB
2 conway ⊢A≪sB→∃!x∈y∈No|A≪sy∧y≪sBbday⁡x=⋂bdayy∈No|A≪sy∧y≪sB
3 riotacl ⊢∃!x∈y∈No|A≪sy∧y≪sBbday⁡x=⋂bdayy∈No|A≪sy∧y≪sB→ιx∈y∈No|A≪sy∧y≪sB|bday⁡x=⋂bdayy∈No|A≪sy∧y≪sB∈y∈No|A≪sy∧y≪sB
4 2 3 syl ⊢A≪sB→ιx∈y∈No|A≪sy∧y≪sB|bday⁡x=⋂bdayy∈No|A≪sy∧y≪sB∈y∈No|A≪sy∧y≪sB
5 1 4 eqeltrd ⊢A≪sB→A|sB∈y∈No|A≪sy∧y≪sB
6 sneq ⊢y=A|sB→y=A|sB
7 6 breq2d ⊢y=A|sB→A≪sy↔A≪sA|sB
8 6 breq1d ⊢y=A|sB→y≪sB↔A|sB≪sB
9 7 8 anbi12d ⊢y=A|sB→A≪sy∧y≪sB↔A≪sA|sB∧A|sB≪sB
10 9 elrab ⊢A|sB∈y∈No|A≪sy∧y≪sB↔A|sB∈No∧A≪sA|sB∧A|sB≪sB
11 3anass ⊢A|sB∈No∧A≪sA|sB∧A|sB≪sB↔A|sB∈No∧A≪sA|sB∧A|sB≪sB
12 10 11 bitr4i ⊢A|sB∈y∈No|A≪sy∧y≪sB↔A|sB∈No∧A≪sA|sB∧A|sB≪sB
13 5 12 sylib ⊢A≪sB→A|sB∈No∧A≪sA|sB∧A|sB≪sB