Metamath Proof Explorer

Theorem mulsrid

Description: Surreal one is a right identity element for multiplication. (Contributed by Scott Fenton, 4-Feb-2025)

Ref Expression
Assertion mulsrid 
|- ( A e. No -> ( A x.s 1s ) = A )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( x = xO -> ( x x.s 1s ) = ( xO x.s 1s ) )
2 id 
 |-  ( x = xO -> x = xO )
3 1 2 eqeq12d 
 |-  ( x = xO -> ( ( x x.s 1s ) = x <-> ( xO x.s 1s ) = xO ) )
4 oveq1 
 |-  ( x = A -> ( x x.s 1s ) = ( A x.s 1s ) )
5 id 
 |-  ( x = A -> x = A )
6 4 5 eqeq12d 
 |-  ( x = A -> ( ( x x.s 1s ) = x <-> ( A x.s 1s ) = A ) )
7 1no 
 |-  1s e. No
8 mulsval 
 |-  ( ( x e. No /\ 1s e. No ) -> ( x x.s 1s ) = ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) ) )
9 7 8 mpan2 
 |-  ( x e. No -> ( x x.s 1s ) = ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) ) )
10 9 adantr 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( x x.s 1s ) = ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) ) )
11 elun1 
 |-  ( p e. ( _Left ` x ) -> p e. ( ( _Left ` x ) u. ( _Right ` x ) ) )
12 oveq1 
 |-  ( xO = p -> ( xO x.s 1s ) = ( p x.s 1s ) )
13 id 
 |-  ( xO = p -> xO = p )
14 12 13 eqeq12d 
 |-  ( xO = p -> ( ( xO x.s 1s ) = xO <-> ( p x.s 1s ) = p ) )
15 14 rspcva 
 |-  ( ( p e. ( ( _Left ` x ) u. ( _Right ` x ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( p x.s 1s ) = p )
16 11 15 sylan 
 |-  ( ( p e. ( _Left ` x ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( p x.s 1s ) = p )
17 16 ancoms 
 |-  ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO /\ p e. ( _Left ` x ) ) -> ( p x.s 1s ) = p )
18 17 adantll 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( p x.s 1s ) = p )
19 muls01 
 |-  ( x e. No -> ( x x.s 0s ) = 0s )
20 19 adantr 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( x x.s 0s ) = 0s )
21 20 adantr 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( x x.s 0s ) = 0s )
22 18 21 oveq12d 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( ( p x.s 1s ) +s ( x x.s 0s ) ) = ( p +s 0s ) )
23 leftno 
 |-  ( p e. ( _Left ` x ) -> p e. No )
24 23 adantl 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> p e. No )
25 24 addsridd 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( p +s 0s ) = p )
26 22 25 eqtrd 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( ( p x.s 1s ) +s ( x x.s 0s ) ) = p )
27 muls01 
 |-  ( p e. No -> ( p x.s 0s ) = 0s )
28 24 27 syl 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( p x.s 0s ) = 0s )
29 26 28 oveq12d 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) = ( p -s 0s ) )
30 subsid1 
 |-  ( p e. No -> ( p -s 0s ) = p )
31 24 30 syl 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( p -s 0s ) = p )
32 29 31 eqtrd 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) = p )
33 32 eqeq2d 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) <-> a = p ) )
34 equcom 
 |-  ( a = p <-> p = a )
35 33 34 bitrdi 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) <-> p = a ) )
36 35 rexbidva 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( E. p e. ( _Left ` x ) a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) <-> E. p e. ( _Left ` x ) p = a ) )
37 left1s 
 |-  ( _Left ` 1s ) = { 0s }
38 37 rexeqi 
 |-  ( E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> E. q e. { 0s } a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) )
39 0no 
 |-  0s e. No
40 39 elexi 
 |-  0s e. _V
41 oveq2 
 |-  ( q = 0s -> ( x x.s q ) = ( x x.s 0s ) )
42 41 oveq2d 
 |-  ( q = 0s -> ( ( p x.s 1s ) +s ( x x.s q ) ) = ( ( p x.s 1s ) +s ( x x.s 0s ) ) )
43 oveq2 
 |-  ( q = 0s -> ( p x.s q ) = ( p x.s 0s ) )
44 42 43 oveq12d 
 |-  ( q = 0s -> ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) )
45 44 eqeq2d 
 |-  ( q = 0s -> ( a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) ) )
46 40 45 rexsn 
 |-  ( E. q e. { 0s } a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) )
47 38 46 bitri 
 |-  ( E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) )
48 47 rexbii 
 |-  ( E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> E. p e. ( _Left ` x ) a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) )
49 risset 
 |-  ( a e. ( _Left ` x ) <-> E. p e. ( _Left ` x ) p = a )
50 36 48 49 3bitr4g 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> a e. ( _Left ` x ) ) )
51 50 eqabcdv 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } = ( _Left ` x ) )
52 rex0 
 |-  -. E. s e. (/) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) )
53 right1s 
 |-  ( _Right ` 1s ) = (/)
54 53 rexeqi 
 |-  ( E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) <-> E. s e. (/) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) )
55 52 54 mtbir 
 |-  -. E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) )
56 55 a1i 
 |-  ( r e. ( _Right ` x ) -> -. E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) )
