Metamath Proof Explorer

Theorem precsexlem11

Description: Lemma for surreal reciprocal. Show that the cut of the left and right sets is a multiplicative inverse for A . (Contributed by Scott Fenton, 15-Mar-2025)

Ref Expression
Hypotheses precsexlem.1 
|- F = rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. )
precsexlem.2 
|- L = ( 1st o. F )
precsexlem.3 
|- R = ( 2nd o. F )
precsexlem.4 
|- ( ph -> A e. No )
precsexlem.5 
|- ( ph -> 0s
precsexlem.6 
|- ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s  E. y e. No ( xO x.s y ) = 1s ) )
precsexlem.7 
|- Y = ( U. ( L " _om ) |s U. ( R " _om ) )
Assertion precsexlem11 
|- ( ph -> ( A x.s Y ) = 1s )

Proof

Step Hyp Ref Expression
1 precsexlem.1 
 |-  F = rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. )
2 precsexlem.2 
 |-  L = ( 1st o. F )
3 precsexlem.3 
 |-  R = ( 2nd o. F )
4 precsexlem.4 
 |-  ( ph -> A e. No )
5 precsexlem.5 
 |-  ( ph -> 0s
6 precsexlem.6 
 |-  ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s  E. y e. No ( xO x.s y ) = 1s ) )
7 precsexlem.7 
 |-  Y = ( U. ( L " _om ) |s U. ( R " _om ) )
8 lltropt 
 |-  ( _Left ` A ) <
9 4 5 0elleft 
 |-  ( ph -> 0s e. ( _Left ` A ) )
