Metamath Proof Explorer

Theorem scutf

Description: Functionhood 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 ∈ ≪ 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 dmscut ⊢ 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 scutval ⊢ 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 scutcut ⊢ a ≪ s b → a | s b ∈ No ∧ a ≪ s a | s b ∧ a | s b ≪ s b
14 13 simp1d ⊢ a ≪ s b → a | s b ∈ No
15 12 14 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
16 11 15 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
17 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
18 16 17 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
19 18 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
20 19 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
21 20 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
22 6 21 eqsstri ⊢ ran ⁡ | s ⊆ No
23 df-f ⊢ | s : ≪ s ⟶ No ↔ | s Fn ≪ s ∧ ran ⁡ | s ⊆ No
24 5 22 23 mpbir2an ⊢ | s : ≪ s ⟶ No