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 Could not format assertion : No typesetting found for |- ( ( 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 ) } ) ) ) with typecode |-

Proof

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