Metamath Proof Explorer

Theorem naddwordnexlem4

Description: When A is the sum of a limit ordinal (or zero) and a natural number and B is the sum of a larger limit ordinal and a smaller natural number, there exists a product with omega such that the ordinal sum with A is less than or equal to B while the natural sum is larger than B . (Contributed by RP, 15-Feb-2025)

Ref Expression
Hypotheses naddwordnex.a 
|- ( ph -> A = ( ( _om .o C ) +o M ) )
naddwordnex.b 
|- ( ph -> B = ( ( _om .o D ) +o N ) )
naddwordnex.c 
|- ( ph -> C e. D )
naddwordnex.d 
|- ( ph -> D e. On )
naddwordnex.m 
|- ( ph -> M e. _om )
naddwordnex.n 
|- ( ph -> N e. M )
naddwordnexlem4.s 
|- S = { y e. On | D C_ ( C +o y ) }
Assertion naddwordnexlem4 
|- ( ph -> E. x e. ( On \ 1o ) ( ( C +o x ) = D /\ ( A +o ( _om .o x ) ) C_ B /\ B e. ( A +no ( _om .o x ) ) ) )

Proof

Step Hyp Ref Expression
1 naddwordnex.a 
 |-  ( ph -> A = ( ( _om .o C ) +o M ) )
2 naddwordnex.b 
 |-  ( ph -> B = ( ( _om .o D ) +o N ) )
3 naddwordnex.c 
 |-  ( ph -> C e. D )
4 naddwordnex.d 
 |-  ( ph -> D e. On )
5 naddwordnex.m 
 |-  ( ph -> M e. _om )
6 naddwordnex.n 
 |-  ( ph -> N e. M )
7 naddwordnexlem4.s 
 |-  S = { y e. On | D C_ ( C +o y ) }
8 7 ssrab3 
 |-  S C_ On
9 oveq2 
 |-  ( y = D -> ( C +o y ) = ( C +o D ) )
10 9 sseq2d 
 |-  ( y = D -> ( D C_ ( C +o y ) <-> D C_ ( C +o D ) ) )
11 onelon 
 |-  ( ( D e. On /\ C e. D ) -> C e. On )
12 4 3 11 syl2anc 
 |-  ( ph -> C e. On )
13 oaword2 
 |-  ( ( D e. On /\ C e. On ) -> D C_ ( C +o D ) )
14 4 12 13 syl2anc 
 |-  ( ph -> D C_ ( C +o D ) )
15 10 4 14 elrabd 
 |-  ( ph -> D e. { y e. On | D C_ ( C +o y ) } )
16 15 7 eleqtrrdi 
 |-  ( ph -> D e. S )
17 16 ne0d 
 |-  ( ph -> S =/= (/) )
18 oninton 
 |-  ( ( S C_ On /\ S =/= (/) ) -> |^| S e. On )
19 8 17 18 sylancr 
 |-  ( ph -> |^| S e. On )
20 oveq2 
 |-  ( y = (/) -> ( C +o y ) = ( C +o (/) ) )
21 oa0 
 |-  ( C e. On -> ( C +o (/) ) = C )
22 12 21 syl 
 |-  ( ph -> ( C +o (/) ) = C )
23 20 22 sylan9eqr 
 |-  ( ( ph /\ y = (/) ) -> ( C +o y ) = C )
24 3 adantr 
 |-  ( ( ph /\ y = (/) ) -> C e. D )
25 23 24 eqeltrd 
 |-  ( ( ph /\ y = (/) ) -> ( C +o y ) e. D )
26 25 ex 
 |-  ( ph -> ( y = (/) -> ( C +o y ) e. D ) )
27 26 adantr 
 |-  ( ( ph /\ y e. On ) -> ( y = (/) -> ( C +o y ) e. D ) )
28 27 con3d 
 |-  ( ( ph /\ y e. On ) -> ( -. ( C +o y ) e. D -> -. y = (/) ) )
29 oacl 
 |-  ( ( C e. On /\ y e. On ) -> ( C +o y ) e. On )
30 12 29 sylan 
 |-  ( ( ph /\ y e. On ) -> ( C +o y ) e. On )
