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 1sno 
 |-  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 leftssno 
 |-  ( _Left ` x ) C_ No
24 23 sseli 
 |-  ( p e. ( _Left ` x ) -> p e. No )
25 24 adantl 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> p e. No )
26 25 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 )
27 22 26 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 )
28 muls01 
 |-  ( p e. No -> ( p x.s 0s ) = 0s )
29 25 28 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 )
30 27 29 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 ) )
31 subsid1 
 |-  ( p e. No -> ( p -s 0s ) = p )
32 25 31 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 )
33 30 32 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 )
34 33 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 ) )
35 equcom 
 |-  ( a = p <-> p = a )
36 34 35 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 ) )
37 36 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 ) )
38 left1s 
 |-  ( _Left ` 1s ) = { 0s }
39 38 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 ) ) )
40 0sno 
 |-  0s e. No
41 40 elexi 
 |-  0s e. _V
42 oveq2 
 |-  ( q = 0s -> ( x x.s q ) = ( x x.s 0s ) )
43 42 oveq2d 
 |-  ( q = 0s -> ( ( p x.s 1s ) +s ( x x.s q ) ) = ( ( p x.s 1s ) +s ( x x.s 0s ) ) )
44 oveq2 
 |-  ( q = 0s -> ( p x.s q ) = ( p x.s 0s ) )
45 43 44 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 ) ) )
46 45 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 ) ) ) )
47 41 46 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 ) ) )
48 39 47 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 ) ) )
49 48 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 ) ) )
50 risset 
 |-  ( a e. ( _Left ` x ) <-> E. p e. ( _Left ` x ) p = a )
51 37 49 50 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 ) ) )
52 51 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 ) )
53 rex0 
 |-  -. E. s e. (/) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) )
54 right1s 
 |-  ( _Right ` 1s ) = (/)
55 54 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 ) ) )
56 53 55 mtbir 
 |-  -. E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) )
57 56 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 ) ) )
58 57 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 ) )
59 58 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 ) ) } = (/)
60 59 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 ) ) } = (/) )
61 52 60 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. (/) ) )
62 un0 
 |-  ( ( _Left ` x ) u. (/) ) = ( _Left ` x )
63 61 62 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 ) )
64 rex0 
 |-  -. E. u e. (/) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) )
65 54 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 ) ) )
66 64 65 mtbir 
 |-  -. E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) )
67 66 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 ) ) )
68 67 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 ) )
69 68 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 ) ) } = (/)
70 69 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 ) ) } = (/) )
71 elun2 
 |-  ( v e. ( _Right ` x ) -> v e. ( ( _Left ` x ) u. ( _Right ` x ) ) )
72 oveq1 
 |-  ( xO = v -> ( xO x.s 1s ) = ( v x.s 1s ) )
73 id 
 |-  ( xO = v -> xO = v )
74 72 73 eqeq12d 
 |-  ( xO = v -> ( ( xO x.s 1s ) = xO <-> ( v x.s 1s ) = v ) )
75 74 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 )
76 71 75 sylan 
 |-  ( ( v e. ( _Right ` x ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( v x.s 1s ) = v )
77 76 ancoms 
 |-  ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO /\ v e. ( _Right ` x ) ) -> ( v x.s 1s ) = v )
78 77 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 )
79 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 )
80 78 79 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 ) )
81 rightssno 
 |-  ( _Right ` x ) C_ No
82 81 sseli 
 |-  ( v e. ( _Right ` x ) -> v e. No )
83 82 adantl 
 |-  ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> v e. No )
84 83 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 )
85 80 84 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 )
86 muls01 
 |-  ( v e. No -> ( v x.s 0s ) = 0s )
87 83 86 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 )
88 85 87 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 ) )
89 subsid1 
 |-  ( v e. No -> ( v -s 0s ) = v )
90 83 89 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 )
91 88 90 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 )
92 91 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 ) )
93 38 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 ) ) )
94 oveq2 
 |-  ( w = 0s -> ( x x.s w ) = ( x x.s 0s ) )
95 94 oveq2d 
 |-  ( w = 0s -> ( ( v x.s 1s ) +s ( x x.s w ) ) = ( ( v x.s 1s ) +s ( x x.s 0s ) ) )
96 oveq2 
 |-  ( w = 0s -> ( v x.s w ) = ( v x.s 0s ) )
97 95 96 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 ) ) )
98 97 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 ) ) ) )
99 41 98 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 ) ) )
100 93 99 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 ) ) )
101 equcom 
 |-  ( v = d <-> d = v )
102 92 100 101 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 ) )
103 102 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 ) )
104 risset 
 |-  ( d e. ( _Right ` x ) <-> E. v e. ( _Right ` x ) v = d )
105 103 104 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 ) ) )
106 105 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 ) )
107 70 106 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 ) ) )
108 0un 
 |-  ( (/) u. ( _Right ` x ) ) = ( _Right ` x )
109 107 108 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 ) )
110 63 109 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 ) ) )
111 lrcut 
 |-  ( x e. No -> ( ( _Left ` x ) |s ( _Right ` x ) ) = x )
112 111 adantr 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( ( _Left ` x ) |s ( _Right ` x ) ) = x )
113 10 110 112 3eqtrd 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( x x.s 1s ) = x )
114 113 ex 
 |-  ( x e. No -> ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO -> ( x x.s 1s ) = x ) )
115 3 6 114 noinds 
 |-  ( A e. No -> ( A x.s 1s ) = A )