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 = ( 𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ { 𝑎 } ) ↦ ( 𝑥 ∈ { 𝑦 No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) )
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 = { 𝑧 ∣ ∃ 𝑎 ∈ 𝒫 No 𝑏 ∈ ( <<s “ { 𝑎 } ) 𝑧 = ( 𝑥 ∈ { 𝑦 No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) }
7 vex 𝑎 ∈ V
8 vex 𝑏 ∈ V
9 7 8 elimasn ( 𝑏 ∈ ( <<s “ { 𝑎 } ) ↔ ⟨ 𝑎 , 𝑏 ⟩ ∈ <<s )
10 df-br ( 𝑎 <<s 𝑏 ↔ ⟨ 𝑎 , 𝑏 ⟩ ∈ <<s )
11 9 10 bitr4i ( 𝑏 ∈ ( <<s “ { 𝑎 } ) ↔ 𝑎 <<s 𝑏 )
12 scutval ( 𝑎 <<s 𝑏 → ( 𝑎 |s 𝑏 ) = ( 𝑥 ∈ { 𝑦 No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) )
13 scutcl ( 𝑎 <<s 𝑏 → ( 𝑎 |s 𝑏 ) ∈ No )
14 12 13 eqeltrrd ( 𝑎 <<s 𝑏 → ( 𝑥 ∈ { 𝑦 No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) ∈ No )
15 11 14 sylbi ( 𝑏 ∈ ( <<s “ { 𝑎 } ) → ( 𝑥 ∈ { 𝑦 No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) ∈ No )
16 eleq1a ( ( 𝑥 ∈ { 𝑦 No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) ∈ No → ( 𝑧 = ( 𝑥 ∈ { 𝑦 No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) → 𝑧 No ) )
17 15 16 syl ( 𝑏 ∈ ( <<s “ { 𝑎 } ) → ( 𝑧 = ( 𝑥 ∈ { 𝑦 No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) → 𝑧 No ) )
18 17 adantl ( ( 𝑎 ∈ 𝒫 No 𝑏 ∈ ( <<s “ { 𝑎 } ) ) → ( 𝑧 = ( 𝑥 ∈ { 𝑦 No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) → 𝑧 No ) )
19 18 rexlimivv ( ∃ 𝑎 ∈ 𝒫 No 𝑏 ∈ ( <<s “ { 𝑎 } ) 𝑧 = ( 𝑥 ∈ { 𝑦 No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) → 𝑧 No )
20 19 abssi { 𝑧 ∣ ∃ 𝑎 ∈ 𝒫 No 𝑏 ∈ ( <<s “ { 𝑎 } ) 𝑧 = ( 𝑥 ∈ { 𝑦 No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) } ⊆ 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