31 ontri1 
 |-  ( ( D e. On /\ ( C +o y ) e. On ) -> ( D C_ ( C +o y ) <-> -. ( C +o y ) e. D ) )
32 4 30 31 syl2an2r 
 |-  ( ( ph /\ y e. On ) -> ( D C_ ( C +o y ) <-> -. ( C +o y ) e. D ) )
33 on0eln0 
 |-  ( y e. On -> ( (/) e. y <-> y =/= (/) ) )
34 df-ne 
 |-  ( y =/= (/) <-> -. y = (/) )
35 33 34 bitrdi 
 |-  ( y e. On -> ( (/) e. y <-> -. y = (/) ) )
36 35 adantl 
 |-  ( ( ph /\ y e. On ) -> ( (/) e. y <-> -. y = (/) ) )
37 28 32 36 3imtr4d 
 |-  ( ( ph /\ y e. On ) -> ( D C_ ( C +o y ) -> (/) e. y ) )
38 37 ex 
 |-  ( ph -> ( y e. On -> ( D C_ ( C +o y ) -> (/) e. y ) ) )
39 38 ralrimiv 
 |-  ( ph -> A. y e. On ( D C_ ( C +o y ) -> (/) e. y ) )
40 0ex 
 |-  (/) e. _V
41 40 elintrab 
 |-  ( (/) e. |^| { y e. On | D C_ ( C +o y ) } <-> A. y e. On ( D C_ ( C +o y ) -> (/) e. y ) )
42 39 41 sylibr 
 |-  ( ph -> (/) e. |^| { y e. On | D C_ ( C +o y ) } )
43 7 inteqi 
 |-  |^| S = |^| { y e. On | D C_ ( C +o y ) }
44 42 43 eleqtrrdi 
 |-  ( ph -> (/) e. |^| S )
45 ondif1 
 |-  ( |^| S e. ( On \ 1o ) <-> ( |^| S e. On /\ (/) e. |^| S ) )
46 19 44 45 sylanbrc 
 |-  ( ph -> |^| S e. ( On \ 1o ) )
47 onzsl 
 |-  ( |^| S e. On <-> ( |^| S = (/) \/ E. z e. On |^| S = suc z \/ ( |^| S e. _V /\ Lim |^| S ) ) )
48 19 47 sylib 
 |-  ( ph -> ( |^| S = (/) \/ E. z e. On |^| S = suc z \/ ( |^| S e. _V /\ Lim |^| S ) ) )
49 oveq2 
 |-  ( |^| S = (/) -> ( C +o |^| S ) = ( C +o (/) ) )
50 49 22 sylan9eqr 
 |-  ( ( ph /\ |^| S = (/) ) -> ( C +o |^| S ) = C )
51 onelpss 
 |-  ( ( C e. On /\ D e. On ) -> ( C e. D <-> ( C C_ D /\ C =/= D ) ) )
52 12 4 51 syl2anc 
 |-  ( ph -> ( C e. D <-> ( C C_ D /\ C =/= D ) ) )
53 3 52 mpbid 
 |-  ( ph -> ( C C_ D /\ C =/= D ) )
54 53 simpld 
 |-  ( ph -> C C_ D )
55 54 adantr 
 |-  ( ( ph /\ |^| S = (/) ) -> C C_ D )
56 50 55 eqsstrd 
 |-  ( ( ph /\ |^| S = (/) ) -> ( C +o |^| S ) C_ D )
57 56 ex 
 |-  ( ph -> ( |^| S = (/) -> ( C +o |^| S ) C_ D ) )
58 oveq2 
 |-  ( |^| S = suc z -> ( C +o |^| S ) = ( C +o suc z ) )
59 oasuc 
 |-  ( ( C e. On /\ z e. On ) -> ( C +o suc z ) = suc ( C +o z ) )
60 12 59 sylan 
 |-  ( ( ph /\ z e. On ) -> ( C +o suc z ) = suc ( C +o z ) )
61 58 60 sylan9eqr 
 |-  ( ( ( ph /\ z e. On ) /\ |^| S = suc z ) -> ( C +o |^| S ) = suc ( C +o z ) )
62 vex 
 |-  z e. _V
63 62 sucid 
 |-  z e. suc z
64 eleq2 
 |-  ( |^| S = suc z -> ( z e. |^| S <-> z e. suc z ) )
