Metamath Proof Explorer

Theorem cutsval

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

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

Proof

Step Hyp Ref Expression
1 sltsex1 ⊢ ( 𝐴 <<s 𝐵 → 𝐴 ∈ V )
2 sltsss1 ⊢ ( 𝐴 <<s 𝐵 → 𝐴 ⊆ No )
3 1 2 elpwd ⊢ ( 𝐴 <<s 𝐵 → 𝐴 ∈ 𝒫 No )
4 df-br ⊢ ( 𝐴 <<s 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ <<s )
5 4 biimpi ⊢ ( 𝐴 <<s 𝐵 → ⟨ 𝐴 , 𝐵 ⟩ ∈ <<s )
6 sltsex2 ⊢ ( 𝐴 <<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-cuts ⊢ |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 𝐵 ) } ) ) )