Metamath Proof Explorer

Theorem scutf

Description: Functionality statement for the surreal cut operator. (Contributed by Scott Fenton, 15-Dec-2021)

Ref Expression
Assertion scutf ⊢|s:≪s⟶No

Proof

Step Hyp Ref Expression
1 df-scut ⊢|s=a∈𝒫No,b∈≪sa⟼ιx∈y∈No|a≪sy∧y≪sb|bday⁡x=⋂bdayy∈No|a≪sy∧y≪sb
2 1 mpofun ⊢Fun⁡|s
3 dmscut ⊢dom⁡|s=≪s
4 df-fn ⊢|sFn≪s↔Fun⁡|s∧dom⁡|s=≪s
5 2 3 4 mpbir2an ⊢|sFn≪s
6 1 rnmpo ⊢ran⁡|s=z|∃a∈𝒫No∃b∈≪saz=ιx∈y∈No|a≪sy∧y≪sb|bday⁡x=⋂bdayy∈No|a≪sy∧y≪sb
7 vex ⊢a∈V
8 vex ⊢b∈V
9 7 8 elimasn ⊢b∈≪sa↔ab∈≪s
10 df-br ⊢a≪sb↔ab∈≪s
11 9 10 bitr4i ⊢b∈≪sa↔a≪sb
12 scutval ⊢a≪sb→a|sb=ιx∈y∈No|a≪sy∧y≪sb|bday⁡x=⋂bdayy∈No|a≪sy∧y≪sb
13 scutcl ⊢a≪sb→a|sb∈No
14 12 13 eqeltrrd ⊢a≪sb→ιx∈y∈No|a≪sy∧y≪sb|bday⁡x=⋂bdayy∈No|a≪sy∧y≪sb∈No
15 11 14 sylbi ⊢b∈≪sa→ιx∈y∈No|a≪sy∧y≪sb|bday⁡x=⋂bdayy∈No|a≪sy∧y≪sb∈No
16 eleq1a ⊢ιx∈y∈No|a≪sy∧y≪sb|bday⁡x=⋂bdayy∈No|a≪sy∧y≪sb∈No→z=ιx∈y∈No|a≪sy∧y≪sb|bday⁡x=⋂bdayy∈No|a≪sy∧y≪sb→z∈No
17 15 16 syl ⊢b∈≪sa→z=ιx∈y∈No|a≪sy∧y≪sb|bday⁡x=⋂bdayy∈No|a≪sy∧y≪sb→z∈No
18 17 adantl ⊢a∈𝒫No∧b∈≪sa→z=ιx∈y∈No|a≪sy∧y≪sb|bday⁡x=⋂bdayy∈No|a≪sy∧y≪sb→z∈No
19 18 rexlimivv ⊢∃a∈𝒫No∃b∈≪saz=ιx∈y∈No|a≪sy∧y≪sb|bday⁡x=⋂bdayy∈No|a≪sy∧y≪sb→z∈No
20 19 abssi ⊢z|∃a∈𝒫No∃b∈≪saz=ιx∈y∈No|a≪sy∧y≪sb|bday⁡x=⋂bdayy∈No|a≪sy∧y≪sb⊆No
21 6 20 eqsstri ⊢ran⁡|s⊆No
22 df-f ⊢|s:≪s⟶No↔|sFn≪s∧ran⁡|s⊆No
23 5 21 22 mpbir2an ⊢|s:≪s⟶No