65 63 64 mpbiri 
 |-  ( |^| S = suc z -> z e. |^| S )
66 65 a1i 
 |-  ( ( ph /\ z e. On ) -> ( |^| S = suc z -> z e. |^| S ) )
67 43 eleq2i 
 |-  ( z e. |^| S <-> z e. |^| { y e. On | D C_ ( C +o y ) } )
68 oveq2 
 |-  ( y = z -> ( C +o y ) = ( C +o z ) )
69 68 sseq2d 
 |-  ( y = z -> ( D C_ ( C +o y ) <-> D C_ ( C +o z ) ) )
70 69 onnminsb 
 |-  ( z e. On -> ( z e. |^| { y e. On | D C_ ( C +o y ) } -> -. D C_ ( C +o z ) ) )
71 70 adantl 
 |-  ( ( ph /\ z e. On ) -> ( z e. |^| { y e. On | D C_ ( C +o y ) } -> -. D C_ ( C +o z ) ) )
72 67 71 biimtrid 
 |-  ( ( ph /\ z e. On ) -> ( z e. |^| S -> -. D C_ ( C +o z ) ) )
73 oacl 
 |-  ( ( C e. On /\ z e. On ) -> ( C +o z ) e. On )
74 12 73 sylan 
 |-  ( ( ph /\ z e. On ) -> ( C +o z ) e. On )
75 ontri1 
 |-  ( ( D e. On /\ ( C +o z ) e. On ) -> ( D C_ ( C +o z ) <-> -. ( C +o z ) e. D ) )
76 4 74 75 syl2an2r 
 |-  ( ( ph /\ z e. On ) -> ( D C_ ( C +o z ) <-> -. ( C +o z ) e. D ) )
77 76 con2bid 
 |-  ( ( ph /\ z e. On ) -> ( ( C +o z ) e. D <-> -. D C_ ( C +o z ) ) )
78 72 77 sylibrd 
 |-  ( ( ph /\ z e. On ) -> ( z e. |^| S -> ( C +o z ) e. D ) )
79 onsucss 
 |-  ( D e. On -> ( ( C +o z ) e. D -> suc ( C +o z ) C_ D ) )
80 4 79 syl 
 |-  ( ph -> ( ( C +o z ) e. D -> suc ( C +o z ) C_ D ) )
81 80 adantr 
 |-  ( ( ph /\ z e. On ) -> ( ( C +o z ) e. D -> suc ( C +o z ) C_ D ) )
82 66 78 81 3syld 
 |-  ( ( ph /\ z e. On ) -> ( |^| S = suc z -> suc ( C +o z ) C_ D ) )
83 82 imp 
 |-  ( ( ( ph /\ z e. On ) /\ |^| S = suc z ) -> suc ( C +o z ) C_ D )
84 61 83 eqsstrd 
 |-  ( ( ( ph /\ z e. On ) /\ |^| S = suc z ) -> ( C +o |^| S ) C_ D )
85 84 rexlimdva2 
 |-  ( ph -> ( E. z e. On |^| S = suc z -> ( C +o |^| S ) C_ D ) )
86 oalim 
 |-  ( ( C e. On /\ ( |^| S e. _V /\ Lim |^| S ) ) -> ( C +o |^| S ) = U_ z e. |^| S ( C +o z ) )
87 12 86 sylan 
 |-  ( ( ph /\ ( |^| S e. _V /\ Lim |^| S ) ) -> ( C +o |^| S ) = U_ z e. |^| S ( C +o z ) )
88 onelon 
 |-  ( ( |^| S e. On /\ z e. |^| S ) -> z e. On )
89 19 88 sylan 
 |-  ( ( ph /\ z e. |^| S ) -> z e. On )
90 89 ex 
 |-  ( ph -> ( z e. |^| S -> z e. On ) )
91 90 ancrd 
 |-  ( ph -> ( z e. |^| S -> ( z e. On /\ z e. |^| S ) ) )
92 78 expimpd 
 |-  ( ph -> ( ( z e. On /\ z e. |^| S ) -> ( C +o z ) e. D ) )
93 onelss 
 |-  ( D e. On -> ( ( C +o z ) e. D -> ( C +o z ) C_ D ) )
