Metamath Proof Explorer

Theorem cutsf

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

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

Proof

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