Metamath Proof Explorer

Theorem addscom

Description: Surreal addition commutes. Part of Theorem 3 of Conway p. 17. (Contributed by Scott Fenton, 20-Aug-2024)

Ref Expression
Assertion addscom Could not format assertion : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( A +s B ) = ( B +s A ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 oveq1 Could not format ( x = xO -> ( x +s y ) = ( xO +s y ) ) : No typesetting found for |- ( x = xO -> ( x +s y ) = ( xO +s y ) ) with typecode |-
2 oveq2 Could not format ( x = xO -> ( y +s x ) = ( y +s xO ) ) : No typesetting found for |- ( x = xO -> ( y +s x ) = ( y +s xO ) ) with typecode |-
3 1 2 eqeq12d Could not format ( x = xO -> ( ( x +s y ) = ( y +s x ) <-> ( xO +s y ) = ( y +s xO ) ) ) : No typesetting found for |- ( x = xO -> ( ( x +s y ) = ( y +s x ) <-> ( xO +s y ) = ( y +s xO ) ) ) with typecode |-
4 oveq2 Could not format ( y = yO -> ( xO +s y ) = ( xO +s yO ) ) : No typesetting found for |- ( y = yO -> ( xO +s y ) = ( xO +s yO ) ) with typecode |-
5 oveq1 Could not format ( y = yO -> ( y +s xO ) = ( yO +s xO ) ) : No typesetting found for |- ( y = yO -> ( y +s xO ) = ( yO +s xO ) ) with typecode |-
6 4 5 eqeq12d Could not format ( y = yO -> ( ( xO +s y ) = ( y +s xO ) <-> ( xO +s yO ) = ( yO +s xO ) ) ) : No typesetting found for |- ( y = yO -> ( ( xO +s y ) = ( y +s xO ) <-> ( xO +s yO ) = ( yO +s xO ) ) ) with typecode |-
7 oveq1 Could not format ( x = xO -> ( x +s yO ) = ( xO +s yO ) ) : No typesetting found for |- ( x = xO -> ( x +s yO ) = ( xO +s yO ) ) with typecode |-
8 oveq2 Could not format ( x = xO -> ( yO +s x ) = ( yO +s xO ) ) : No typesetting found for |- ( x = xO -> ( yO +s x ) = ( yO +s xO ) ) with typecode |-
9 7 8 eqeq12d Could not format ( x = xO -> ( ( x +s yO ) = ( yO +s x ) <-> ( xO +s yO ) = ( yO +s xO ) ) ) : No typesetting found for |- ( x = xO -> ( ( x +s yO ) = ( yO +s x ) <-> ( xO +s yO ) = ( yO +s xO ) ) ) with typecode |-
10 oveq1 Could not format ( x = A -> ( x +s y ) = ( A +s y ) ) : No typesetting found for |- ( x = A -> ( x +s y ) = ( A +s y ) ) with typecode |-
11 oveq2 Could not format ( x = A -> ( y +s x ) = ( y +s A ) ) : No typesetting found for |- ( x = A -> ( y +s x ) = ( y +s A ) ) with typecode |-
12 10 11 eqeq12d Could not format ( x = A -> ( ( x +s y ) = ( y +s x ) <-> ( A +s y ) = ( y +s A ) ) ) : No typesetting found for |- ( x = A -> ( ( x +s y ) = ( y +s x ) <-> ( A +s y ) = ( y +s A ) ) ) with typecode |-
13 oveq2 Could not format ( y = B -> ( A +s y ) = ( A +s B ) ) : No typesetting found for |- ( y = B -> ( A +s y ) = ( A +s B ) ) with typecode |-
14 oveq1 Could not format ( y = B -> ( y +s A ) = ( B +s A ) ) : No typesetting found for |- ( y = B -> ( y +s A ) = ( B +s A ) ) with typecode |-
15 13 14 eqeq12d Could not format ( y = B -> ( ( A +s y ) = ( y +s A ) <-> ( A +s B ) = ( B +s A ) ) ) : No typesetting found for |- ( y = B -> ( ( A +s y ) = ( y +s A ) <-> ( A +s B ) = ( B +s A ) ) ) with typecode |-
16 simpr2 Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) ) with typecode |-
17 elun1 ⊢ l ∈ L ⁡ x → l ∈ L ⁡ x ∪ R ⁡ x
18 oveq1 Could not format ( xO = l -> ( xO +s y ) = ( l +s y ) ) : No typesetting found for |- ( xO = l -> ( xO +s y ) = ( l +s y ) ) with typecode |-
19 oveq2 Could not format ( xO = l -> ( y +s xO ) = ( y +s l ) ) : No typesetting found for |- ( xO = l -> ( y +s xO ) = ( y +s l ) ) with typecode |-
20 18 19 eqeq12d Could not format ( xO = l -> ( ( xO +s y ) = ( y +s xO ) <-> ( l +s y ) = ( y +s l ) ) ) : No typesetting found for |- ( xO = l -> ( ( xO +s y ) = ( y +s xO ) <-> ( l +s y ) = ( y +s l ) ) ) with typecode |-
21 20 rspccva Could not format ( ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ l e. ( ( _L ` x ) u. ( _R ` x ) ) ) -> ( l +s y ) = ( y +s l ) ) : No typesetting found for |- ( ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ l e. ( ( _L ` x ) u. ( _R ` x ) ) ) -> ( l +s y ) = ( y +s l ) ) with typecode |-
22 16 17 21 syl2an Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) /\ l e. ( _L ` x ) ) -> ( l +s y ) = ( y +s l ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) /\ l e. ( _L ` x ) ) -> ( l +s y ) = ( y +s l ) ) with typecode |-
23 22 eqeq2d Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) /\ l e. ( _L ` x ) ) -> ( w = ( l +s y ) <-> w = ( y +s l ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) /\ l e. ( _L ` x ) ) -> ( w = ( l +s y ) <-> w = ( y +s l ) ) ) with typecode |-
24 23 rexbidva Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( E. l e. ( _L ` x ) w = ( l +s y ) <-> E. l e. ( _L ` x ) w = ( y +s l ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( E. l e. ( _L ` x ) w = ( l +s y ) <-> E. l e. ( _L ` x ) w = ( y +s l ) ) ) with typecode |-
25 24 abbidv Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> { w | E. l e. ( _L ` x ) w = ( l +s y ) } = { w | E. l e. ( _L ` x ) w = ( y +s l ) } ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> { w | E. l e. ( _L ` x ) w = ( l +s y ) } = { w | E. l e. ( _L ` x ) w = ( y +s l ) } ) with typecode |-
26 simpr3 Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) with typecode |-
27 elun1 ⊢ l ∈ L ⁡ y → l ∈ L ⁡ y ∪ R ⁡ y
28 oveq2 Could not format ( yO = l -> ( x +s yO ) = ( x +s l ) ) : No typesetting found for |- ( yO = l -> ( x +s yO ) = ( x +s l ) ) with typecode |-
29 oveq1 Could not format ( yO = l -> ( yO +s x ) = ( l +s x ) ) : No typesetting found for |- ( yO = l -> ( yO +s x ) = ( l +s x ) ) with typecode |-
30 28 29 eqeq12d Could not format ( yO = l -> ( ( x +s yO ) = ( yO +s x ) <-> ( x +s l ) = ( l +s x ) ) ) : No typesetting found for |- ( yO = l -> ( ( x +s yO ) = ( yO +s x ) <-> ( x +s l ) = ( l +s x ) ) ) with typecode |-
31 30 rspccva Could not format ( ( A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) /\ l e. ( ( _L ` y ) u. ( _R ` y ) ) ) -> ( x +s l ) = ( l +s x ) ) : No typesetting found for |- ( ( A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) /\ l e. ( ( _L ` y ) u. ( _R ` y ) ) ) -> ( x +s l ) = ( l +s x ) ) with typecode |-
32 26 27 31 syl2an Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) /\ l e. ( _L ` y ) ) -> ( x +s l ) = ( l +s x ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) /\ l e. ( _L ` y ) ) -> ( x +s l ) = ( l +s x ) ) with typecode |-
33 32 eqeq2d Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) /\ l e. ( _L ` y ) ) -> ( z = ( x +s l ) <-> z = ( l +s x ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) /\ l e. ( _L ` y ) ) -> ( z = ( x +s l ) <-> z = ( l +s x ) ) ) with typecode |-
34 33 rexbidva Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( E. l e. ( _L ` y ) z = ( x +s l ) <-> E. l e. ( _L ` y ) z = ( l +s x ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( E. l e. ( _L ` y ) z = ( x +s l ) <-> E. l e. ( _L ` y ) z = ( l +s x ) ) ) with typecode |-
35 34 abbidv Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> { z | E. l e. ( _L ` y ) z = ( x +s l ) } = { z | E. l e. ( _L ` y ) z = ( l +s x ) } ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> { z | E. l e. ( _L ` y ) z = ( x +s l ) } = { z | E. l e. ( _L ` y ) z = ( l +s x ) } ) with typecode |-
36 25 35 uneq12d Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( { w | E. l e. ( _L ` x ) w = ( l +s y ) } u. { z | E. l e. ( _L ` y ) z = ( x +s l ) } ) = ( { w | E. l e. ( _L ` x ) w = ( y +s l ) } u. { z | E. l e. ( _L ` y ) z = ( l +s x ) } ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( { w | E. l e. ( _L ` x ) w = ( l +s y ) } u. { z | E. l e. ( _L ` y ) z = ( x +s l ) } ) = ( { w | E. l e. ( _L ` x ) w = ( y +s l ) } u. { z | E. l e. ( _L ` y ) z = ( l +s x ) } ) ) with typecode |-
37 uncom Could not format ( { w | E. l e. ( _L ` x ) w = ( y +s l ) } u. { z | E. l e. ( _L ` y ) z = ( l +s x ) } ) = ( { z | E. l e. ( _L ` y ) z = ( l +s x ) } u. { w | E. l e. ( _L ` x ) w = ( y +s l ) } ) : No typesetting found for |- ( { w | E. l e. ( _L ` x ) w = ( y +s l ) } u. { z | E. l e. ( _L ` y ) z = ( l +s x ) } ) = ( { z | E. l e. ( _L ` y ) z = ( l +s x ) } u. { w | E. l e. ( _L ` x ) w = ( y +s l ) } ) with typecode |-
38 36 37 eqtrdi Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( { w | E. l e. ( _L ` x ) w = ( l +s y ) } u. { z | E. l e. ( _L ` y ) z = ( x +s l ) } ) = ( { z | E. l e. ( _L ` y ) z = ( l +s x ) } u. { w | E. l e. ( _L ` x ) w = ( y +s l ) } ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( { w | E. l e. ( _L ` x ) w = ( l +s y ) } u. { z | E. l e. ( _L ` y ) z = ( x +s l ) } ) = ( { z | E. l e. ( _L ` y ) z = ( l +s x ) } u. { w | E. l e. ( _L ` x ) w = ( y +s l ) } ) ) with typecode |-
39 elun2 ⊢ r ∈ R ⁡ x → r ∈ L ⁡ x ∪ R ⁡ x
40 oveq1 Could not format ( xO = r -> ( xO +s y ) = ( r +s y ) ) : No typesetting found for |- ( xO = r -> ( xO +s y ) = ( r +s y ) ) with typecode |-
41 oveq2 Could not format ( xO = r -> ( y +s xO ) = ( y +s r ) ) : No typesetting found for |- ( xO = r -> ( y +s xO ) = ( y +s r ) ) with typecode |-
42 40 41 eqeq12d Could not format ( xO = r -> ( ( xO +s y ) = ( y +s xO ) <-> ( r +s y ) = ( y +s r ) ) ) : No typesetting found for |- ( xO = r -> ( ( xO +s y ) = ( y +s xO ) <-> ( r +s y ) = ( y +s r ) ) ) with typecode |-
43 42 rspccva Could not format ( ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ r e. ( ( _L ` x ) u. ( _R ` x ) ) ) -> ( r +s y ) = ( y +s r ) ) : No typesetting found for |- ( ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ r e. ( ( _L ` x ) u. ( _R ` x ) ) ) -> ( r +s y ) = ( y +s r ) ) with typecode |-
44 16 39 43 syl2an Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) /\ r e. ( _R ` x ) ) -> ( r +s y ) = ( y +s r ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) /\ r e. ( _R ` x ) ) -> ( r +s y ) = ( y +s r ) ) with typecode |-
45 44 eqeq2d Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) /\ r e. ( _R ` x ) ) -> ( w = ( r +s y ) <-> w = ( y +s r ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) /\ r e. ( _R ` x ) ) -> ( w = ( r +s y ) <-> w = ( y +s r ) ) ) with typecode |-
46 45 rexbidva Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( E. r e. ( _R ` x ) w = ( r +s y ) <-> E. r e. ( _R ` x ) w = ( y +s r ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( E. r e. ( _R ` x ) w = ( r +s y ) <-> E. r e. ( _R ` x ) w = ( y +s r ) ) ) with typecode |-
47 46 abbidv Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> { w | E. r e. ( _R ` x ) w = ( r +s y ) } = { w | E. r e. ( _R ` x ) w = ( y +s r ) } ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> { w | E. r e. ( _R ` x ) w = ( r +s y ) } = { w | E. r e. ( _R ` x ) w = ( y +s r ) } ) with typecode |-
48 elun2 ⊢ r ∈ R ⁡ y → r ∈ L ⁡ y ∪ R ⁡ y
49 oveq2 Could not format ( yO = r -> ( x +s yO ) = ( x +s r ) ) : No typesetting found for |- ( yO = r -> ( x +s yO ) = ( x +s r ) ) with typecode |-
50 oveq1 Could not format ( yO = r -> ( yO +s x ) = ( r +s x ) ) : No typesetting found for |- ( yO = r -> ( yO +s x ) = ( r +s x ) ) with typecode |-
51 49 50 eqeq12d Could not format ( yO = r -> ( ( x +s yO ) = ( yO +s x ) <-> ( x +s r ) = ( r +s x ) ) ) : No typesetting found for |- ( yO = r -> ( ( x +s yO ) = ( yO +s x ) <-> ( x +s r ) = ( r +s x ) ) ) with typecode |-
52 51 rspccva Could not format ( ( A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) /\ r e. ( ( _L ` y ) u. ( _R ` y ) ) ) -> ( x +s r ) = ( r +s x ) ) : No typesetting found for |- ( ( A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) /\ r e. ( ( _L ` y ) u. ( _R ` y ) ) ) -> ( x +s r ) = ( r +s x ) ) with typecode |-
53 26 48 52 syl2an Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) /\ r e. ( _R ` y ) ) -> ( x +s r ) = ( r +s x ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) /\ r e. ( _R ` y ) ) -> ( x +s r ) = ( r +s x ) ) with typecode |-
54 53 eqeq2d Could not format ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) /\ r e. ( _R ` y ) ) -> ( z = ( x +s r ) <-> z = ( r +s x ) ) ) : No typesetting found for |- ( ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) /\ r e. ( _R ` y ) ) -> ( z = ( x +s r ) <-> z = ( r +s x ) ) ) with typecode |-
55 54 rexbidva Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( E. r e. ( _R ` y ) z = ( x +s r ) <-> E. r e. ( _R ` y ) z = ( r +s x ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( E. r e. ( _R ` y ) z = ( x +s r ) <-> E. r e. ( _R ` y ) z = ( r +s x ) ) ) with typecode |-
56 55 abbidv Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> { z | E. r e. ( _R ` y ) z = ( x +s r ) } = { z | E. r e. ( _R ` y ) z = ( r +s x ) } ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> { z | E. r e. ( _R ` y ) z = ( x +s r ) } = { z | E. r e. ( _R ` y ) z = ( r +s x ) } ) with typecode |-
57 47 56 uneq12d Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( { w | E. r e. ( _R ` x ) w = ( r +s y ) } u. { z | E. r e. ( _R ` y ) z = ( x +s r ) } ) = ( { w | E. r e. ( _R ` x ) w = ( y +s r ) } u. { z | E. r e. ( _R ` y ) z = ( r +s x ) } ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( { w | E. r e. ( _R ` x ) w = ( r +s y ) } u. { z | E. r e. ( _R ` y ) z = ( x +s r ) } ) = ( { w | E. r e. ( _R ` x ) w = ( y +s r ) } u. { z | E. r e. ( _R ` y ) z = ( r +s x ) } ) ) with typecode |-
58 uncom Could not format ( { w | E. r e. ( _R ` x ) w = ( y +s r ) } u. { z | E. r e. ( _R ` y ) z = ( r +s x ) } ) = ( { z | E. r e. ( _R ` y ) z = ( r +s x ) } u. { w | E. r e. ( _R ` x ) w = ( y +s r ) } ) : No typesetting found for |- ( { w | E. r e. ( _R ` x ) w = ( y +s r ) } u. { z | E. r e. ( _R ` y ) z = ( r +s x ) } ) = ( { z | E. r e. ( _R ` y ) z = ( r +s x ) } u. { w | E. r e. ( _R ` x ) w = ( y +s r ) } ) with typecode |-
59 57 58 eqtrdi Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( { w | E. r e. ( _R ` x ) w = ( r +s y ) } u. { z | E. r e. ( _R ` y ) z = ( x +s r ) } ) = ( { z | E. r e. ( _R ` y ) z = ( r +s x ) } u. { w | E. r e. ( _R ` x ) w = ( y +s r ) } ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( { w | E. r e. ( _R ` x ) w = ( r +s y ) } u. { z | E. r e. ( _R ` y ) z = ( x +s r ) } ) = ( { z | E. r e. ( _R ` y ) z = ( r +s x ) } u. { w | E. r e. ( _R ` x ) w = ( y +s r ) } ) ) with typecode |-
60 38 59 oveq12d Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( ( { w | E. l e. ( _L ` x ) w = ( l +s y ) } u. { z | E. l e. ( _L ` y ) z = ( x +s l ) } ) |s ( { w | E. r e. ( _R ` x ) w = ( r +s y ) } u. { z | E. r e. ( _R ` y ) z = ( x +s r ) } ) ) = ( ( { z | E. l e. ( _L ` y ) z = ( l +s x ) } u. { w | E. l e. ( _L ` x ) w = ( y +s l ) } ) |s ( { z | E. r e. ( _R ` y ) z = ( r +s x ) } u. { w | E. r e. ( _R ` x ) w = ( y +s r ) } ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( ( { w | E. l e. ( _L ` x ) w = ( l +s y ) } u. { z | E. l e. ( _L ` y ) z = ( x +s l ) } ) |s ( { w | E. r e. ( _R ` x ) w = ( r +s y ) } u. { z | E. r e. ( _R ` y ) z = ( x +s r ) } ) ) = ( ( { z | E. l e. ( _L ` y ) z = ( l +s x ) } u. { w | E. l e. ( _L ` x ) w = ( y +s l ) } ) |s ( { z | E. r e. ( _R ` y ) z = ( r +s x ) } u. { w | E. r e. ( _R ` x ) w = ( y +s r ) } ) ) ) with typecode |-
61 addsov Could not format ( ( x e. No /\ y e. No ) -> ( x +s y ) = ( ( { w | E. l e. ( _L ` x ) w = ( l +s y ) } u. { z | E. l e. ( _L ` y ) z = ( x +s l ) } ) |s ( { w | E. r e. ( _R ` x ) w = ( r +s y ) } u. { z | E. r e. ( _R ` y ) z = ( x +s r ) } ) ) ) : No typesetting found for |- ( ( x e. No /\ y e. No ) -> ( x +s y ) = ( ( { w | E. l e. ( _L ` x ) w = ( l +s y ) } u. { z | E. l e. ( _L ` y ) z = ( x +s l ) } ) |s ( { w | E. r e. ( _R ` x ) w = ( r +s y ) } u. { z | E. r e. ( _R ` y ) z = ( x +s r ) } ) ) ) with typecode |-
62 61 adantr Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( x +s y ) = ( ( { w | E. l e. ( _L ` x ) w = ( l +s y ) } u. { z | E. l e. ( _L ` y ) z = ( x +s l ) } ) |s ( { w | E. r e. ( _R ` x ) w = ( r +s y ) } u. { z | E. r e. ( _R ` y ) z = ( x +s r ) } ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( x +s y ) = ( ( { w | E. l e. ( _L ` x ) w = ( l +s y ) } u. { z | E. l e. ( _L ` y ) z = ( x +s l ) } ) |s ( { w | E. r e. ( _R ` x ) w = ( r +s y ) } u. { z | E. r e. ( _R ` y ) z = ( x +s r ) } ) ) ) with typecode |-
63 addsov Could not format ( ( y e. No /\ x e. No ) -> ( y +s x ) = ( ( { z | E. l e. ( _L ` y ) z = ( l +s x ) } u. { w | E. l e. ( _L ` x ) w = ( y +s l ) } ) |s ( { z | E. r e. ( _R ` y ) z = ( r +s x ) } u. { w | E. r e. ( _R ` x ) w = ( y +s r ) } ) ) ) : No typesetting found for |- ( ( y e. No /\ x e. No ) -> ( y +s x ) = ( ( { z | E. l e. ( _L ` y ) z = ( l +s x ) } u. { w | E. l e. ( _L ` x ) w = ( y +s l ) } ) |s ( { z | E. r e. ( _R ` y ) z = ( r +s x ) } u. { w | E. r e. ( _R ` x ) w = ( y +s r ) } ) ) ) with typecode |-
64 63 ancoms Could not format ( ( x e. No /\ y e. No ) -> ( y +s x ) = ( ( { z | E. l e. ( _L ` y ) z = ( l +s x ) } u. { w | E. l e. ( _L ` x ) w = ( y +s l ) } ) |s ( { z | E. r e. ( _R ` y ) z = ( r +s x ) } u. { w | E. r e. ( _R ` x ) w = ( y +s r ) } ) ) ) : No typesetting found for |- ( ( x e. No /\ y e. No ) -> ( y +s x ) = ( ( { z | E. l e. ( _L ` y ) z = ( l +s x ) } u. { w | E. l e. ( _L ` x ) w = ( y +s l ) } ) |s ( { z | E. r e. ( _R ` y ) z = ( r +s x ) } u. { w | E. r e. ( _R ` x ) w = ( y +s r ) } ) ) ) with typecode |-
65 64 adantr Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( y +s x ) = ( ( { z | E. l e. ( _L ` y ) z = ( l +s x ) } u. { w | E. l e. ( _L ` x ) w = ( y +s l ) } ) |s ( { z | E. r e. ( _R ` y ) z = ( r +s x ) } u. { w | E. r e. ( _R ` x ) w = ( y +s r ) } ) ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( y +s x ) = ( ( { z | E. l e. ( _L ` y ) z = ( l +s x ) } u. { w | E. l e. ( _L ` x ) w = ( y +s l ) } ) |s ( { z | E. r e. ( _R ` y ) z = ( r +s x ) } u. { w | E. r e. ( _R ` x ) w = ( y +s r ) } ) ) ) with typecode |-
66 60 62 65 3eqtr4d Could not format ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( x +s y ) = ( y +s x ) ) : No typesetting found for |- ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) ) -> ( x +s y ) = ( y +s x ) ) with typecode |-
67 66 ex Could not format ( ( x e. No /\ y e. No ) -> ( ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) -> ( x +s y ) = ( y +s x ) ) ) : No typesetting found for |- ( ( x e. No /\ y e. No ) -> ( ( A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( xO +s yO ) = ( yO +s xO ) /\ A. xO e. ( ( _L ` x ) u. ( _R ` x ) ) ( xO +s y ) = ( y +s xO ) /\ A. yO e. ( ( _L ` y ) u. ( _R ` y ) ) ( x +s yO ) = ( yO +s x ) ) -> ( x +s y ) = ( y +s x ) ) ) with typecode |-
68 3 6 9 12 15 67 no2inds Could not format ( ( A e. No /\ B e. No ) -> ( A +s B ) = ( B +s A ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( A +s B ) = ( B +s A ) ) with typecode |-