94 4 93 syl 
 |-  ( ph -> ( ( C +o z ) e. D -> ( C +o z ) C_ D ) )
95 91 92 94 3syld 
 |-  ( ph -> ( z e. |^| S -> ( C +o z ) C_ D ) )
96 95 ralrimiv 
 |-  ( ph -> A. z e. |^| S ( C +o z ) C_ D )
97 iunss 
 |-  ( U_ z e. |^| S ( C +o z ) C_ D <-> A. z e. |^| S ( C +o z ) C_ D )
98 96 97 sylibr 
 |-  ( ph -> U_ z e. |^| S ( C +o z ) C_ D )
99 98 adantr 
 |-  ( ( ph /\ ( |^| S e. _V /\ Lim |^| S ) ) -> U_ z e. |^| S ( C +o z ) C_ D )
100 87 99 eqsstrd 
 |-  ( ( ph /\ ( |^| S e. _V /\ Lim |^| S ) ) -> ( C +o |^| S ) C_ D )
101 100 ex 
 |-  ( ph -> ( ( |^| S e. _V /\ Lim |^| S ) -> ( C +o |^| S ) C_ D ) )
102 57 85 101 3jaod 
 |-  ( ph -> ( ( |^| S = (/) \/ E. z e. On |^| S = suc z \/ ( |^| S e. _V /\ Lim |^| S ) ) -> ( C +o |^| S ) C_ D ) )
103 48 102 mpd 
 |-  ( ph -> ( C +o |^| S ) C_ D )
104 10 rspcev 
 |-  ( ( D e. On /\ D C_ ( C +o D ) ) -> E. y e. On D C_ ( C +o y ) )
105 4 14 104 syl2anc 
 |-  ( ph -> E. y e. On D C_ ( C +o y ) )
106 nfcv 
 |-  F/_ y D
107 nfcv 
 |-  F/_ y C
108 nfcv 
 |-  F/_ y +o
109 nfrab1 
 |-  F/_ y { y e. On | D C_ ( C +o y ) }
110 109 nfint 
 |-  F/_ y |^| { y e. On | D C_ ( C +o y ) }
111 107 108 110 nfov 
 |-  F/_ y ( C +o |^| { y e. On | D C_ ( C +o y ) } )
112 106 111 nfss 
 |-  F/ y D C_ ( C +o |^| { y e. On | D C_ ( C +o y ) } )
113 oveq2 
 |-  ( y = |^| { y e. On | D C_ ( C +o y ) } -> ( C +o y ) = ( C +o |^| { y e. On | D C_ ( C +o y ) } ) )
114 113 sseq2d 
 |-  ( y = |^| { y e. On | D C_ ( C +o y ) } -> ( D C_ ( C +o y ) <-> D C_ ( C +o |^| { y e. On | D C_ ( C +o y ) } ) ) )
115 112 114 onminsb 
 |-  ( E. y e. On D C_ ( C +o y ) -> D C_ ( C +o |^| { y e. On | D C_ ( C +o y ) } ) )
116 105 115 syl 
 |-  ( ph -> D C_ ( C +o |^| { y e. On | D C_ ( C +o y ) } ) )
117 43 oveq2i 
 |-  ( C +o |^| S ) = ( C +o |^| { y e. On | D C_ ( C +o y ) } )
118 116 117 sseqtrrdi 
 |-  ( ph -> D C_ ( C +o |^| S ) )
119 103 118 eqssd 
 |-  ( ph -> ( C +o |^| S ) = D )
120 omelon 
 |-  _om e. On
121 omcl 
 |-  ( ( _om e. On /\ D e. On ) -> ( _om .o D ) e. On )
122 120 4 121 sylancr 
 |-  ( ph -> ( _om .o D ) e. On )
123 120 a1i 
 |-  ( ph -> _om e. On )
124 6 5 jca 
 |-  ( ph -> ( N e. M /\ M e. _om ) )
125 ontr1 
 |-  ( _om e. On -> ( ( N e. M /\ M e. _om ) -> N e. _om ) )
126 123 124 125 sylc 
 |-  ( ph -> N e. _om )
127 nnon 
 |-  ( N e. _om -> N e. On )
