Metamath Proof Explorer

Theorem addsval2

Description: The value of surreal addition with different choices for each bound variable. Definition from Conway p. 5. (Contributed by Scott Fenton, 21-Jan-2025)

Ref Expression
Assertion addsval2 
|- ( ( A e. No /\ B e. No ) -> ( A +s B ) = ( ( { y | E. l e. ( _Left ` A ) y = ( l +s B ) } u. { z | E. m e. ( _Left ` B ) z = ( A +s m ) } ) |s ( { w | E. r e. ( _Right ` A ) w = ( r +s B ) } u. { t | E. s e. ( _Right ` B ) t = ( A +s s ) } ) ) )

Proof

Step Hyp Ref Expression
1 addsval 
 |-  ( ( A e. No /\ B e. No ) -> ( A +s B ) = ( ( { a | E. b e. ( _Left ` A ) a = ( b +s B ) } u. { c | E. b e. ( _Left ` B ) c = ( A +s b ) } ) |s ( { a | E. d e. ( _Right ` A ) a = ( d +s B ) } u. { c | E. d e. ( _Right ` B ) c = ( A +s d ) } ) ) )
2 eqeq1 
 |-  ( a = y -> ( a = ( b +s B ) <-> y = ( b +s B ) ) )
3 2 rexbidv 
 |-  ( a = y -> ( E. b e. ( _Left ` A ) a = ( b +s B ) <-> E. b e. ( _Left ` A ) y = ( b +s B ) ) )
4 oveq1 
 |-  ( b = l -> ( b +s B ) = ( l +s B ) )
5 4 eqeq2d 
 |-  ( b = l -> ( y = ( b +s B ) <-> y = ( l +s B ) ) )
6 5 cbvrexvw 
 |-  ( E. b e. ( _Left ` A ) y = ( b +s B ) <-> E. l e. ( _Left ` A ) y = ( l +s B ) )
7 3 6 bitrdi 
 |-  ( a = y -> ( E. b e. ( _Left ` A ) a = ( b +s B ) <-> E. l e. ( _Left ` A ) y = ( l +s B ) ) )
8 7 cbvabv 
 |-  { a | E. b e. ( _Left ` A ) a = ( b +s B ) } = { y | E. l e. ( _Left ` A ) y = ( l +s B ) }
9 eqeq1 
 |-  ( c = z -> ( c = ( A +s b ) <-> z = ( A +s b ) ) )
10 9 rexbidv 
 |-  ( c = z -> ( E. b e. ( _Left ` B ) c = ( A +s b ) <-> E. b e. ( _Left ` B ) z = ( A +s b ) ) )
11 oveq2 
 |-  ( b = m -> ( A +s b ) = ( A +s m ) )
12 11 eqeq2d 
 |-  ( b = m -> ( z = ( A +s b ) <-> z = ( A +s m ) ) )
13 12 cbvrexvw 
 |-  ( E. b e. ( _Left ` B ) z = ( A +s b ) <-> E. m e. ( _Left ` B ) z = ( A +s m ) )
14 10 13 bitrdi 
 |-  ( c = z -> ( E. b e. ( _Left ` B ) c = ( A +s b ) <-> E. m e. ( _Left ` B ) z = ( A +s m ) ) )
15 14 cbvabv 
 |-  { c | E. b e. ( _Left ` B ) c = ( A +s b ) } = { z | E. m e. ( _Left ` B ) z = ( A +s m ) }
16 8 15 uneq12i 
 |-  ( { a | E. b e. ( _Left ` A ) a = ( b +s B ) } u. { c | E. b e. ( _Left ` B ) c = ( A +s b ) } ) = ( { y | E. l e. ( _Left ` A ) y = ( l +s B ) } u. { z | E. m e. ( _Left ` B ) z = ( A +s m ) } )
17 eqeq1 
 |-  ( a = w -> ( a = ( d +s B ) <-> w = ( d +s B ) ) )
18 17 rexbidv 
 |-  ( a = w -> ( E. d e. ( _Right ` A ) a = ( d +s B ) <-> E. d e. ( _Right ` A ) w = ( d +s B ) ) )
19 oveq1 
 |-  ( d = r -> ( d +s B ) = ( r +s B ) )
20 19 eqeq2d 
 |-  ( d = r -> ( w = ( d +s B ) <-> w = ( r +s B ) ) )
21 20 cbvrexvw 
 |-  ( E. d e. ( _Right ` A ) w = ( d +s B ) <-> E. r e. ( _Right ` A ) w = ( r +s B ) )
22 18 21 bitrdi 
 |-  ( a = w -> ( E. d e. ( _Right ` A ) a = ( d +s B ) <-> E. r e. ( _Right ` A ) w = ( r +s B ) ) )
23 22 cbvabv 
 |-  { a | E. d e. ( _Right ` A ) a = ( d +s B ) } = { w | E. r e. ( _Right ` A ) w = ( r +s B ) }
24 eqeq1 
 |-  ( c = t -> ( c = ( A +s d ) <-> t = ( A +s d ) ) )
25 24 rexbidv 
 |-  ( c = t -> ( E. d e. ( _Right ` B ) c = ( A +s d ) <-> E. d e. ( _Right ` B ) t = ( A +s d ) ) )
26 oveq2 
 |-  ( d = s -> ( A +s d ) = ( A +s s ) )
27 26 eqeq2d 
 |-  ( d = s -> ( t = ( A +s d ) <-> t = ( A +s s ) ) )
28 27 cbvrexvw 
 |-  ( E. d e. ( _Right ` B ) t = ( A +s d ) <-> E. s e. ( _Right ` B ) t = ( A +s s ) )
29 25 28 bitrdi 
 |-  ( c = t -> ( E. d e. ( _Right ` B ) c = ( A +s d ) <-> E. s e. ( _Right ` B ) t = ( A +s s ) ) )
30 29 cbvabv 
 |-  { c | E. d e. ( _Right ` B ) c = ( A +s d ) } = { t | E. s e. ( _Right ` B ) t = ( A +s s ) }
31 23 30 uneq12i 
 |-  ( { a | E. d e. ( _Right ` A ) a = ( d +s B ) } u. { c | E. d e. ( _Right ` B ) c = ( A +s d ) } ) = ( { w | E. r e. ( _Right ` A ) w = ( r +s B ) } u. { t | E. s e. ( _Right ` B ) t = ( A +s s ) } )
32 16 31 oveq12i 
 |-  ( ( { a | E. b e. ( _Left ` A ) a = ( b +s B ) } u. { c | E. b e. ( _Left ` B ) c = ( A +s b ) } ) |s ( { a | E. d e. ( _Right ` A ) a = ( d +s B ) } u. { c | E. d e. ( _Right ` B ) c = ( A +s d ) } ) ) = ( ( { y | E. l e. ( _Left ` A ) y = ( l +s B ) } u. { z | E. m e. ( _Left ` B ) z = ( A +s m ) } ) |s ( { w | E. r e. ( _Right ` A ) w = ( r +s B ) } u. { t | E. s e. ( _Right ` B ) t = ( A +s s ) } ) )
33 1 32 eqtrdi 
 |-  ( ( A e. No /\ B e. No ) -> ( A +s B ) = ( ( { y | E. l e. ( _Left ` A ) y = ( l +s B ) } u. { z | E. m e. ( _Left ` B ) z = ( A +s m ) } ) |s ( { w | E. r e. ( _Right ` A ) w = ( r +s B ) } u. { t | E. s e. ( _Right ` B ) t = ( A +s s ) } ) ) )