10 9 snssd 
 |-  ( ph -> { 0s } C_ ( _Left ` A ) )
11 ssrab2 
 |-  { x e. ( _Left ` A ) | 0s
12 11 a1i 
 |-  ( ph -> { x e. ( _Left ` A ) | 0s
13 10 12 unssd 
 |-  ( ph -> ( { 0s } u. { x e. ( _Left ` A ) | 0s
14 sssslt1 
 |-  ( ( ( _Left ` A ) < ( { 0s } u. { x e. ( _Left ` A ) | 0s
15 8 13 14 sylancr 
 |-  ( ph -> ( { 0s } u. { x e. ( _Left ` A ) | 0s
16 1 2 3 4 5 6 precsexlem10 
 |-  ( ph -> U. ( L " _om ) <
17 4 5 cutpos 
 |-  ( ph -> A = ( ( { 0s } u. { x e. ( _Left ` A ) | 0s
18 7 a1i 
 |-  ( ph -> Y = ( U. ( L " _om ) |s U. ( R " _om ) ) )
19 15 16 17 18 mulsunif 
 |-  ( ph -> ( A x.s Y ) = ( ( { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s
20 0sno 
 |-  0s e. No
21 20 elexi 
 |-  0s e. _V
22 21 snid 
 |-  0s e. { 0s }
23 elun1 
 |-  ( 0s e. { 0s } -> 0s e. ( { 0s } u. { x e. ( _Left ` A ) | 0s
24 22 23 ax-mp 
 |-  0s e. ( { 0s } u. { x e. ( _Left ` A ) | 0s
25 peano1 
 |-  (/) e. _om
26 1 2 3 precsexlem1 
 |-  ( L ` (/) ) = { 0s }
27 22 26 eleqtrri 
 |-  0s e. ( L ` (/) )
28 fveq2 
 |-  ( b = (/) -> ( L ` b ) = ( L ` (/) ) )
29 28 eleq2d 
 |-  ( b = (/) -> ( 0s e. ( L ` b ) <-> 0s e. ( L ` (/) ) ) )
30 29 rspcev 
 |-  ( ( (/) e. _om /\ 0s e. ( L ` (/) ) ) -> E. b e. _om 0s e. ( L ` b ) )
31 25 27 30 mp2an 
 |-  E. b e. _om 0s e. ( L ` b )
32 eliun 
 |-  ( 0s e. U_ b e. _om ( L ` b ) <-> E. b e. _om 0s e. ( L ` b ) )
33 31 32 mpbir 
 |-  0s e. U_ b e. _om ( L ` b )
34 fo1st 
 |-  1st : _V -onto-> _V
35 fofun 
 |-  ( 1st : _V -onto-> _V -> Fun 1st )
36 34 35 ax-mp 
 |-  Fun 1st
37 rdgfun 
 |-  Fun rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. )
38 1 funeqi 
 |-  ( Fun F <-> Fun rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. ) )
39 37 38 mpbir 
 |-  Fun F
40 funco 
 |-  ( ( Fun 1st /\ Fun F ) -> Fun ( 1st o. F ) )
41 36 39 40 mp2an 
 |-  Fun ( 1st o. F )
42 2 funeqi 
 |-  ( Fun L <-> Fun ( 1st o. F ) )
43 41 42 mpbir 
 |-  Fun L
44 funiunfv 
 |-  ( Fun L -> U_ b e. _om ( L ` b ) = U. ( L " _om ) )
45 43 44 ax-mp 
 |-  U_ b e. _om ( L ` b ) = U. ( L " _om )
46 33 45 eleqtri 
 |-  0s e. U. ( L " _om )
47 addsrid 
 |-  ( 0s e. No -> ( 0s +s 0s ) = 0s )
48 20 47 ax-mp 
 |-  ( 0s +s 0s ) = 0s
49 muls01 
 |-  ( 0s e. No -> ( 0s x.s 0s ) = 0s )
50 20 49 ax-mp 
 |-  ( 0s x.s 0s ) = 0s
51 48 50 oveq12i 
 |-  ( ( 0s +s 0s ) -s ( 0s x.s 0s ) ) = ( 0s -s 0s )
52 subsid 
 |-  ( 0s e. No -> ( 0s -s 0s ) = 0s )
53 20 52 ax-mp 
 |-  ( 0s -s 0s ) = 0s
54 51 53 eqtr2i 
 |-  0s = ( ( 0s +s 0s ) -s ( 0s x.s 0s ) )
55 16 scutcld 
 |-  ( ph -> ( U. ( L " _om ) |s U. ( R " _om ) ) e. No )
56 7 55 eqeltrid 
 |-  ( ph -> Y e. No )
57 muls02 
 |-  ( Y e. No -> ( 0s x.s Y ) = 0s )
58 56 57 syl 
 |-  ( ph -> ( 0s x.s Y ) = 0s )
59 muls01 
 |-  ( A e. No -> ( A x.s 0s ) = 0s )
60 4 59 syl 
 |-  ( ph -> ( A x.s 0s ) = 0s )
61 58 60 oveq12d 
 |-  ( ph -> ( ( 0s x.s Y ) +s ( A x.s 0s ) ) = ( 0s +s 0s ) )
62 61 oveq1d 
 |-  ( ph -> ( ( ( 0s x.s Y ) +s ( A x.s 0s ) ) -s ( 0s x.s 0s ) ) = ( ( 0s +s 0s ) -s ( 0s x.s 0s ) ) )
63 54 62 eqtr4id 
 |-  ( ph -> 0s = ( ( ( 0s x.s Y ) +s ( A x.s 0s ) ) -s ( 0s x.s 0s ) ) )
64 oveq1 
 |-  ( c = 0s -> ( c x.s Y ) = ( 0s x.s Y ) )
65 64 oveq1d 
 |-  ( c = 0s -> ( ( c x.s Y ) +s ( A x.s d ) ) = ( ( 0s x.s Y ) +s ( A x.s d ) ) )
66 oveq1 
 |-  ( c = 0s -> ( c x.s d ) = ( 0s x.s d ) )
67 65 66 oveq12d 
 |-  ( c = 0s -> ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) = ( ( ( 0s x.s Y ) +s ( A x.s d ) ) -s ( 0s x.s d ) ) )
68 67 eqeq2d 
 |-  ( c = 0s -> ( 0s = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) <-> 0s = ( ( ( 0s x.s Y ) +s ( A x.s d ) ) -s ( 0s x.s d ) ) ) )
69 oveq2 
 |-  ( d = 0s -> ( A x.s d ) = ( A x.s 0s ) )
70 69 oveq2d 
 |-  ( d = 0s -> ( ( 0s x.s Y ) +s ( A x.s d ) ) = ( ( 0s x.s Y ) +s ( A x.s 0s ) ) )
71 oveq2 
 |-  ( d = 0s -> ( 0s x.s d ) = ( 0s x.s 0s ) )
72 70 71 oveq12d 
 |-  ( d = 0s -> ( ( ( 0s x.s Y ) +s ( A x.s d ) ) -s ( 0s x.s d ) ) = ( ( ( 0s x.s Y ) +s ( A x.s 0s ) ) -s ( 0s x.s 0s ) ) )
73 72 eqeq2d 
 |-  ( d = 0s -> ( 0s = ( ( ( 0s x.s Y ) +s ( A x.s d ) ) -s ( 0s x.s d ) ) <-> 0s = ( ( ( 0s x.s Y ) +s ( A x.s 0s ) ) -s ( 0s x.s 0s ) ) ) )
74 68 73 rspc2ev 
 |-  ( ( 0s e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s
75 24 46 63 74 mp3an12i 
 |-  ( ph -> E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s
76 eqeq1 
 |-  ( b = 0s -> ( b = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) <-> 0s = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) )
77 76 2rexbidv 
 |-  ( b = 0s -> ( E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s
78 21 77 elab 
 |-  ( 0s e. { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s
79 75 78 sylibr 
 |-  ( ph -> 0s e. { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s
80 elun1 
 |-  ( 0s e. { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  0s e. ( { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s
81 79 80 syl 
 |-  ( ph -> 0s e. ( { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s
82 eqid 
 |-  ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) = ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) )
83 82 rnmpo 
 |-  ran ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) = { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s
84 ssltex1 
 |-  ( ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( { 0s } u. { x e. ( _Left ` A ) | 0s
85 15 84 syl 
 |-  ( ph -> ( { 0s } u. { x e. ( _Left ` A ) | 0s
86 ssltex1 
 |-  ( U. ( L " _om ) < U. ( L " _om ) e. _V )
87 16 86 syl 
 |-  ( ph -> U. ( L " _om ) e. _V )
88 mpoexga 
 |-  ( ( ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) e. _V )
89 85 87 88 syl2anc 
 |-  ( ph -> ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) e. _V )
90 rnexg 
 |-  ( ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) e. _V -> ran ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) e. _V )
91 89 90 syl 
 |-  ( ph -> ran ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) e. _V )
92 83 91 eqeltrrid 
 |-  ( ph -> { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s
93 eqid 
 |-  ( c e. ( _Right ` A ) , d e. U. ( R " _om ) |-> ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) = ( c e. ( _Right ` A ) , d e. U. ( R " _om ) |-> ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) )
94 93 rnmpo 
 |-  ran ( c e. ( _Right ` A ) , d e. U. ( R " _om ) |-> ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) = { b | E. c e. ( _Right ` A ) E. d e. U. ( R " _om ) b = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) }
95 fvex 
 |-  ( _Right ` A ) e. _V
96 ssltex2 
 |-  ( U. ( L " _om ) < U. ( R " _om ) e. _V )
97 16 96 syl 
 |-  ( ph -> U. ( R " _om ) e. _V )
98 mpoexga 
 |-  ( ( ( _Right ` A ) e. _V /\ U. ( R " _om ) e. _V ) -> ( c e. ( _Right ` A ) , d e. U. ( R " _om ) |-> ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) e. _V )
99 95 97 98 sylancr 
 |-  ( ph -> ( c e. ( _Right ` A ) , d e. U. ( R " _om ) |-> ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) e. _V )
100 rnexg 
 |-  ( ( c e. ( _Right ` A ) , d e. U. ( R " _om ) |-> ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) e. _V -> ran ( c e. ( _Right ` A ) , d e. U. ( R " _om ) |-> ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) e. _V )
101 99 100 syl 
 |-  ( ph -> ran ( c e. ( _Right ` A ) , d e. U. ( R " _om ) |-> ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) e. _V )
102 94 101 eqeltrrid 
 |-  ( ph -> { b | E. c e. ( _Right ` A ) E. d e. U. ( R " _om ) b = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) } e. _V )
103 92 102 unexd 
 |-  ( ph -> ( { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s
104 snex 
 |-  { 1s } e. _V
105 104 a1i 
 |-  ( ph -> { 1s } e. _V )
106 ssltss1 
 |-  ( ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( { 0s } u. { x e. ( _Left ` A ) | 0s
107 15 106 syl 
 |-  ( ph -> ( { 0s } u. { x e. ( _Left ` A ) | 0s
108 107 sselda 
 |-  ( ( ph /\ c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  c e. No )
109 108 adantrr 
 |-  ( ( ph /\ ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  c e. No )
110 56 adantr 
 |-  ( ( ph /\ ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  Y e. No )
111 109 110 mulscld 
 |-  ( ( ph /\ ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( c x.s Y ) e. No )
112 4 adantr 
 |-  ( ( ph /\ ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  A e. No )
113 ssltss1 
 |-  ( U. ( L " _om ) < U. ( L " _om ) C_ No )
114 16 113 syl 
 |-  ( ph -> U. ( L " _om ) C_ No )
115 114 sselda 
 |-  ( ( ph /\ d e. U. ( L " _om ) ) -> d e. No )
116 115 adantrl 
 |-  ( ( ph /\ ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  d e. No )
117 112 116 mulscld 
 |-  ( ( ph /\ ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( A x.s d ) e. No )
118 111 117 addscld 
 |-  ( ( ph /\ ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( ( c x.s Y ) +s ( A x.s d ) ) e. No )
119 109 116 mulscld 
 |-  ( ( ph /\ ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( c x.s d ) e. No )
120 118 119 subscld 
 |-  ( ( ph /\ ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) e. No )
121 eleq1 
 |-  ( b = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) -> ( b e. No <-> ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) e. No ) )
122 120 121 syl5ibrcom 
 |-  ( ( ph /\ ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( b = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) -> b e. No ) )
123 122 rexlimdvva 
 |-  ( ph -> ( E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  b e. No ) )
124 123 abssdv 
 |-  ( ph -> { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s
125 rightssno 
 |-  ( _Right ` A ) C_ No
126 125 a1i 
 |-  ( ph -> ( _Right ` A ) C_ No )
127 126 sselda 
 |-  ( ( ph /\ c e. ( _Right ` A ) ) -> c e. No )
128 127 adantrr 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> c e. No )
129 56 adantr 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> Y e. No )
130 128 129 mulscld 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> ( c x.s Y ) e. No )
131 4 adantr 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> A e. No )
132 ssltss2 
 |-  ( U. ( L " _om ) < U. ( R " _om ) C_ No )
133 16 132 syl 
 |-  ( ph -> U. ( R " _om ) C_ No )
134 133 sselda 
 |-  ( ( ph /\ d e. U. ( R " _om ) ) -> d e. No )
135 134 adantrl 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> d e. No )
136 131 135 mulscld 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> ( A x.s d ) e. No )
137 130 136 addscld 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> ( ( c x.s Y ) +s ( A x.s d ) ) e. No )
138 128 135 mulscld 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> ( c x.s d ) e. No )
139 137 138 subscld 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) e. No )
140 139 121 syl5ibrcom 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> ( b = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) -> b e. No ) )
141 140 rexlimdvva 
 |-  ( ph -> ( E. c e. ( _Right ` A ) E. d e. U. ( R " _om ) b = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) -> b e. No ) )
142 141 abssdv 
 |-  ( ph -> { b | E. c e. ( _Right ` A ) E. d e. U. ( R " _om ) b = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) } C_ No )
143 124 142 unssd 
 |-  ( ph -> ( { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s
144 1sno 
 |-  1s e. No
145 snssi 
 |-  ( 1s e. No -> { 1s } C_ No )
146 144 145 mp1i 
 |-  ( ph -> { 1s } C_ No )
147 elun 
 |-  ( e e. ( { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( e e. { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s
148 vex 
 |-  e e. _V
149 eqeq1 
 |-  ( b = e -> ( b = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) <-> e = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) )
150 149 2rexbidv 
 |-  ( b = e -> ( E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s
151 148 150 elab 
 |-  ( e e. { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s
152 149 2rexbidv 
 |-  ( b = e -> ( E. c e. ( _Right ` A ) E. d e. U. ( R " _om ) b = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) <-> E. c e. ( _Right ` A ) E. d e. U. ( R " _om ) e = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) )
153 148 152 elab 
 |-  ( e e. { b | E. c e. ( _Right ` A ) E. d e. U. ( R " _om ) b = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) } <-> E. c e. ( _Right ` A ) E. d e. U. ( R " _om ) e = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) )
154 151 153 orbi12i 
 |-  ( ( e e. { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s
155 147 154 bitri 
 |-  ( e e. ( { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s
156 elun 
 |-  ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( c e. { 0s } \/ c e. { x e. ( _Left ` A ) | 0s
157 velsn 
 |-  ( c e. { 0s } <-> c = 0s )
158 157 orbi1i 
 |-  ( ( c e. { 0s } \/ c e. { x e. ( _Left ` A ) | 0s  ( c = 0s \/ c e. { x e. ( _Left ` A ) | 0s
159 156 158 bitri 
 |-  ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( c = 0s \/ c e. { x e. ( _Left ` A ) | 0s
160 58 adantr 
 |-  ( ( ph /\ d e. U. ( L " _om ) ) -> ( 0s x.s Y ) = 0s )
161 160 oveq1d 
 |-  ( ( ph /\ d e. U. ( L " _om ) ) -> ( ( 0s x.s Y ) +s ( A x.s d ) ) = ( 0s +s ( A x.s d ) ) )
162 muls02 
 |-  ( d e. No -> ( 0s x.s d ) = 0s )
163 115 162 syl 
 |-  ( ( ph /\ d e. U. ( L " _om ) ) -> ( 0s x.s d ) = 0s )
164 161 163 oveq12d 
 |-  ( ( ph /\ d e. U. ( L " _om ) ) -> ( ( ( 0s x.s Y ) +s ( A x.s d ) ) -s ( 0s x.s d ) ) = ( ( 0s +s ( A x.s d ) ) -s 0s ) )
165 4 adantr 
 |-  ( ( ph /\ d e. U. ( L " _om ) ) -> A e. No )
166 165 115 mulscld 
 |-  ( ( ph /\ d e. U. ( L " _om ) ) -> ( A x.s d ) e. No )
167 addslid 
 |-  ( ( A x.s d ) e. No -> ( 0s +s ( A x.s d ) ) = ( A x.s d ) )
168 166 167 syl 
 |-  ( ( ph /\ d e. U. ( L " _om ) ) -> ( 0s +s ( A x.s d ) ) = ( A x.s d ) )
169 168 oveq1d 
 |-  ( ( ph /\ d e. U. ( L " _om ) ) -> ( ( 0s +s ( A x.s d ) ) -s 0s ) = ( ( A x.s d ) -s 0s ) )
170 subsid1 
 |-  ( ( A x.s d ) e. No -> ( ( A x.s d ) -s 0s ) = ( A x.s d ) )
171 166 170 syl 
 |-  ( ( ph /\ d e. U. ( L " _om ) ) -> ( ( A x.s d ) -s 0s ) = ( A x.s d ) )
172 164 169 171 3eqtrd 
 |-  ( ( ph /\ d e. U. ( L " _om ) ) -> ( ( ( 0s x.s Y ) +s ( A x.s d ) ) -s ( 0s x.s d ) ) = ( A x.s d ) )
173 eliun 
 |-  ( d e. U_ i e. _om ( L ` i ) <-> E. i e. _om d e. ( L ` i ) )
174 funiunfv 
 |-  ( Fun L -> U_ i e. _om ( L ` i ) = U. ( L " _om ) )
175 43 174 ax-mp 
 |-  U_ i e. _om ( L ` i ) = U. ( L " _om )
176 175 eleq2i 
 |-  ( d e. U_ i e. _om ( L ` i ) <-> d e. U. ( L " _om ) )
177 173 176 bitr3i 
 |-  ( E. i e. _om d e. ( L ` i ) <-> d e. U. ( L " _om ) )
178 1 2 3 4 5 6 precsexlem9 
 |-  ( ( ph /\ i e. _om ) -> ( A. d e. ( L ` i ) ( A x.s d )
179 178 simpld 
 |-  ( ( ph /\ i e. _om ) -> A. d e. ( L ` i ) ( A x.s d )
180 rsp 
 |-  ( A. d e. ( L ` i ) ( A x.s d )  ( d e. ( L ` i ) -> ( A x.s d )
181 179 180 syl 
 |-  ( ( ph /\ i e. _om ) -> ( d e. ( L ` i ) -> ( A x.s d )
182 181 rexlimdva 
 |-  ( ph -> ( E. i e. _om d e. ( L ` i ) -> ( A x.s d )
183 177 182 biimtrrid 
 |-  ( ph -> ( d e. U. ( L " _om ) -> ( A x.s d )
184 183 imp 
 |-  ( ( ph /\ d e. U. ( L " _om ) ) -> ( A x.s d )
185 172 184 eqbrtrd 
 |-  ( ( ph /\ d e. U. ( L " _om ) ) -> ( ( ( 0s x.s Y ) +s ( A x.s d ) ) -s ( 0s x.s d ) )
186 185 ex 
 |-  ( ph -> ( d e. U. ( L " _om ) -> ( ( ( 0s x.s Y ) +s ( A x.s d ) ) -s ( 0s x.s d ) )
187 67 breq1d 
 |-  ( c = 0s -> ( ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) )  ( ( ( 0s x.s Y ) +s ( A x.s d ) ) -s ( 0s x.s d ) )
188 187 imbi2d 
 |-  ( c = 0s -> ( ( d e. U. ( L " _om ) -> ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) )  ( d e. U. ( L " _om ) -> ( ( ( 0s x.s Y ) +s ( A x.s d ) ) -s ( 0s x.s d ) )
189 186 188 syl5ibrcom 
 |-  ( ph -> ( c = 0s -> ( d e. U. ( L " _om ) -> ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) )
190 scutcut 
 |-  ( U. ( L " _om ) < ( ( U. ( L " _om ) |s U. ( R " _om ) ) e. No /\ U. ( L " _om ) <
191 16 190 syl 
 |-  ( ph -> ( ( U. ( L " _om ) |s U. ( R " _om ) ) e. No /\ U. ( L " _om ) <
192 191 simp3d 
 |-  ( ph -> { ( U. ( L " _om ) |s U. ( R " _om ) ) } <
193 192 adantr 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  { ( U. ( L " _om ) |s U. ( R " _om ) ) } <
194 ovex 
 |-  ( U. ( L " _om ) |s U. ( R " _om ) ) e. _V
195 194 snid 
 |-  ( U. ( L " _om ) |s U. ( R " _om ) ) e. { ( U. ( L " _om ) |s U. ( R " _om ) ) }
196 7 195 eqeltri 
 |-  Y e. { ( U. ( L " _om ) |s U. ( R " _om ) ) }
197 196 a1i 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  Y e. { ( U. ( L " _om ) |s U. ( R " _om ) ) } )
198 peano2 
 |-  ( i e. _om -> suc i e. _om )
199 198 ad2antrl 
 |-  ( ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s  suc i e. _om )
200 eqid 
 |-  ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c )
201 oveq1 
 |-  ( xL = c -> ( xL -s A ) = ( c -s A ) )
202 201 oveq1d 
 |-  ( xL = c -> ( ( xL -s A ) x.s yL ) = ( ( c -s A ) x.s yL ) )
203 202 oveq2d 
 |-  ( xL = c -> ( 1s +s ( ( xL -s A ) x.s yL ) ) = ( 1s +s ( ( c -s A ) x.s yL ) ) )
204 id 
 |-  ( xL = c -> xL = c )
205 203 204 oveq12d 
 |-  ( xL = c -> ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) = ( ( 1s +s ( ( c -s A ) x.s yL ) ) /su c ) )
206 205 eqeq2d 
 |-  ( xL = c -> ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s yL ) ) /su c ) ) )
207 oveq2 
 |-  ( yL = d -> ( ( c -s A ) x.s yL ) = ( ( c -s A ) x.s d ) )
208 207 oveq2d 
 |-  ( yL = d -> ( 1s +s ( ( c -s A ) x.s yL ) ) = ( 1s +s ( ( c -s A ) x.s d ) ) )
209 208 oveq1d 
 |-  ( yL = d -> ( ( 1s +s ( ( c -s A ) x.s yL ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) )
210 209 eqeq2d 
 |-  ( yL = d -> ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s yL ) ) /su c ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) ) )
211 206 210 rspc2ev 
 |-  ( ( c e. { x e. ( _Left ` A ) | 0s  E. xL e. { x e. ( _Left ` A ) | 0s
212 200 211 mp3an3 
 |-  ( ( c e. { x e. ( _Left ` A ) | 0s  E. xL e. { x e. ( _Left ` A ) | 0s
213 212 ad2ant2l 
 |-  ( ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s  E. xL e. { x e. ( _Left ` A ) | 0s
214 ovex 
 |-  ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. _V
215 eqeq1 
 |-  ( a = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) -> ( a = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) ) )
216 215 2rexbidv 
 |-  ( a = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) -> ( E. xL e. { x e. ( _Left ` A ) | 0s  E. xL e. { x e. ( _Left ` A ) | 0s
217 214 216 elab 
 |-  ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. { a | E. xL e. { x e. ( _Left ` A ) | 0s  E. xL e. { x e. ( _Left ` A ) | 0s
218 213 217 sylibr 
 |-  ( ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s  ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. { a | E. xL e. { x e. ( _Left ` A ) | 0s
219 elun1 
 |-  ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. { a | E. xL e. { x e. ( _Left ` A ) | 0s  ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
220 elun2 
 |-  ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s  ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( ( R ` i ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
221 218 219 220 3syl 
 |-  ( ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s  ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( ( R ` i ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
222 1 2 3 precsexlem5 
 |-  ( i e. _om -> ( R ` suc i ) = ( ( R ` i ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
223 222 ad2antrl 
 |-  ( ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s  ( R ` suc i ) = ( ( R ` i ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
224 221 223 eleqtrrd 
 |-  ( ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s  ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( R ` suc i ) )
225 fveq2 
 |-  ( j = suc i -> ( R ` j ) = ( R ` suc i ) )
226 225 eleq2d 
 |-  ( j = suc i -> ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( R ` j ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( R ` suc i ) ) )
227 226 rspcev 
 |-  ( ( suc i e. _om /\ ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( R ` suc i ) ) -> E. j e. _om ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( R ` j ) )
228 199 224 227 syl2anc 
 |-  ( ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s  E. j e. _om ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( R ` j ) )
229 228 rexlimdvaa 
 |-  ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s  ( E. i e. _om d e. ( L ` i ) -> E. j e. _om ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( R ` j ) ) )
230 eliun 
 |-  ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. U_ j e. _om ( R ` j ) <-> E. j e. _om ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( R ` j ) )
231 fo2nd 
 |-  2nd : _V -onto-> _V
232 fofun 
 |-  ( 2nd : _V -onto-> _V -> Fun 2nd )
233 231 232 ax-mp 
 |-  Fun 2nd
234 funco 
 |-  ( ( Fun 2nd /\ Fun F ) -> Fun ( 2nd o. F ) )
235 233 39 234 mp2an 
 |-  Fun ( 2nd o. F )
236 3 funeqi 
 |-  ( Fun R <-> Fun ( 2nd o. F ) )
237 235 236 mpbir 
 |-  Fun R
238 funiunfv 
 |-  ( Fun R -> U_ j e. _om ( R ` j ) = U. ( R " _om ) )
239 237 238 ax-mp 
 |-  U_ j e. _om ( R ` j ) = U. ( R " _om )
240 239 eleq2i 
 |-  ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. U_ j e. _om ( R ` j ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. U. ( R " _om ) )
241 230 240 bitr3i 
 |-  ( E. j e. _om ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( R ` j ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. U. ( R " _om ) )
242 229 177 241 3imtr3g 
 |-  ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s  ( d e. U. ( L " _om ) -> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. U. ( R " _om ) ) )
243 242 impr 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. U. ( R " _om ) )
244 193 197 243 ssltsepcd 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  Y
245 56 adantr 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  Y e. No )
246 144 a1i 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  1s e. No )
247 leftssno 
 |-  ( _Left ` A ) C_ No
248 11 247 sstri 
 |-  { x e. ( _Left ` A ) | 0s
249 248 sseli 
 |-  ( c e. { x e. ( _Left ` A ) | 0s  c e. No )
250 249 adantl 
 |-  ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s  c e. No )
251 4 adantr 
 |-  ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s  A e. No )
252 250 251 subscld 
 |-  ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s  ( c -s A ) e. No )
253 252 adantrr 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( c -s A ) e. No )
254 115 adantrl 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  d e. No )
255 253 254 mulscld 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( ( c -s A ) x.s d ) e. No )
256 246 255 addscld 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( 1s +s ( ( c -s A ) x.s d ) ) e. No )
257 249 ad2antrl 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  c e. No )
258 breq2 
 |-  ( x = c -> ( 0s  0s
259 258 elrab 
 |-  ( c e. { x e. ( _Left ` A ) | 0s  ( c e. ( _Left ` A ) /\ 0s
260 259 simprbi 
 |-  ( c e. { x e. ( _Left ` A ) | 0s  0s
261 260 ad2antrl 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  0s
262 260 adantl 
 |-  ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s  0s
263 breq2 
 |-  ( xO = c -> ( 0s  0s
264 oveq1 
 |-  ( xO = c -> ( xO x.s y ) = ( c x.s y ) )
265 264 eqeq1d 
 |-  ( xO = c -> ( ( xO x.s y ) = 1s <-> ( c x.s y ) = 1s ) )
266 265 rexbidv 
 |-  ( xO = c -> ( E. y e. No ( xO x.s y ) = 1s <-> E. y e. No ( c x.s y ) = 1s ) )
267 263 266 imbi12d 
 |-  ( xO = c -> ( ( 0s  E. y e. No ( xO x.s y ) = 1s ) <-> ( 0s  E. y e. No ( c x.s y ) = 1s ) ) )
268 6 adantr 
 |-  ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s  A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s  E. y e. No ( xO x.s y ) = 1s ) )
269 ssun1 
 |-  ( _Left ` A ) C_ ( ( _Left ` A ) u. ( _Right ` A ) )
270 11 269 sstri 
 |-  { x e. ( _Left ` A ) | 0s
271 270 sseli 
 |-  ( c e. { x e. ( _Left ` A ) | 0s  c e. ( ( _Left ` A ) u. ( _Right ` A ) ) )
272 271 adantl 
 |-  ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s  c e. ( ( _Left ` A ) u. ( _Right ` A ) ) )
273 267 268 272 rspcdva 
 |-  ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s  ( 0s  E. y e. No ( c x.s y ) = 1s ) )
274 262 273 mpd 
 |-  ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s  E. y e. No ( c x.s y ) = 1s )
275 274 adantrr 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  E. y e. No ( c x.s y ) = 1s )
276 245 256 257 261 275 sltmuldiv2wd 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( ( c x.s Y )  Y
277 244 276 mpbird 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( c x.s Y )
278 257 254 mulscld 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( c x.s d ) e. No )
279 166 adantrl 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( A x.s d ) e. No )
280 246 278 279 addsubsassd 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( ( 1s +s ( c x.s d ) ) -s ( A x.s d ) ) = ( 1s +s ( ( c x.s d ) -s ( A x.s d ) ) ) )
281 4 adantr 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  A e. No )
282 257 281 254 subsdird 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( ( c -s A ) x.s d ) = ( ( c x.s d ) -s ( A x.s d ) ) )
283 282 oveq2d 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( 1s +s ( ( c -s A ) x.s d ) ) = ( 1s +s ( ( c x.s d ) -s ( A x.s d ) ) ) )
284 280 283 eqtr4d 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( ( 1s +s ( c x.s d ) ) -s ( A x.s d ) ) = ( 1s +s ( ( c -s A ) x.s d ) ) )
285 277 284 breqtrrd 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( c x.s Y )
286 56 adantr 
 |-  ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s  Y e. No )
287 250 286 mulscld 
 |-  ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s  ( c x.s Y ) e. No )
288 287 adantrr 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( c x.s Y ) e. No )
289 288 279 addscld 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( ( c x.s Y ) +s ( A x.s d ) ) e. No )
290 289 278 246 sltsubaddd 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) )  ( ( c x.s Y ) +s ( A x.s d ) )
291 246 278 addscld 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( 1s +s ( c x.s d ) ) e. No )
292 288 279 291 sltaddsubd 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( ( ( c x.s Y ) +s ( A x.s d ) )  ( c x.s Y )
293 290 292 bitrd 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) )  ( c x.s Y )
294 285 293 mpbird 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) )
295 294 exp32 
 |-  ( ph -> ( c e. { x e. ( _Left ` A ) | 0s  ( d e. U. ( L " _om ) -> ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) )
296 189 295 jaod 
 |-  ( ph -> ( ( c = 0s \/ c e. { x e. ( _Left ` A ) | 0s  ( d e. U. ( L " _om ) -> ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) )
297 159 296 biimtrid 
 |-  ( ph -> ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( d e. U. ( L " _om ) -> ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) )
298 297 imp32 
 |-  ( ( ph /\ ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) )
299 breq1 
 |-  ( e = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) -> ( e  ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) )
300 298 299 syl5ibrcom 
 |-  ( ( ph /\ ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( e = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) -> e
301 300 rexlimdvva 
 |-  ( ph -> ( E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  e
302 192 adantr 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> { ( U. ( L " _om ) |s U. ( R " _om ) ) } <
303 196 a1i 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> Y e. { ( U. ( L " _om ) |s U. ( R " _om ) ) } )
304 198 ad2antrl 
 |-  ( ( ( ph /\ c e. ( _Right ` A ) ) /\ ( i e. _om /\ d e. ( R ` i ) ) ) -> suc i e. _om )
305 oveq1 
 |-  ( xR = c -> ( xR -s A ) = ( c -s A ) )
306 305 oveq1d 
 |-  ( xR = c -> ( ( xR -s A ) x.s yR ) = ( ( c -s A ) x.s yR ) )
307 306 oveq2d 
 |-  ( xR = c -> ( 1s +s ( ( xR -s A ) x.s yR ) ) = ( 1s +s ( ( c -s A ) x.s yR ) ) )
308 id 
 |-  ( xR = c -> xR = c )
309 307 308 oveq12d 
 |-  ( xR = c -> ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) = ( ( 1s +s ( ( c -s A ) x.s yR ) ) /su c ) )
310 309 eqeq2d 
 |-  ( xR = c -> ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s yR ) ) /su c ) ) )
311 oveq2 
 |-  ( yR = d -> ( ( c -s A ) x.s yR ) = ( ( c -s A ) x.s d ) )
312 311 oveq2d 
 |-  ( yR = d -> ( 1s +s ( ( c -s A ) x.s yR ) ) = ( 1s +s ( ( c -s A ) x.s d ) ) )
313 312 oveq1d 
 |-  ( yR = d -> ( ( 1s +s ( ( c -s A ) x.s yR ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) )
314 313 eqeq2d 
 |-  ( yR = d -> ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s yR ) ) /su c ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) ) )
315 310 314 rspc2ev 
 |-  ( ( c e. ( _Right ` A ) /\ d e. ( R ` i ) /\ ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) ) -> E. xR e. ( _Right ` A ) E. yR e. ( R ` i ) ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) )
316 200 315 mp3an3 
 |-  ( ( c e. ( _Right ` A ) /\ d e. ( R ` i ) ) -> E. xR e. ( _Right ` A ) E. yR e. ( R ` i ) ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) )
317 316 ad2ant2l 
 |-  ( ( ( ph /\ c e. ( _Right ` A ) ) /\ ( i e. _om /\ d e. ( R ` i ) ) ) -> E. xR e. ( _Right ` A ) E. yR e. ( R ` i ) ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) )
318 eqeq1 
 |-  ( a = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) -> ( a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) )
319 318 2rexbidv 
 |-  ( a = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) -> ( E. xR e. ( _Right ` A ) E. yR e. ( R ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> E. xR e. ( _Right ` A ) E. yR e. ( R ` i ) ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) )
320 214 319 elab 
 |-  ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. { a | E. xR e. ( _Right ` A ) E. yR e. ( R ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) } <-> E. xR e. ( _Right ` A ) E. yR e. ( R ` i ) ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) )
321 317 320 sylibr 
 |-  ( ( ( ph /\ c e. ( _Right ` A ) ) /\ ( i e. _om /\ d e. ( R ` i ) ) ) -> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. { a | E. xR e. ( _Right ` A ) E. yR e. ( R ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) } )
322 elun2 
 |-  ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. { a | E. xR e. ( _Right ` A ) E. yR e. ( R ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) } -> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
323 321 322 220 3syl 
 |-  ( ( ( ph /\ c e. ( _Right ` A ) ) /\ ( i e. _om /\ d e. ( R ` i ) ) ) -> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( ( R ` i ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
324 222 ad2antrl 
 |-  ( ( ( ph /\ c e. ( _Right ` A ) ) /\ ( i e. _om /\ d e. ( R ` i ) ) ) -> ( R ` suc i ) = ( ( R ` i ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
325 323 324 eleqtrrd 
 |-  ( ( ( ph /\ c e. ( _Right ` A ) ) /\ ( i e. _om /\ d e. ( R ` i ) ) ) -> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( R ` suc i ) )
326 304 325 227 syl2anc 
 |-  ( ( ( ph /\ c e. ( _Right ` A ) ) /\ ( i e. _om /\ d e. ( R ` i ) ) ) -> E. j e. _om ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( R ` j ) )
327 326 rexlimdvaa 
 |-  ( ( ph /\ c e. ( _Right ` A ) ) -> ( E. i e. _om d e. ( R ` i ) -> E. j e. _om ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( R ` j ) ) )
328 eliun 
 |-  ( d e. U_ i e. _om ( R ` i ) <-> E. i e. _om d e. ( R ` i ) )
329 funiunfv 
 |-  ( Fun R -> U_ i e. _om ( R ` i ) = U. ( R " _om ) )
330 237 329 ax-mp 
 |-  U_ i e. _om ( R ` i ) = U. ( R " _om )
331 330 eleq2i 
 |-  ( d e. U_ i e. _om ( R ` i ) <-> d e. U. ( R " _om ) )
332 328 331 bitr3i 
 |-  ( E. i e. _om d e. ( R ` i ) <-> d e. U. ( R " _om ) )
333 327 332 241 3imtr3g 
 |-  ( ( ph /\ c e. ( _Right ` A ) ) -> ( d e. U. ( R " _om ) -> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. U. ( R " _om ) ) )
334 333 impr 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. U. ( R " _om ) )
335 302 303 334 ssltsepcd 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> Y
336 144 a1i 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> 1s e. No )
337 4 adantr 
 |-  ( ( ph /\ c e. ( _Right ` A ) ) -> A e. No )
338 127 337 subscld 
 |-  ( ( ph /\ c e. ( _Right ` A ) ) -> ( c -s A ) e. No )
339 338 adantrr 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> ( c -s A ) e. No )
340 339 135 mulscld 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> ( ( c -s A ) x.s d ) e. No )
341 336 340 addscld 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> ( 1s +s ( ( c -s A ) x.s d ) ) e. No )
342 20 a1i 
 |-  ( ( ph /\ c e. ( _Right ` A ) ) -> 0s e. No )
343 5 adantr 
 |-  ( ( ph /\ c e. ( _Right ` A ) ) -> 0s
344 breq2 
 |-  ( xO = c -> ( A  A
345 rightval 
 |-  ( _Right ` A ) = { xO e. ( _Old ` ( bday ` A ) ) | A
346 344 345 elrab2 
 |-  ( c e. ( _Right ` A ) <-> ( c e. ( _Old ` ( bday ` A ) ) /\ A
347 346 simprbi 
 |-  ( c e. ( _Right ` A ) -> A
348 347 adantl 
 |-  ( ( ph /\ c e. ( _Right ` A ) ) -> A
349 342 337 127 343 348 slttrd 
 |-  ( ( ph /\ c e. ( _Right ` A ) ) -> 0s
350 349 adantrr 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> 0s
351 6 adantr 
 |-  ( ( ph /\ c e. ( _Right ` A ) ) -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s  E. y e. No ( xO x.s y ) = 1s ) )
352 elun2 
 |-  ( c e. ( _Right ` A ) -> c e. ( ( _Left ` A ) u. ( _Right ` A ) ) )
353 352 adantl 
 |-  ( ( ph /\ c e. ( _Right ` A ) ) -> c e. ( ( _Left ` A ) u. ( _Right ` A ) ) )
354 267 351 353 rspcdva 
 |-  ( ( ph /\ c e. ( _Right ` A ) ) -> ( 0s  E. y e. No ( c x.s y ) = 1s ) )
355 349 354 mpd 
 |-  ( ( ph /\ c e. ( _Right ` A ) ) -> E. y e. No ( c x.s y ) = 1s )
356 355 adantrr 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> E. y e. No ( c x.s y ) = 1s )
357 129 341 128 350 356 sltmuldiv2wd 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> ( ( c x.s Y )  Y
358 335 357 mpbird 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> ( c x.s Y )
359 336 138 136 addsubsassd 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> ( ( 1s +s ( c x.s d ) ) -s ( A x.s d ) ) = ( 1s +s ( ( c x.s d ) -s ( A x.s d ) ) ) )
360 128 131 135 subsdird 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> ( ( c -s A ) x.s d ) = ( ( c x.s d ) -s ( A x.s d ) ) )
361 360 oveq2d 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> ( 1s +s ( ( c -s A ) x.s d ) ) = ( 1s +s ( ( c x.s d ) -s ( A x.s d ) ) ) )
362 359 361 eqtr4d 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> ( ( 1s +s ( c x.s d ) ) -s ( A x.s d ) ) = ( 1s +s ( ( c -s A ) x.s d ) ) )
363 358 362 breqtrrd 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> ( c x.s Y )
364 137 138 336 sltsubaddd 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> ( ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) )  ( ( c x.s Y ) +s ( A x.s d ) )
365 336 138 addscld 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> ( 1s +s ( c x.s d ) ) e. No )
366 130 136 365 sltaddsubd 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> ( ( ( c x.s Y ) +s ( A x.s d ) )  ( c x.s Y )
367 364 366 bitrd 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> ( ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) )  ( c x.s Y )
368 363 367 mpbird 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) )
369 368 299 syl5ibrcom 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( R " _om ) ) ) -> ( e = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) -> e
370 369 rexlimdvva 
 |-  ( ph -> ( E. c e. ( _Right ` A ) E. d e. U. ( R " _om ) e = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) -> e
371 301 370 jaod 
 |-  ( ph -> ( ( E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  e
372 155 371 biimtrid 
 |-  ( ph -> ( e e. ( { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  e
373 372 imp 
 |-  ( ( ph /\ e e. ( { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  e
374 velsn 
 |-  ( f e. { 1s } <-> f = 1s )
375 breq2 
 |-  ( f = 1s -> ( e  e
376 374 375 sylbi 
 |-  ( f e. { 1s } -> ( e  e
377 373 376 syl5ibrcom 
 |-  ( ( ph /\ e e. ( { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( f e. { 1s } -> e
378 377 3impia 
 |-  ( ( ph /\ e e. ( { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  e
379 103 105 143 146 378 ssltd 
 |-  ( ph -> ( { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s
380 eqid 
 |-  ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) = ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) )
381 380 rnmpo 
 |-  ran ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) = { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s
382 mpoexga 
 |-  ( ( ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) e. _V )
383 85 97 382 syl2anc 
 |-  ( ph -> ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) e. _V )
384 rnexg 
 |-  ( ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) e. _V -> ran ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) e. _V )
385 383 384 syl 
 |-  ( ph -> ran ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) e. _V )
386 381 385 eqeltrrid 
 |-  ( ph -> { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s
387 eqid 
 |-  ( c e. ( _Right ` A ) , d e. U. ( L " _om ) |-> ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) = ( c e. ( _Right ` A ) , d e. U. ( L " _om ) |-> ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) )
388 387 rnmpo 
 |-  ran ( c e. ( _Right ` A ) , d e. U. ( L " _om ) |-> ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) = { b | E. c e. ( _Right ` A ) E. d e. U. ( L " _om ) b = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) }
389 mpoexga 
 |-  ( ( ( _Right ` A ) e. _V /\ U. ( L " _om ) e. _V ) -> ( c e. ( _Right ` A ) , d e. U. ( L " _om ) |-> ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) e. _V )
390 95 87 389 sylancr 
 |-  ( ph -> ( c e. ( _Right ` A ) , d e. U. ( L " _om ) |-> ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) e. _V )
391 rnexg 
 |-  ( ( c e. ( _Right ` A ) , d e. U. ( L " _om ) |-> ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) e. _V -> ran ( c e. ( _Right ` A ) , d e. U. ( L " _om ) |-> ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) e. _V )
392 390 391 syl 
 |-  ( ph -> ran ( c e. ( _Right ` A ) , d e. U. ( L " _om ) |-> ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) e. _V )
393 388 392 eqeltrrid 
 |-  ( ph -> { b | E. c e. ( _Right ` A ) E. d e. U. ( L " _om ) b = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) } e. _V )
394 386 393 unexd 
 |-  ( ph -> ( { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s
395 108 adantrr 
 |-  ( ( ph /\ ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  c e. No )
396 56 adantr 
 |-  ( ( ph /\ ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  Y e. No )
397 395 396 mulscld 
 |-  ( ( ph /\ ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( c x.s Y ) e. No )
398 4 adantr 
 |-  ( ( ph /\ ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  A e. No )
399 134 adantrl 
 |-  ( ( ph /\ ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  d e. No )
400 398 399 mulscld 
 |-  ( ( ph /\ ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( A x.s d ) e. No )
401 397 400 addscld 
 |-  ( ( ph /\ ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( ( c x.s Y ) +s ( A x.s d ) ) e. No )
402 395 399 mulscld 
 |-  ( ( ph /\ ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( c x.s d ) e. No )
403 401 402 subscld 
 |-  ( ( ph /\ ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) e. No )
404 403 121 syl5ibrcom 
 |-  ( ( ph /\ ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( b = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) -> b e. No ) )
405 404 rexlimdvva 
 |-  ( ph -> ( E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  b e. No ) )
406 405 abssdv 
 |-  ( ph -> { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s
407 127 adantrr 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> c e. No )
408 56 adantr 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> Y e. No )
409 407 408 mulscld 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> ( c x.s Y ) e. No )
410 4 adantr 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> A e. No )
411 115 adantrl 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> d e. No )
412 410 411 mulscld 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> ( A x.s d ) e. No )
413 409 412 addscld 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> ( ( c x.s Y ) +s ( A x.s d ) ) e. No )
414 407 411 mulscld 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> ( c x.s d ) e. No )
415 413 414 subscld 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) e. No )
416 415 121 syl5ibrcom 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> ( b = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) -> b e. No ) )
417 416 rexlimdvva 
 |-  ( ph -> ( E. c e. ( _Right ` A ) E. d e. U. ( L " _om ) b = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) -> b e. No ) )
418 417 abssdv 
 |-  ( ph -> { b | E. c e. ( _Right ` A ) E. d e. U. ( L " _om ) b = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) } C_ No )
419 406 418 unssd 
 |-  ( ph -> ( { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s
420 elun 
 |-  ( f e. ( { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( f e. { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s
421 vex 
 |-  f e. _V
422 eqeq1 
 |-  ( b = f -> ( b = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) <-> f = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) )
423 422 2rexbidv 
 |-  ( b = f -> ( E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s
424 421 423 elab 
 |-  ( f e. { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s
425 422 2rexbidv 
 |-  ( b = f -> ( E. c e. ( _Right ` A ) E. d e. U. ( L " _om ) b = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) <-> E. c e. ( _Right ` A ) E. d e. U. ( L " _om ) f = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) ) )
426 421 425 elab 
 |-  ( f e. { b | E. c e. ( _Right ` A ) E. d e. U. ( L " _om ) b = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) } <-> E. c e. ( _Right ` A ) E. d e. U. ( L " _om ) f = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) )
427 424 426 orbi12i 
 |-  ( ( f e. { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s
428 420 427 bitri 
 |-  ( f e. ( { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s
429 eliun 
 |-  ( d e. U_ j e. _om ( R ` j ) <-> E. j e. _om d e. ( R ` j ) )
430 239 eleq2i 
 |-  ( d e. U_ j e. _om ( R ` j ) <-> d e. U. ( R " _om ) )
431 429 430 bitr3i 
 |-  ( E. j e. _om d e. ( R ` j ) <-> d e. U. ( R " _om ) )
432 1 2 3 4 5 6 precsexlem9 
 |-  ( ( ph /\ j e. _om ) -> ( A. c e. ( L ` j ) ( A x.s c )
433 rsp 
 |-  ( A. d e. ( R ` j ) 1s  ( d e. ( R ` j ) -> 1s
434 432 433 simpl2im 
 |-  ( ( ph /\ j e. _om ) -> ( d e. ( R ` j ) -> 1s
435 434 rexlimdva 
 |-  ( ph -> ( E. j e. _om d e. ( R ` j ) -> 1s
436 431 435 biimtrrid 
 |-  ( ph -> ( d e. U. ( R " _om ) -> 1s
437 436 imp 
 |-  ( ( ph /\ d e. U. ( R " _om ) ) -> 1s
438 56 adantr 
 |-  ( ( ph /\ d e. U. ( R " _om ) ) -> Y e. No )
439 57 oveq1d 
 |-  ( Y e. No -> ( ( 0s x.s Y ) +s ( A x.s d ) ) = ( 0s +s ( A x.s d ) ) )
440 438 439 syl 
 |-  ( ( ph /\ d e. U. ( R " _om ) ) -> ( ( 0s x.s Y ) +s ( A x.s d ) ) = ( 0s +s ( A x.s d ) ) )
441 4 adantr 
 |-  ( ( ph /\ d e. U. ( R " _om ) ) -> A e. No )
442 441 134 mulscld 
 |-  ( ( ph /\ d e. U. ( R " _om ) ) -> ( A x.s d ) e. No )
443 442 167 syl 
 |-  ( ( ph /\ d e. U. ( R " _om ) ) -> ( 0s +s ( A x.s d ) ) = ( A x.s d ) )
444 440 443 eqtrd 
 |-  ( ( ph /\ d e. U. ( R " _om ) ) -> ( ( 0s x.s Y ) +s ( A x.s d ) ) = ( A x.s d ) )
445 134 162 syl 
 |-  ( ( ph /\ d e. U. ( R " _om ) ) -> ( 0s x.s d ) = 0s )
446 444 445 oveq12d 
 |-  ( ( ph /\ d e. U. ( R " _om ) ) -> ( ( ( 0s x.s Y ) +s ( A x.s d ) ) -s ( 0s x.s d ) ) = ( ( A x.s d ) -s 0s ) )
447 442 170 syl 
 |-  ( ( ph /\ d e. U. ( R " _om ) ) -> ( ( A x.s d ) -s 0s ) = ( A x.s d ) )
448 446 447 eqtrd 
 |-  ( ( ph /\ d e. U. ( R " _om ) ) -> ( ( ( 0s x.s Y ) +s ( A x.s d ) ) -s ( 0s x.s d ) ) = ( A x.s d ) )
449 437 448 breqtrrd 
 |-  ( ( ph /\ d e. U. ( R " _om ) ) -> 1s
450 449 ex 
 |-  ( ph -> ( d e. U. ( R " _om ) -> 1s
451 67 breq2d 
 |-  ( c = 0s -> ( 1s  1s
452 451 imbi2d 
 |-  ( c = 0s -> ( ( d e. U. ( R " _om ) -> 1s  ( d e. U. ( R " _om ) -> 1s
453 450 452 syl5ibrcom 
 |-  ( ph -> ( c = 0s -> ( d e. U. ( R " _om ) -> 1s
454 144 a1i 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  1s e. No )
455 249 ad2antrl 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  c e. No )
456 134 adantrl 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  d e. No )
457 455 456 mulscld 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( c x.s d ) e. No )
458 442 adantrl 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( A x.s d ) e. No )
459 454 457 458 addsubsassd 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( ( 1s +s ( c x.s d ) ) -s ( A x.s d ) ) = ( 1s +s ( ( c x.s d ) -s ( A x.s d ) ) ) )
460 4 adantr 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  A e. No )
461 455 460 456 subsdird 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( ( c -s A ) x.s d ) = ( ( c x.s d ) -s ( A x.s d ) ) )
462 461 oveq2d 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( 1s +s ( ( c -s A ) x.s d ) ) = ( 1s +s ( ( c x.s d ) -s ( A x.s d ) ) ) )
463 459 462 eqtr4d 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( ( 1s +s ( c x.s d ) ) -s ( A x.s d ) ) = ( 1s +s ( ( c -s A ) x.s d ) ) )
464 191 simp2d 
 |-  ( ph -> U. ( L " _om ) <
465 464 adantr 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  U. ( L " _om ) <
466 198 ad2antrl 
 |-  ( ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s  suc i e. _om )
467 201 oveq1d 
 |-  ( xL = c -> ( ( xL -s A ) x.s yR ) = ( ( c -s A ) x.s yR ) )
468 467 oveq2d 
 |-  ( xL = c -> ( 1s +s ( ( xL -s A ) x.s yR ) ) = ( 1s +s ( ( c -s A ) x.s yR ) ) )
469 468 204 oveq12d 
 |-  ( xL = c -> ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) = ( ( 1s +s ( ( c -s A ) x.s yR ) ) /su c ) )
470 469 eqeq2d 
 |-  ( xL = c -> ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s yR ) ) /su c ) ) )
471 470 314 rspc2ev 
 |-  ( ( c e. { x e. ( _Left ` A ) | 0s  E. xL e. { x e. ( _Left ` A ) | 0s
472 200 471 mp3an3 
 |-  ( ( c e. { x e. ( _Left ` A ) | 0s  E. xL e. { x e. ( _Left ` A ) | 0s
473 472 ad2ant2l 
 |-  ( ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s  E. xL e. { x e. ( _Left ` A ) | 0s
474 eqeq1 
 |-  ( a = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) -> ( a = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) ) )
475 474 2rexbidv 
 |-  ( a = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) -> ( E. xL e. { x e. ( _Left ` A ) | 0s  E. xL e. { x e. ( _Left ` A ) | 0s
476 214 475 elab 
 |-  ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. { a | E. xL e. { x e. ( _Left ` A ) | 0s  E. xL e. { x e. ( _Left ` A ) | 0s
477 473 476 sylibr 
 |-  ( ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s  ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. { a | E. xL e. { x e. ( _Left ` A ) | 0s
478 elun2 
 |-  ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. { a | E. xL e. { x e. ( _Left ` A ) | 0s  ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
479 elun2 
 |-  ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s  ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( ( L ` i ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
480 477 478 479 3syl 
 |-  ( ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s  ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( ( L ` i ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
481 1 2 3 precsexlem4 
 |-  ( i e. _om -> ( L ` suc i ) = ( ( L ` i ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
482 481 ad2antrl 
 |-  ( ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s  ( L ` suc i ) = ( ( L ` i ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
483 480 482 eleqtrrd 
 |-  ( ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s  ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( L ` suc i ) )
484 fveq2 
 |-  ( j = suc i -> ( L ` j ) = ( L ` suc i ) )
485 484 eleq2d 
 |-  ( j = suc i -> ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( L ` j ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( L ` suc i ) ) )
486 485 rspcev 
 |-  ( ( suc i e. _om /\ ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( L ` suc i ) ) -> E. j e. _om ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( L ` j ) )
487 466 483 486 syl2anc 
 |-  ( ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s  E. j e. _om ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( L ` j ) )
488 487 rexlimdvaa 
 |-  ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s  ( E. i e. _om d e. ( R ` i ) -> E. j e. _om ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( L ` j ) ) )
489 eliun 
 |-  ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. U_ j e. _om ( L ` j ) <-> E. j e. _om ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( L ` j ) )
490 funiunfv 
 |-  ( Fun L -> U_ j e. _om ( L ` j ) = U. ( L " _om ) )
491 43 490 ax-mp 
 |-  U_ j e. _om ( L ` j ) = U. ( L " _om )
492 491 eleq2i 
 |-  ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. U_ j e. _om ( L ` j ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. U. ( L " _om ) )
493 489 492 bitr3i 
 |-  ( E. j e. _om ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( L ` j ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. U. ( L " _om ) )
494 488 332 493 3imtr3g 
 |-  ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s  ( d e. U. ( R " _om ) -> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. U. ( L " _om ) ) )
495 494 impr 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. U. ( L " _om ) )
496 196 a1i 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  Y e. { ( U. ( L " _om ) |s U. ( R " _om ) ) } )
497 465 495 496 ssltsepcd 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c )
498 252 adantrr 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( c -s A ) e. No )
499 498 456 mulscld 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( ( c -s A ) x.s d ) e. No )
500 454 499 addscld 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( 1s +s ( ( c -s A ) x.s d ) ) e. No )
501 56 adantr 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  Y e. No )
502 260 ad2antrl 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  0s
503 274 adantrr 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  E. y e. No ( c x.s y ) = 1s )
504 500 501 455 502 503 sltdivmulwd 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c )  ( 1s +s ( ( c -s A ) x.s d ) )
505 497 504 mpbid 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( 1s +s ( ( c -s A ) x.s d ) )
506 463 505 eqbrtrd 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( ( 1s +s ( c x.s d ) ) -s ( A x.s d ) )
507 454 457 addscld 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( 1s +s ( c x.s d ) ) e. No )
508 287 adantrr 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( c x.s Y ) e. No )
509 507 458 508 sltsubaddd 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( ( ( 1s +s ( c x.s d ) ) -s ( A x.s d ) )  ( 1s +s ( c x.s d ) )
510 508 458 addscld 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( ( c x.s Y ) +s ( A x.s d ) ) e. No )
511 454 457 510 sltaddsubd 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( ( 1s +s ( c x.s d ) )  1s
512 509 511 bitrd 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  ( ( ( 1s +s ( c x.s d ) ) -s ( A x.s d ) )  1s
513 506 512 mpbid 
 |-  ( ( ph /\ ( c e. { x e. ( _Left ` A ) | 0s  1s
514 513 exp32 
 |-  ( ph -> ( c e. { x e. ( _Left ` A ) | 0s  ( d e. U. ( R " _om ) -> 1s
515 453 514 jaod 
 |-  ( ph -> ( ( c = 0s \/ c e. { x e. ( _Left ` A ) | 0s  ( d e. U. ( R " _om ) -> 1s
516 159 515 biimtrid 
 |-  ( ph -> ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( d e. U. ( R " _om ) -> 1s
517 516 imp32 
 |-  ( ( ph /\ ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  1s
518 breq2 
 |-  ( f = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) -> ( 1s  1s
519 517 518 syl5ibrcom 
 |-  ( ( ph /\ ( c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  ( f = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) -> 1s
520 519 rexlimdvva 
 |-  ( ph -> ( E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  1s
521 144 a1i 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> 1s e. No )
522 521 414 412 addsubsassd 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> ( ( 1s +s ( c x.s d ) ) -s ( A x.s d ) ) = ( 1s +s ( ( c x.s d ) -s ( A x.s d ) ) ) )
523 407 410 411 subsdird 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> ( ( c -s A ) x.s d ) = ( ( c x.s d ) -s ( A x.s d ) ) )
524 523 oveq2d 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> ( 1s +s ( ( c -s A ) x.s d ) ) = ( 1s +s ( ( c x.s d ) -s ( A x.s d ) ) ) )
525 522 524 eqtr4d 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> ( ( 1s +s ( c x.s d ) ) -s ( A x.s d ) ) = ( 1s +s ( ( c -s A ) x.s d ) ) )
526 464 adantr 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> U. ( L " _om ) <
527 198 ad2antrl 
 |-  ( ( ( ph /\ c e. ( _Right ` A ) ) /\ ( i e. _om /\ d e. ( L ` i ) ) ) -> suc i e. _om )
528 305 oveq1d 
 |-  ( xR = c -> ( ( xR -s A ) x.s yL ) = ( ( c -s A ) x.s yL ) )
529 528 oveq2d 
 |-  ( xR = c -> ( 1s +s ( ( xR -s A ) x.s yL ) ) = ( 1s +s ( ( c -s A ) x.s yL ) ) )
530 529 308 oveq12d 
 |-  ( xR = c -> ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) = ( ( 1s +s ( ( c -s A ) x.s yL ) ) /su c ) )
531 530 eqeq2d 
 |-  ( xR = c -> ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s yL ) ) /su c ) ) )
532 531 210 rspc2ev 
 |-  ( ( c e. ( _Right ` A ) /\ d e. ( L ` i ) /\ ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) ) -> E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) )
533 200 532 mp3an3 
 |-  ( ( c e. ( _Right ` A ) /\ d e. ( L ` i ) ) -> E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) )
534 533 ad2ant2l 
 |-  ( ( ( ph /\ c e. ( _Right ` A ) ) /\ ( i e. _om /\ d e. ( L ` i ) ) ) -> E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) )
535 eqeq1 
 |-  ( a = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) -> ( a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) )
536 535 2rexbidv 
 |-  ( a = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) -> ( E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) )
537 214 536 elab 
 |-  ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } <-> E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) )
538 534 537 sylibr 
 |-  ( ( ( ph /\ c e. ( _Right ` A ) ) /\ ( i e. _om /\ d e. ( L ` i ) ) ) -> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } )
539 elun1 
 |-  ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } -> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
540 538 539 479 3syl 
 |-  ( ( ( ph /\ c e. ( _Right ` A ) ) /\ ( i e. _om /\ d e. ( L ` i ) ) ) -> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( ( L ` i ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
541 481 ad2antrl 
 |-  ( ( ( ph /\ c e. ( _Right ` A ) ) /\ ( i e. _om /\ d e. ( L ` i ) ) ) -> ( L ` suc i ) = ( ( L ` i ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
542 540 541 eleqtrrd 
 |-  ( ( ( ph /\ c e. ( _Right ` A ) ) /\ ( i e. _om /\ d e. ( L ` i ) ) ) -> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( L ` suc i ) )
543 527 542 486 syl2anc 
 |-  ( ( ( ph /\ c e. ( _Right ` A ) ) /\ ( i e. _om /\ d e. ( L ` i ) ) ) -> E. j e. _om ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( L ` j ) )
544 543 rexlimdvaa 
 |-  ( ( ph /\ c e. ( _Right ` A ) ) -> ( E. i e. _om d e. ( L ` i ) -> E. j e. _om ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( L ` j ) ) )
545 544 177 493 3imtr3g 
 |-  ( ( ph /\ c e. ( _Right ` A ) ) -> ( d e. U. ( L " _om ) -> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. U. ( L " _om ) ) )
546 545 impr 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. U. ( L " _om ) )
547 196 a1i 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> Y e. { ( U. ( L " _om ) |s U. ( R " _om ) ) } )
548 526 546 547 ssltsepcd 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c )
549 338 adantrr 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> ( c -s A ) e. No )
550 549 411 mulscld 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> ( ( c -s A ) x.s d ) e. No )
551 521 550 addscld 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> ( 1s +s ( ( c -s A ) x.s d ) ) e. No )
552 349 adantrr 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> 0s
553 355 adantrr 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> E. y e. No ( c x.s y ) = 1s )
554 551 408 407 552 553 sltdivmulwd 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c )  ( 1s +s ( ( c -s A ) x.s d ) )
555 548 554 mpbid 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> ( 1s +s ( ( c -s A ) x.s d ) )
556 525 555 eqbrtrd 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> ( ( 1s +s ( c x.s d ) ) -s ( A x.s d ) )
557 521 414 addscld 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> ( 1s +s ( c x.s d ) ) e. No )
558 557 412 409 sltsubaddd 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> ( ( ( 1s +s ( c x.s d ) ) -s ( A x.s d ) )  ( 1s +s ( c x.s d ) )
559 521 414 413 sltaddsubd 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> ( ( 1s +s ( c x.s d ) )  1s
560 558 559 bitrd 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> ( ( ( 1s +s ( c x.s d ) ) -s ( A x.s d ) )  1s
561 556 560 mpbid 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> 1s
562 561 518 syl5ibrcom 
 |-  ( ( ph /\ ( c e. ( _Right ` A ) /\ d e. U. ( L " _om ) ) ) -> ( f = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) -> 1s
563 562 rexlimdvva 
 |-  ( ph -> ( E. c e. ( _Right ` A ) E. d e. U. ( L " _om ) f = ( ( ( c x.s Y ) +s ( A x.s d ) ) -s ( c x.s d ) ) -> 1s
564 520 563 jaod 
 |-  ( ph -> ( ( E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  1s
565 428 564 biimtrid 
 |-  ( ph -> ( f e. ( { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  1s
566 velsn 
 |-  ( e e. { 1s } <-> e = 1s )
567 breq1 
 |-  ( e = 1s -> ( e  1s
568 567 imbi2d 
 |-  ( e = 1s -> ( ( f e. ( { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  e  ( f e. ( { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  1s
569 566 568 sylbi 
 |-  ( e e. { 1s } -> ( ( f e. ( { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  e  ( f e. ( { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  1s
570 565 569 syl5ibrcom 
 |-  ( ph -> ( e e. { 1s } -> ( f e. ( { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  e
571 570 3imp 
 |-  ( ( ph /\ e e. { 1s } /\ f e. ( { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s  e
572 105 394 146 419 571 ssltd 
 |-  ( ph -> { 1s } <
573 81 379 572 cuteq1 
 |-  ( ph -> ( ( { b | E. c e. ( { 0s } u. { x e. ( _Left ` A ) | 0s
574 19 573 eqtrd 
 |-  ( ph -> ( A x.s Y ) = 1s )