128 126 127 syl 
 |-  ( ph -> N e. On )
129 oaword1 
 |-  ( ( ( _om .o D ) e. On /\ N e. On ) -> ( _om .o D ) C_ ( ( _om .o D ) +o N ) )
130 122 128 129 syl2anc 
 |-  ( ph -> ( _om .o D ) C_ ( ( _om .o D ) +o N ) )
131 1 oveq1d 
 |-  ( ph -> ( A +o ( _om .o |^| S ) ) = ( ( ( _om .o C ) +o M ) +o ( _om .o |^| S ) ) )
132 omcl 
 |-  ( ( _om e. On /\ C e. On ) -> ( _om .o C ) e. On )
133 120 12 132 sylancr 
 |-  ( ph -> ( _om .o C ) e. On )
134 nnon 
 |-  ( M e. _om -> M e. On )
135 5 134 syl 
 |-  ( ph -> M e. On )
136 omcl 
 |-  ( ( _om e. On /\ |^| S e. On ) -> ( _om .o |^| S ) e. On )
137 120 19 136 sylancr 
 |-  ( ph -> ( _om .o |^| S ) e. On )
138 oaass 
 |-  ( ( ( _om .o C ) e. On /\ M e. On /\ ( _om .o |^| S ) e. On ) -> ( ( ( _om .o C ) +o M ) +o ( _om .o |^| S ) ) = ( ( _om .o C ) +o ( M +o ( _om .o |^| S ) ) ) )
139 133 135 137 138 syl3anc 
 |-  ( ph -> ( ( ( _om .o C ) +o M ) +o ( _om .o |^| S ) ) = ( ( _om .o C ) +o ( M +o ( _om .o |^| S ) ) ) )
140 19 120 jctil 
 |-  ( ph -> ( _om e. On /\ |^| S e. On ) )
141 omword1 
 |-  ( ( ( _om e. On /\ |^| S e. On ) /\ (/) e. |^| S ) -> _om C_ ( _om .o |^| S ) )
142 140 44 141 syl2anc 
 |-  ( ph -> _om C_ ( _om .o |^| S ) )
143 oaabs 
 |-  ( ( ( M e. _om /\ ( _om .o |^| S ) e. On ) /\ _om C_ ( _om .o |^| S ) ) -> ( M +o ( _om .o |^| S ) ) = ( _om .o |^| S ) )
144 5 137 142 143 syl21anc 
 |-  ( ph -> ( M +o ( _om .o |^| S ) ) = ( _om .o |^| S ) )
145 144 oveq2d 
 |-  ( ph -> ( ( _om .o C ) +o ( M +o ( _om .o |^| S ) ) ) = ( ( _om .o C ) +o ( _om .o |^| S ) ) )
146 odi 
 |-  ( ( _om e. On /\ C e. On /\ |^| S e. On ) -> ( _om .o ( C +o |^| S ) ) = ( ( _om .o C ) +o ( _om .o |^| S ) ) )
147 123 12 19 146 syl3anc 
 |-  ( ph -> ( _om .o ( C +o |^| S ) ) = ( ( _om .o C ) +o ( _om .o |^| S ) ) )
148 119 oveq2d 
 |-  ( ph -> ( _om .o ( C +o |^| S ) ) = ( _om .o D ) )
149 145 147 148 3eqtr2d 
 |-  ( ph -> ( ( _om .o C ) +o ( M +o ( _om .o |^| S ) ) ) = ( _om .o D ) )
150 131 139 149 3eqtrd 
 |-  ( ph -> ( A +o ( _om .o |^| S ) ) = ( _om .o D ) )
151 130 150 2 3sstr4d 
 |-  ( ph -> ( A +o ( _om .o |^| S ) ) C_ B )
152 naddcl 
 |-  ( ( ( _om .o C ) e. On /\ ( _om .o |^| S ) e. On ) -> ( ( _om .o C ) +no ( _om .o |^| S ) ) e. On )
153 133 137 152 syl2anc 
 |-  ( ph -> ( ( _om .o C ) +no ( _om .o |^| S ) ) e. On )
154 122 153 135 3jca 
 |-  ( ph -> ( ( _om .o D ) e. On /\ ( ( _om .o C ) +no ( _om .o |^| S ) ) e. On /\ M e. On ) )
