Metamath Proof Explorer


Theorem scutval

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

Ref Expression
Assertion scutval ( 𝐴 <<s 𝐵 → ( 𝐴 |s 𝐵 ) = ( 𝑥 ∈ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) )

Proof

Step Hyp Ref Expression
1 ssltex1 ( 𝐴 <<s 𝐵𝐴 ∈ V )
2 ssltss1 ( 𝐴 <<s 𝐵𝐴 No )
3 1 2 elpwd ( 𝐴 <<s 𝐵𝐴 ∈ 𝒫 No )
4 df-br ( 𝐴 <<s 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ <<s )
5 4 biimpi ( 𝐴 <<s 𝐵 → ⟨ 𝐴 , 𝐵 ⟩ ∈ <<s )
6 ssltex2 ( 𝐴 <<s 𝐵𝐵 ∈ V )
7 elimasng ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐵 ∈ ( <<s “ { 𝐴 } ) ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ <<s ) )
8 1 6 7 syl2anc ( 𝐴 <<s 𝐵 → ( 𝐵 ∈ ( <<s “ { 𝐴 } ) ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ <<s ) )
9 5 8 mpbird ( 𝐴 <<s 𝐵𝐵 ∈ ( <<s “ { 𝐴 } ) )
10 riotaex ( 𝑥 ∈ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) ∈ V
11 breq1 ( 𝑎 = 𝐴 → ( 𝑎 <<s { 𝑦 } ↔ 𝐴 <<s { 𝑦 } ) )
12 breq2 ( 𝑏 = 𝐵 → ( { 𝑦 } <<s 𝑏 ↔ { 𝑦 } <<s 𝐵 ) )
13 11 12 bi2anan9 ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) → ( ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) ↔ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) ) )
14 13 rabbidv ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) → { 𝑦 No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } = { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } )
15 14 imaeq2d ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) → ( bday “ { 𝑦 No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )
16 15 inteqd ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) → ( bday “ { 𝑦 No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )
17 16 eqeq2d ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) → ( ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ↔ ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) )
18 14 17 riotaeqbidv ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) → ( 𝑥 ∈ { 𝑦 No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) = ( 𝑥 ∈ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) )
19 sneq ( 𝑎 = 𝐴 → { 𝑎 } = { 𝐴 } )
20 19 imaeq2d ( 𝑎 = 𝐴 → ( <<s “ { 𝑎 } ) = ( <<s “ { 𝐴 } ) )
21 df-scut |s = ( 𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ { 𝑎 } ) ↦ ( 𝑥 ∈ { 𝑦 No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) )
22 18 20 21 ovmpox ( ( 𝐴 ∈ 𝒫 No 𝐵 ∈ ( <<s “ { 𝐴 } ) ∧ ( 𝑥 ∈ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) ∈ V ) → ( 𝐴 |s 𝐵 ) = ( 𝑥 ∈ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) )
23 10 22 mp3an3 ( ( 𝐴 ∈ 𝒫 No 𝐵 ∈ ( <<s “ { 𝐴 } ) ) → ( 𝐴 |s 𝐵 ) = ( 𝑥 ∈ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) )
24 3 9 23 syl2anc ( 𝐴 <<s 𝐵 → ( 𝐴 |s 𝐵 ) = ( 𝑥 ∈ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday 𝑥 ) = ( bday “ { 𝑦 No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) )