57 56 nrex 
 |-  -. E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) )
58 57 abf 
 |-  { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } = (/)
59 58 a1i 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } = (/) )
60 51 59 uneq12d 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) = ( ( _Left ` x ) u. (/) ) )
61 un0 
 |-  ( ( _Left ` x ) u. (/) ) = ( _Left ` x )
62 60 61 eqtrdi 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) = ( _Left ` x ) )
63 rex0 
 |-  -. E. u e. (/) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) )
64 53 rexeqi 
 |-  ( E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) <-> E. u e. (/) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) )
65 63 64 mtbir 
 |-  -. E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) )
66 65 a1i 
 |-  ( t e. ( _Left ` x ) -> -. E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) )
67 66 nrex 
 |-  -. E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) )
68 67 abf 
 |-  { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } = (/)
69 68 a1i 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } = (/) )
70 elun2 
 |-  ( v e. ( _Right ` x ) -> v e. ( ( _Left ` x ) u. ( _Right ` x ) ) )
71 oveq1 
 |-  ( xO = v -> ( xO x.s 1s ) = ( v x.s 1s ) )
72 id 
 |-  ( xO = v -> xO = v )
73 71 72 eqeq12d 
 |-  ( xO = v -> ( ( xO x.s 1s ) = xO <-> ( v x.s 1s ) = v ) )
74 73 rspcva 
 |-  ( ( v e. ( ( _Left ` x ) u. ( _Right ` x ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( v x.s 1s ) = v )
75 70 74 sylan 
 |-  ( ( v e. ( _Right ` x ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( v x.s 1s ) = v )
76 75 ancoms 
 |-  ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO /\ v e. ( _Right ` x ) ) -> ( v x.s 1s ) = v )
77 76 adantll 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( v x.s 1s ) = v )
78 20 adantr 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( x x.s 0s ) = 0s )
79 77 78 oveq12d 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( ( v x.s 1s ) +s ( x x.s 0s ) ) = ( v +s 0s ) )
80 rightno 
 |-  ( v e. ( _Right ` x ) -> v e. No )
81 80 adantl 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> v e. No )
82 81 addsridd 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( v +s 0s ) = v )
83 79 82 eqtrd 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( ( v x.s 1s ) +s ( x x.s 0s ) ) = v )
84 muls01 
 |-  ( v e. No -> ( v x.s 0s ) = 0s )
85 81 84 syl 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( v x.s 0s ) = 0s )
86 83 85 oveq12d 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) = ( v -s 0s ) )
87 subsid1 
 |-  ( v e. No -> ( v -s 0s ) = v )
88 81 87 syl 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( v -s 0s ) = v )
89 86 88 eqtrd 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) = v )
90 89 eqeq2d 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( d = ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) <-> d = v ) )
91 37 rexeqi 
 |-  ( E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> E. w e. { 0s } d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) )
92 oveq2 
 |-  ( w = 0s -> ( x x.s w ) = ( x x.s 0s ) )
93 92 oveq2d 
 |-  ( w = 0s -> ( ( v x.s 1s ) +s ( x x.s w ) ) = ( ( v x.s 1s ) +s ( x x.s 0s ) ) )
94 oveq2 
 |-  ( w = 0s -> ( v x.s w ) = ( v x.s 0s ) )
95 93 94 oveq12d 
 |-  ( w = 0s -> ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) = ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) )
96 95 eqeq2d 
 |-  ( w = 0s -> ( d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> d = ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) ) )
97 40 96 rexsn 
 |-  ( E. w e. { 0s } d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> d = ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) )
98 91 97 bitri 
 |-  ( E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> d = ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) )
99 equcom 
 |-  ( v = d <-> d = v )
100 90 98 99 3bitr4g 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> v = d ) )
101 100 rexbidva 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> E. v e. ( _Right ` x ) v = d ) )
102 risset 
 |-  ( d e. ( _Right ` x ) <-> E. v e. ( _Right ` x ) v = d )
103 101 102 bitr4di 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> d e. ( _Right ` x ) ) )
104 103 eqabcdv 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } = ( _Right ` x ) )
105 69 104 uneq12d 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) = ( (/) u. ( _Right ` x ) ) )
106 0un 
 |-  ( (/) u. ( _Right ` x ) ) = ( _Right ` x )
107 105 106 eqtrdi 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) = ( _Right ` x ) )
108 62 107 oveq12d 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) ) = ( ( _Left ` x ) |s ( _Right ` x ) ) )
109 lrcut 
 |-  ( x e. No -> ( ( _Left ` x ) |s ( _Right ` x ) ) = x )
110 109 adantr 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( ( _Left ` x ) |s ( _Right ` x ) ) = x )
111 10 108 110 3eqtrd 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( x x.s 1s ) = x )
112 111 ex 
 |-  ( x e. No -> ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO -> ( x x.s 1s ) = x ) )
113 3 6 112 noinds 
 |-  ( A e. No -> ( A x.s 1s ) = A )