155 148 147 eqtr3d 
 |-  ( ph -> ( _om .o D ) = ( ( _om .o C ) +o ( _om .o |^| S ) ) )
156 naddgeoa 
 |-  ( ( ( _om .o C ) e. On /\ ( _om .o |^| S ) e. On ) -> ( ( _om .o C ) +o ( _om .o |^| S ) ) C_ ( ( _om .o C ) +no ( _om .o |^| S ) ) )
157 133 137 156 syl2anc 
 |-  ( ph -> ( ( _om .o C ) +o ( _om .o |^| S ) ) C_ ( ( _om .o C ) +no ( _om .o |^| S ) ) )
158 155 157 eqsstrd 
 |-  ( ph -> ( _om .o D ) C_ ( ( _om .o C ) +no ( _om .o |^| S ) ) )
159 oawordri 
 |-  ( ( ( _om .o D ) e. On /\ ( ( _om .o C ) +no ( _om .o |^| S ) ) e. On /\ M e. On ) -> ( ( _om .o D ) C_ ( ( _om .o C ) +no ( _om .o |^| S ) ) -> ( ( _om .o D ) +o M ) C_ ( ( ( _om .o C ) +no ( _om .o |^| S ) ) +o M ) ) )
160 154 158 159 sylc 
 |-  ( ph -> ( ( _om .o D ) +o M ) C_ ( ( ( _om .o C ) +no ( _om .o |^| S ) ) +o M ) )
161 naddonnn 
 |-  ( ( ( _om .o C ) e. On /\ M e. _om ) -> ( ( _om .o C ) +o M ) = ( ( _om .o C ) +no M ) )
162 133 5 161 syl2anc 
 |-  ( ph -> ( ( _om .o C ) +o M ) = ( ( _om .o C ) +no M ) )
163 1 162 eqtrd 
 |-  ( ph -> A = ( ( _om .o C ) +no M ) )
164 163 oveq1d 
 |-  ( ph -> ( A +no ( _om .o |^| S ) ) = ( ( ( _om .o C ) +no M ) +no ( _om .o |^| S ) ) )
165 naddass 
 |-  ( ( ( _om .o C ) e. On /\ M e. On /\ ( _om .o |^| S ) e. On ) -> ( ( ( _om .o C ) +no M ) +no ( _om .o |^| S ) ) = ( ( _om .o C ) +no ( M +no ( _om .o |^| S ) ) ) )
166 133 135 137 165 syl3anc 
 |-  ( ph -> ( ( ( _om .o C ) +no M ) +no ( _om .o |^| S ) ) = ( ( _om .o C ) +no ( M +no ( _om .o |^| S ) ) ) )
167 naddcom 
 |-  ( ( M e. On /\ ( _om .o |^| S ) e. On ) -> ( M +no ( _om .o |^| S ) ) = ( ( _om .o |^| S ) +no M ) )
168 135 137 167 syl2anc 
 |-  ( ph -> ( M +no ( _om .o |^| S ) ) = ( ( _om .o |^| S ) +no M ) )
169 168 oveq2d 
 |-  ( ph -> ( ( _om .o C ) +no ( M +no ( _om .o |^| S ) ) ) = ( ( _om .o C ) +no ( ( _om .o |^| S ) +no M ) ) )
170 naddonnn 
 |-  ( ( ( ( _om .o C ) +no ( _om .o |^| S ) ) e. On /\ M e. _om ) -> ( ( ( _om .o C ) +no ( _om .o |^| S ) ) +o M ) = ( ( ( _om .o C ) +no ( _om .o |^| S ) ) +no M ) )
171 153 5 170 syl2anc 
 |-  ( ph -> ( ( ( _om .o C ) +no ( _om .o |^| S ) ) +o M ) = ( ( ( _om .o C ) +no ( _om .o |^| S ) ) +no M ) )
172 naddass 
 |-  ( ( ( _om .o C ) e. On /\ ( _om .o |^| S ) e. On /\ M e. On ) -> ( ( ( _om .o C ) +no ( _om .o |^| S ) ) +no M ) = ( ( _om .o C ) +no ( ( _om .o |^| S ) +no M ) ) )
