Metamath Proof Explorer

Theorem divsval

Description: The value of surreal division. (Contributed by Scott Fenton, 12-Mar-2025)

Ref Expression
Assertion divsval 
|- ( ( A e. No /\ B e. No /\ B =/= 0s ) -> ( A /su B ) = ( iota_ x e. No ( B x.s x ) = A ) )

Proof

Step Hyp Ref Expression
1 eldifsn 
 |-  ( B e. ( No \ { 0s } ) <-> ( B e. No /\ B =/= 0s ) )
2 eqeq2 
 |-  ( y = A -> ( ( z x.s x ) = y <-> ( z x.s x ) = A ) )
3 2 riotabidv 
 |-  ( y = A -> ( iota_ x e. No ( z x.s x ) = y ) = ( iota_ x e. No ( z x.s x ) = A ) )
4 oveq1 
 |-  ( z = B -> ( z x.s x ) = ( B x.s x ) )
5 4 eqeq1d 
 |-  ( z = B -> ( ( z x.s x ) = A <-> ( B x.s x ) = A ) )
6 5 riotabidv 
 |-  ( z = B -> ( iota_ x e. No ( z x.s x ) = A ) = ( iota_ x e. No ( B x.s x ) = A ) )
7 df-divs 
 |-  /su = ( y e. No , z e. ( No \ { 0s } ) |-> ( iota_ x e. No ( z x.s x ) = y ) )
8 riotaex 
 |-  ( iota_ x e. No ( B x.s x ) = A ) e. _V
9 3 6 7 8 ovmpo 
 |-  ( ( A e. No /\ B e. ( No \ { 0s } ) ) -> ( A /su B ) = ( iota_ x e. No ( B x.s x ) = A ) )
10 1 9 sylan2br 
 |-  ( ( A e. No /\ ( B e. No /\ B =/= 0s ) ) -> ( A /su B ) = ( iota_ x e. No ( B x.s x ) = A ) )
11 10 3impb 
 |-  ( ( A e. No /\ B e. No /\ B =/= 0s ) -> ( A /su B ) = ( iota_ x e. No ( B x.s x ) = A ) )