173 133 137 135 172 syl3anc 
 |-  ( ph -> ( ( ( _om .o C ) +no ( _om .o |^| S ) ) +no M ) = ( ( _om .o C ) +no ( ( _om .o |^| S ) +no M ) ) )
174 171 173 eqtr2d 
 |-  ( ph -> ( ( _om .o C ) +no ( ( _om .o |^| S ) +no M ) ) = ( ( ( _om .o C ) +no ( _om .o |^| S ) ) +o M ) )
175 166 169 174 3eqtrd 
 |-  ( ph -> ( ( ( _om .o C ) +no M ) +no ( _om .o |^| S ) ) = ( ( ( _om .o C ) +no ( _om .o |^| S ) ) +o M ) )
176 164 175 eqtr2d 
 |-  ( ph -> ( ( ( _om .o C ) +no ( _om .o |^| S ) ) +o M ) = ( A +no ( _om .o |^| S ) ) )
177 160 176 sseqtrd 
 |-  ( ph -> ( ( _om .o D ) +o M ) C_ ( A +no ( _om .o |^| S ) ) )
178 135 122 jca 
 |-  ( ph -> ( M e. On /\ ( _om .o D ) e. On ) )
179 oaordi 
 |-  ( ( M e. On /\ ( _om .o D ) e. On ) -> ( N e. M -> ( ( _om .o D ) +o N ) e. ( ( _om .o D ) +o M ) ) )
180 178 6 179 sylc 
 |-  ( ph -> ( ( _om .o D ) +o N ) e. ( ( _om .o D ) +o M ) )
181 2 180 eqeltrd 
 |-  ( ph -> B e. ( ( _om .o D ) +o M ) )
182 177 181 sseldd 
 |-  ( ph -> B e. ( A +no ( _om .o |^| S ) ) )
183 119 151 182 3jca 
 |-  ( ph -> ( ( C +o |^| S ) = D /\ ( A +o ( _om .o |^| S ) ) C_ B /\ B e. ( A +no ( _om .o |^| S ) ) ) )
184 oveq2 
 |-  ( x = |^| S -> ( C +o x ) = ( C +o |^| S ) )
185 184 eqeq1d 
 |-  ( x = |^| S -> ( ( C +o x ) = D <-> ( C +o |^| S ) = D ) )
186 oveq2 
 |-  ( x = |^| S -> ( _om .o x ) = ( _om .o |^| S ) )
187 186 oveq2d 
 |-  ( x = |^| S -> ( A +o ( _om .o x ) ) = ( A +o ( _om .o |^| S ) ) )
188 187 sseq1d 
 |-  ( x = |^| S -> ( ( A +o ( _om .o x ) ) C_ B <-> ( A +o ( _om .o |^| S ) ) C_ B ) )
189 186 oveq2d 
 |-  ( x = |^| S -> ( A +no ( _om .o x ) ) = ( A +no ( _om .o |^| S ) ) )
190 189 eleq2d 
 |-  ( x = |^| S -> ( B e. ( A +no ( _om .o x ) ) <-> B e. ( A +no ( _om .o |^| S ) ) ) )
191 185 188 190 3anbi123d 
 |-  ( x = |^| S -> ( ( ( C +o x ) = D /\ ( A +o ( _om .o x ) ) C_ B /\ B e. ( A +no ( _om .o x ) ) ) <-> ( ( C +o |^| S ) = D /\ ( A +o ( _om .o |^| S ) ) C_ B /\ B e. ( A +no ( _om .o |^| S ) ) ) ) )
192 191 rspcev 
 |-  ( ( |^| S e. ( On \ 1o ) /\ ( ( C +o |^| S ) = D /\ ( A +o ( _om .o |^| S ) ) C_ B /\ B e. ( A +no ( _om .o |^| S ) ) ) ) -> E. x e. ( On \ 1o ) ( ( C +o x ) = D /\ ( A +o ( _om .o x ) ) C_ B /\ B e. ( A +no ( _om .o x ) ) ) )
193 46 183 192 syl2anc 
 |-  ( ph -> E. x e. ( On \ 1o ) ( ( C +o x ) = D /\ ( A +o ( _om .o x ) ) C_ B /\ B e. ( A +no ( _om .o x ) ) ) )