MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oaabs2 Unicode version

Theorem oaabs2 6659
Description: The absorption law oaabs 6658 is also a property of higher powers of  om. (Contributed by Mario Carneiro, 29-May-2015.)
Assertion
Ref Expression
oaabs2  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  ( A  +o  B )  =  B )

Proof of Theorem oaabs2
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 n0i 3473 . . . . . . 7  |-  ( A  e.  ( om  ^o  C )  ->  -.  ( om  ^o  C )  =  (/) )
2 fnoe 6525 . . . . . . . . 9  |-  ^o  Fn  ( On  X.  On )
3 fndm 5359 . . . . . . . . 9  |-  (  ^o  Fn  ( On  X.  On )  ->  dom  ^o  =  ( On  X.  On ) )
42, 3ax-mp 8 . . . . . . . 8  |-  dom  ^o  =  ( On  X.  On )
54ndmov 6020 . . . . . . 7  |-  ( -.  ( om  e.  On  /\  C  e.  On )  ->  ( om  ^o  C )  =  (/) )
61, 5nsyl2 119 . . . . . 6  |-  ( A  e.  ( om  ^o  C )  ->  ( om  e.  On  /\  C  e.  On ) )
76ad2antrr 706 . . . . 5  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  ( om  e.  On  /\  C  e.  On ) )
8 oecl 6552 . . . . 5  |-  ( ( om  e.  On  /\  C  e.  On )  ->  ( om  ^o  C
)  e.  On )
97, 8syl 15 . . . 4  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  ( om  ^o  C )  e.  On )
10 simplr 731 . . . 4  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  B  e.  On )
11 simpr 447 . . . 4  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  ( om  ^o  C )  C_  B
)
12 oawordeu 6569 . . . 4  |-  ( ( ( ( om  ^o  C )  e.  On  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  E! x  e.  On  ( ( om 
^o  C )  +o  x )  =  B )
139, 10, 11, 12syl21anc 1181 . . 3  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  E! x  e.  On  ( ( om 
^o  C )  +o  x )  =  B )
14 reurex 2767 . . 3  |-  ( E! x  e.  On  (
( om  ^o  C
)  +o  x )  =  B  ->  E. x  e.  On  ( ( om 
^o  C )  +o  x )  =  B )
1513, 14syl 15 . 2  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  E. x  e.  On  ( ( om 
^o  C )  +o  x )  =  B )
16 simpll 730 . . . . . . . 8  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  A  e.  ( om  ^o  C ) )
17 onelon 4433 . . . . . . . 8  |-  ( ( ( om  ^o  C
)  e.  On  /\  A  e.  ( om  ^o  C ) )  ->  A  e.  On )
189, 16, 17syl2anc 642 . . . . . . 7  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  A  e.  On )
1918adantr 451 . . . . . 6  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  x  e.  On )  ->  A  e.  On )
209adantr 451 . . . . . 6  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  x  e.  On )  ->  ( om  ^o  C )  e.  On )
21 simpr 447 . . . . . 6  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  x  e.  On )  ->  x  e.  On )
22 oaass 6575 . . . . . 6  |-  ( ( A  e.  On  /\  ( om  ^o  C )  e.  On  /\  x  e.  On )  ->  (
( A  +o  ( om  ^o  C ) )  +o  x )  =  ( A  +o  (
( om  ^o  C
)  +o  x ) ) )
2319, 20, 21, 22syl3anc 1182 . . . . 5  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  x  e.  On )  ->  (
( A  +o  ( om  ^o  C ) )  +o  x )  =  ( A  +o  (
( om  ^o  C
)  +o  x ) ) )
247simprd 449 . . . . . . . . . 10  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  C  e.  On )
25 eloni 4418 . . . . . . . . . 10  |-  ( C  e.  On  ->  Ord  C )
2624, 25syl 15 . . . . . . . . 9  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  Ord  C )
27 ordzsl 4652 . . . . . . . . 9  |-  ( Ord 
C  <->  ( C  =  (/)  \/  E. x  e.  On  C  =  suc  x  \/  Lim  C ) )
2826, 27sylib 188 . . . . . . . 8  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  ( C  =  (/)  \/  E. x  e.  On  C  =  suc  x  \/  Lim  C ) )
29 simplll 734 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  C  =  (/) )  ->  A  e.  ( om  ^o  C
) )
30 oveq2 5882 . . . . . . . . . . . . . . 15  |-  ( C  =  (/)  ->  ( om 
^o  C )  =  ( om  ^o  (/) ) )
317simpld 445 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  om  e.  On )
32 oe0 6537 . . . . . . . . . . . . . . . 16  |-  ( om  e.  On  ->  ( om  ^o  (/) )  =  1o )
3331, 32syl 15 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  ( om  ^o  (/) )  =  1o )
3430, 33sylan9eqr 2350 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  C  =  (/) )  ->  ( om  ^o  C )  =  1o )
3529, 34eleqtrd 2372 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  C  =  (/) )  ->  A  e.  1o )
36 el1o 6514 . . . . . . . . . . . . 13  |-  ( A  e.  1o  <->  A  =  (/) )
3735, 36sylib 188 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  C  =  (/) )  ->  A  =  (/) )
3837oveq1d 5889 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  C  =  (/) )  ->  ( A  +o  ( om  ^o  C ) )  =  ( (/)  +o  ( om  ^o  C ) ) )
399adantr 451 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  C  =  (/) )  ->  ( om  ^o  C )  e.  On )
40 oa0r 6553 . . . . . . . . . . . 12  |-  ( ( om  ^o  C )  e.  On  ->  ( (/) 
+o  ( om  ^o  C ) )  =  ( om  ^o  C
) )
4139, 40syl 15 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  C  =  (/) )  ->  ( (/) 
+o  ( om  ^o  C ) )  =  ( om  ^o  C
) )
4238, 41eqtrd 2328 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  C  =  (/) )  ->  ( A  +o  ( om  ^o  C ) )  =  ( om  ^o  C
) )
4342ex 423 . . . . . . . . 9  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  ( C  =  (/)  ->  ( A  +o  ( om  ^o  C
) )  =  ( om  ^o  C ) ) )
4431adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  ->  om  e.  On )
45 simprl 732 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  ->  x  e.  On )
46 oecl 6552 . . . . . . . . . . . . . . 15  |-  ( ( om  e.  On  /\  x  e.  On )  ->  ( om  ^o  x
)  e.  On )
4744, 45, 46syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  ->  ( om  ^o  x )  e.  On )
48 limom 4687 . . . . . . . . . . . . . . 15  |-  Lim  om
4944, 48jctir 524 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  ->  ( om  e.  On  /\  Lim  om ) )
50 simplll 734 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  ->  A  e.  ( om  ^o  C ) )
51 simprr 733 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  ->  C  =  suc  x )
5251oveq2d 5890 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  ->  ( om  ^o  C )  =  ( om  ^o  suc  x
) )
53 oesuc 6542 . . . . . . . . . . . . . . . . 17  |-  ( ( om  e.  On  /\  x  e.  On )  ->  ( om  ^o  suc  x )  =  ( ( om  ^o  x
)  .o  om )
)
5444, 45, 53syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  ->  ( om  ^o 
suc  x )  =  ( ( om  ^o  x )  .o  om ) )
5552, 54eqtrd 2328 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  ->  ( om  ^o  C )  =  ( ( om  ^o  x
)  .o  om )
)
5650, 55eleqtrd 2372 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  ->  A  e.  ( ( om  ^o  x )  .o  om ) )
57 omordlim 6591 . . . . . . . . . . . . . 14  |-  ( ( ( ( om  ^o  x )  e.  On  /\  ( om  e.  On  /\ 
Lim  om ) )  /\  A  e.  ( ( om  ^o  x )  .o 
om ) )  ->  E. y  e.  om  A  e.  ( ( om  ^o  x )  .o  y ) )
5847, 49, 56, 57syl21anc 1181 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  ->  E. y  e.  om  A  e.  ( ( om  ^o  x
)  .o  y ) )
5947adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  /\  ( y  e.  om  /\  A  e.  ( ( om  ^o  x )  .o  y
) ) )  -> 
( om  ^o  x
)  e.  On )
60 nnon 4678 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  om  ->  y  e.  On )
6160ad2antrl 708 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  /\  ( y  e.  om  /\  A  e.  ( ( om  ^o  x )  .o  y
) ) )  -> 
y  e.  On )
62 omcl 6551 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( om  ^o  x
)  e.  On  /\  y  e.  On )  ->  ( ( om  ^o  x )  .o  y
)  e.  On )
6359, 61, 62syl2anc 642 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  /\  ( y  e.  om  /\  A  e.  ( ( om  ^o  x )  .o  y
) ) )  -> 
( ( om  ^o  x )  .o  y
)  e.  On )
64 eloni 4418 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( om  ^o  x
)  .o  y )  e.  On  ->  Ord  ( ( om  ^o  x )  .o  y
) )
6563, 64syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  /\  ( y  e.  om  /\  A  e.  ( ( om  ^o  x )  .o  y
) ) )  ->  Ord  ( ( om  ^o  x )  .o  y
) )
66 simprr 733 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  /\  ( y  e.  om  /\  A  e.  ( ( om  ^o  x )  .o  y
) ) )  ->  A  e.  ( ( om  ^o  x )  .o  y ) )
67 ordelss 4424 . . . . . . . . . . . . . . . . . 18  |-  ( ( Ord  ( ( om 
^o  x )  .o  y )  /\  A  e.  ( ( om  ^o  x )  .o  y
) )  ->  A  C_  ( ( om  ^o  x )  .o  y
) )
6865, 66, 67syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  /\  ( y  e.  om  /\  A  e.  ( ( om  ^o  x )  .o  y
) ) )  ->  A  C_  ( ( om 
^o  x )  .o  y ) )
6918ad2antrr 706 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  /\  ( y  e.  om  /\  A  e.  ( ( om  ^o  x )  .o  y
) ) )  ->  A  e.  On )
709ad2antrr 706 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  /\  ( y  e.  om  /\  A  e.  ( ( om  ^o  x )  .o  y
) ) )  -> 
( om  ^o  C
)  e.  On )
71 oawordri 6564 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  On  /\  ( ( om  ^o  x )  .o  y
)  e.  On  /\  ( om  ^o  C )  e.  On )  -> 
( A  C_  (
( om  ^o  x
)  .o  y )  ->  ( A  +o  ( om  ^o  C ) )  C_  ( (
( om  ^o  x
)  .o  y )  +o  ( om  ^o  C ) ) ) )
7269, 63, 70, 71syl3anc 1182 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  /\  ( y  e.  om  /\  A  e.  ( ( om  ^o  x )  .o  y
) ) )  -> 
( A  C_  (
( om  ^o  x
)  .o  y )  ->  ( A  +o  ( om  ^o  C ) )  C_  ( (
( om  ^o  x
)  .o  y )  +o  ( om  ^o  C ) ) ) )
7368, 72mpd 14 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  /\  ( y  e.  om  /\  A  e.  ( ( om  ^o  x )  .o  y
) ) )  -> 
( A  +o  ( om  ^o  C ) ) 
C_  ( ( ( om  ^o  x )  .o  y )  +o  ( om  ^o  C
) ) )
7444adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  /\  ( y  e.  om  /\  A  e.  ( ( om  ^o  x )  .o  y
) ) )  ->  om  e.  On )
75 odi 6593 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( om  ^o  x
)  e.  On  /\  y  e.  On  /\  om  e.  On )  ->  (
( om  ^o  x
)  .o  ( y  +o  om ) )  =  ( ( ( om  ^o  x )  .o  y )  +o  ( ( om  ^o  x )  .o  om ) ) )
7659, 61, 74, 75syl3anc 1182 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  /\  ( y  e.  om  /\  A  e.  ( ( om  ^o  x )  .o  y
) ) )  -> 
( ( om  ^o  x )  .o  (
y  +o  om )
)  =  ( ( ( om  ^o  x
)  .o  y )  +o  ( ( om 
^o  x )  .o 
om ) ) )
77 simprl 732 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  /\  ( y  e.  om  /\  A  e.  ( ( om  ^o  x )  .o  y
) ) )  -> 
y  e.  om )
78 oaabslem 6657 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( om  e.  On  /\  y  e.  om )  ->  ( y  +o  om )  =  om )
7974, 77, 78syl2anc 642 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  /\  ( y  e.  om  /\  A  e.  ( ( om  ^o  x )  .o  y
) ) )  -> 
( y  +o  om )  =  om )
8079oveq2d 5890 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  /\  ( y  e.  om  /\  A  e.  ( ( om  ^o  x )  .o  y
) ) )  -> 
( ( om  ^o  x )  .o  (
y  +o  om )
)  =  ( ( om  ^o  x )  .o  om ) )
8176, 80eqtr3d 2330 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  /\  ( y  e.  om  /\  A  e.  ( ( om  ^o  x )  .o  y
) ) )  -> 
( ( ( om 
^o  x )  .o  y )  +o  (
( om  ^o  x
)  .o  om )
)  =  ( ( om  ^o  x )  .o  om ) )
8255adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  /\  ( y  e.  om  /\  A  e.  ( ( om  ^o  x )  .o  y
) ) )  -> 
( om  ^o  C
)  =  ( ( om  ^o  x )  .o  om ) )
8382oveq2d 5890 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  /\  ( y  e.  om  /\  A  e.  ( ( om  ^o  x )  .o  y
) ) )  -> 
( ( ( om 
^o  x )  .o  y )  +o  ( om  ^o  C ) )  =  ( ( ( om  ^o  x )  .o  y )  +o  ( ( om  ^o  x )  .o  om ) ) )
8481, 83, 823eqtr4d 2338 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  /\  ( y  e.  om  /\  A  e.  ( ( om  ^o  x )  .o  y
) ) )  -> 
( ( ( om 
^o  x )  .o  y )  +o  ( om  ^o  C ) )  =  ( om  ^o  C ) )
8573, 84sseqtrd 3227 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  /\  ( y  e.  om  /\  A  e.  ( ( om  ^o  x )  .o  y
) ) )  -> 
( A  +o  ( om  ^o  C ) ) 
C_  ( om  ^o  C ) )
8685expr 598 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  /\  y  e. 
om )  ->  ( A  e.  ( ( om  ^o  x )  .o  y )  ->  ( A  +o  ( om  ^o  C ) )  C_  ( om  ^o  C ) ) )
8786rexlimdva 2680 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  ->  ( E. y  e.  om  A  e.  ( ( om  ^o  x )  .o  y
)  ->  ( A  +o  ( om  ^o  C
) )  C_  ( om  ^o  C ) ) )
8858, 87mpd 14 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  ->  ( A  +o  ( om  ^o  C
) )  C_  ( om  ^o  C ) )
89 oaword2 6567 . . . . . . . . . . . . . 14  |-  ( ( ( om  ^o  C
)  e.  On  /\  A  e.  On )  ->  ( om  ^o  C
)  C_  ( A  +o  ( om  ^o  C
) ) )
909, 18, 89syl2anc 642 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  ( om  ^o  C )  C_  ( A  +o  ( om  ^o  C ) ) )
9190adantr 451 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  ->  ( om  ^o  C )  C_  ( A  +o  ( om  ^o  C ) ) )
9288, 91eqssd 3209 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  ->  ( A  +o  ( om  ^o  C
) )  =  ( om  ^o  C ) )
9392expr 598 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  x  e.  On )  ->  ( C  =  suc  x  -> 
( A  +o  ( om  ^o  C ) )  =  ( om  ^o  C ) ) )
9493rexlimdva 2680 . . . . . . . . 9  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  ( E. x  e.  On  C  =  suc  x  ->  ( A  +o  ( om  ^o  C ) )  =  ( om  ^o  C
) ) )
95 simplll 734 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  ->  A  e.  ( om  ^o  C ) )
9631adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  ->  om  e.  On )
9724adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  ->  C  e.  On )
98 simpr 447 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  ->  Lim  C )
99 oelim2 6609 . . . . . . . . . . . . . . 15  |-  ( ( om  e.  On  /\  ( C  e.  On  /\ 
Lim  C ) )  ->  ( om  ^o  C )  =  U_ x  e.  ( C  \  1o ) ( om 
^o  x ) )
10096, 97, 98, 99syl12anc 1180 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  ->  ( om  ^o  C )  =  U_ x  e.  ( C  \  1o ) ( om 
^o  x ) )
10195, 100eleqtrd 2372 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  ->  A  e.  U_ x  e.  ( C 
\  1o ) ( om  ^o  x ) )
102 eliun 3925 . . . . . . . . . . . . 13  |-  ( A  e.  U_ x  e.  ( C  \  1o ) ( om  ^o  x )  <->  E. x  e.  ( C  \  1o ) A  e.  ( om  ^o  x ) )
103101, 102sylib 188 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  ->  E. x  e.  ( C  \  1o ) A  e.  ( om  ^o  x ) )
104 eldifi 3311 . . . . . . . . . . . . . 14  |-  ( x  e.  ( C  \  1o )  ->  x  e.  C )
10518ad2antrr 706 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x
) ) )  ->  A  e.  On )
1069ad2antrr 706 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x
) ) )  -> 
( om  ^o  C
)  e.  On )
10796adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x
) ) )  ->  om  e.  On )
108 1onn 6653 . . . . . . . . . . . . . . . . . . . 20  |-  1o  e.  om
109108a1i 10 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x
) ) )  ->  1o  e.  om )
110 ondif2 6517 . . . . . . . . . . . . . . . . . . 19  |-  ( om  e.  ( On  \  2o )  <->  ( om  e.  On  /\  1o  e.  om ) )
111107, 109, 110sylanbrc 645 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x
) ) )  ->  om  e.  ( On  \  2o ) )
11297adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x
) ) )  ->  C  e.  On )
113 simplr 731 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x
) ) )  ->  Lim  C )
114 oelimcl 6614 . . . . . . . . . . . . . . . . . 18  |-  ( ( om  e.  ( On 
\  2o )  /\  ( C  e.  On  /\ 
Lim  C ) )  ->  Lim  ( om  ^o  C ) )
115111, 112, 113, 114syl12anc 1180 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x
) ) )  ->  Lim  ( om  ^o  C
) )
116 oalim 6547 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  On  /\  ( ( om  ^o  C )  e.  On  /\ 
Lim  ( om  ^o  C ) ) )  ->  ( A  +o  ( om  ^o  C ) )  =  U_ y  e.  ( om  ^o  C
) ( A  +o  y ) )
117105, 106, 115, 116syl12anc 1180 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x
) ) )  -> 
( A  +o  ( om  ^o  C ) )  =  U_ y  e.  ( om  ^o  C
) ( A  +o  y ) )
118 oelim2 6609 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( om  e.  On  /\  ( C  e.  On  /\ 
Lim  C ) )  ->  ( om  ^o  C )  =  U_ z  e.  ( C  \  1o ) ( om 
^o  z ) )
11996, 97, 98, 118syl12anc 1180 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  ->  ( om  ^o  C )  =  U_ z  e.  ( C  \  1o ) ( om 
^o  z ) )
120119eleq2d 2363 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  ->  ( y  e.  ( om  ^o  C
)  <->  y  e.  U_ z  e.  ( C  \  1o ) ( om 
^o  z ) ) )
121 eliun 3925 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  U_ z  e.  ( C  \  1o ) ( om  ^o  z )  <->  E. z  e.  ( C  \  1o ) y  e.  ( om  ^o  z ) )
122120, 121syl6bb 252 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  ->  ( y  e.  ( om  ^o  C
)  <->  E. z  e.  ( C  \  1o ) y  e.  ( om 
^o  z ) ) )
123122adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x
) ) )  -> 
( y  e.  ( om  ^o  C )  <->  E. z  e.  ( C  \  1o ) y  e.  ( om  ^o  z ) ) )
124 eldifi 3311 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  e.  ( C  \  1o )  ->  z  e.  C )
125107adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  ->  om  e.  On )
126112adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  ->  C  e.  On )
127 simplrl 736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  ->  x  e.  C )
128 onelon 4433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( C  e.  On  /\  x  e.  C )  ->  x  e.  On )
129126, 127, 128syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  ->  x  e.  On )
130125, 129, 46syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  -> 
( om  ^o  x
)  e.  On )
131 eloni 4418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( om  ^o  x )  e.  On  ->  Ord  ( om  ^o  x ) )
132130, 131syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  ->  Ord  ( om  ^o  x
) )
133 simplrr 737 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  ->  A  e.  ( om  ^o  x ) )
134 ordelss 4424 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( Ord  ( om  ^o  x )  /\  A  e.  ( om  ^o  x
) )  ->  A  C_  ( om  ^o  x
) )
135132, 133, 134syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  ->  A  C_  ( om  ^o  x ) )
136 ssun1 3351 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  x  C_  ( x  u.  z
)
13726ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  ->  Ord  C )
138 simprl 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  -> 
z  e.  C )
139 ordunel 4634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( Ord  C  /\  x  e.  C  /\  z  e.  C )  ->  (
x  u.  z )  e.  C )
140137, 127, 138, 139syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  -> 
( x  u.  z
)  e.  C )
141 onelon 4433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( C  e.  On  /\  ( x  u.  z
)  e.  C )  ->  ( x  u.  z )  e.  On )
142126, 140, 141syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  -> 
( x  u.  z
)  e.  On )
143 peano1 4691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  (/)  e.  om
144143a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  ->  (/) 
e.  om )
145 oewordi 6605 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( x  e.  On  /\  ( x  u.  z
)  e.  On  /\  om  e.  On )  /\  (/) 
e.  om )  ->  (
x  C_  ( x  u.  z )  ->  ( om  ^o  x )  C_  ( om  ^o  ( x  u.  z ) ) ) )
146129, 142, 125, 144, 145syl31anc 1185 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  -> 
( x  C_  (
x  u.  z )  ->  ( om  ^o  x )  C_  ( om  ^o  ( x  u.  z ) ) ) )
147136, 146mpi 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  -> 
( om  ^o  x
)  C_  ( om  ^o  ( x  u.  z
) ) )
148135, 147sstrd 3202 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  ->  A  C_  ( om  ^o  ( x  u.  z
) ) )
149105adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  ->  A  e.  On )
150 oecl 6552 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( om  e.  On  /\  ( x  u.  z
)  e.  On )  ->  ( om  ^o  ( x  u.  z
) )  e.  On )
151125, 142, 150syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  -> 
( om  ^o  (
x  u.  z ) )  e.  On )
152 onelon 4433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( C  e.  On  /\  z  e.  C )  ->  z  e.  On )
153126, 138, 152syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  -> 
z  e.  On )
154 oecl 6552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( om  e.  On  /\  z  e.  On )  ->  ( om  ^o  z
)  e.  On )
155125, 153, 154syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  -> 
( om  ^o  z
)  e.  On )
156 simprr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  -> 
y  e.  ( om 
^o  z ) )
157 onelon 4433 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( om  ^o  z
)  e.  On  /\  y  e.  ( om  ^o  z ) )  -> 
y  e.  On )
158155, 156, 157syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  -> 
y  e.  On )
159 oawordri 6564 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( A  e.  On  /\  ( om  ^o  ( x  u.  z ) )  e.  On  /\  y  e.  On )  ->  ( A  C_  ( om  ^o  ( x  u.  z
) )  ->  ( A  +o  y )  C_  ( ( om  ^o  ( x  u.  z
) )  +o  y
) ) )
160149, 151, 158, 159syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  -> 
( A  C_  ( om  ^o  ( x  u.  z ) )  -> 
( A  +o  y
)  C_  ( ( om  ^o  ( x  u.  z ) )  +o  y ) ) )
161148, 160mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  -> 
( A  +o  y
)  C_  ( ( om  ^o  ( x  u.  z ) )  +o  y ) )
162 eloni 4418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( om  ^o  z )  e.  On  ->  Ord  ( om  ^o  z ) )
163155, 162syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  ->  Ord  ( om  ^o  z
) )
164 ordelss 4424 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( Ord  ( om  ^o  z )  /\  y  e.  ( om  ^o  z
) )  ->  y  C_  ( om  ^o  z
) )
165163, 156, 164syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  -> 
y  C_  ( om  ^o  z ) )
166 ssun2 3352 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  z  C_  ( x  u.  z
)
167 oewordi 6605 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( z  e.  On  /\  ( x  u.  z
)  e.  On  /\  om  e.  On )  /\  (/) 
e.  om )  ->  (
z  C_  ( x  u.  z )  ->  ( om  ^o  z )  C_  ( om  ^o  ( x  u.  z ) ) ) )
168153, 142, 125, 144, 167syl31anc 1185 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  -> 
( z  C_  (
x  u.  z )  ->  ( om  ^o  z )  C_  ( om  ^o  ( x  u.  z ) ) ) )
169166, 168mpi 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  -> 
( om  ^o  z
)  C_  ( om  ^o  ( x  u.  z
) ) )
170165, 169sstrd 3202 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  -> 
y  C_  ( om  ^o  ( x  u.  z
) ) )
171 oaword 6563 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( y  e.  On  /\  ( om  ^o  ( x  u.  z ) )  e.  On  /\  ( om  ^o  ( x  u.  z ) )  e.  On )  ->  (
y  C_  ( om  ^o  ( x  u.  z
) )  <->  ( ( om  ^o  ( x  u.  z ) )  +o  y )  C_  (
( om  ^o  (
x  u.  z ) )  +o  ( om 
^o  ( x  u.  z ) ) ) ) )
172158, 151, 151, 171syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  -> 
( y  C_  ( om  ^o  ( x  u.  z ) )  <->  ( ( om  ^o  ( x  u.  z ) )  +o  y )  C_  (
( om  ^o  (
x  u.  z ) )  +o  ( om 
^o  ( x  u.  z ) ) ) ) )
173170, 172mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  -> 
( ( om  ^o  ( x  u.  z
) )  +o  y
)  C_  ( ( om  ^o  ( x  u.  z ) )  +o  ( om  ^o  (
x  u.  z ) ) ) )
174161, 173sstrd 3202 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  -> 
( A  +o  y
)  C_  ( ( om  ^o  ( x  u.  z ) )  +o  ( om  ^o  (
x  u.  z ) ) ) )
175 ordom 4681 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  Ord  om
176 ordsucss 4625 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( Ord 
om  ->  ( 1o  e.  om 
->  suc  1o  C_  om )
)
177175, 108, 176mp2 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  suc  1o  C_ 
om
178 1on 6502 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  1o  e.  On
179 suceloni 4620 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 1o  e.  On  ->  suc  1o  e.  On )
180178, 179mp1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  ->  suc  1o  e.  On )
181 omwordi 6585 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( suc  1o  e.  On  /\ 
om  e.  On  /\  ( om  ^o  ( x  u.  z ) )  e.  On )  -> 
( suc  1o  C_  om  ->  ( ( om  ^o  (
x  u.  z ) )  .o  suc  1o )  C_  ( ( om 
^o  ( x  u.  z ) )  .o 
om ) ) )
182180, 125, 151, 181syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  -> 
( suc  1o  C_  om  ->  ( ( om  ^o  (
x  u.  z ) )  .o  suc  1o )  C_  ( ( om 
^o  ( x  u.  z ) )  .o 
om ) ) )
183177, 182mpi 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  -> 
( ( om  ^o  ( x  u.  z
) )  .o  suc  1o )  C_  ( ( om  ^o  ( x  u.  z ) )  .o 
om ) )
184178a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  ->  1o  e.  On )
185 omsuc 6541 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( om  ^o  (
x  u.  z ) )  e.  On  /\  1o  e.  On )  -> 
( ( om  ^o  ( x  u.  z
) )  .o  suc  1o )  =  ( ( ( om  ^o  (
x  u.  z ) )  .o  1o )  +o  ( om  ^o  ( x  u.  z
) ) ) )
186151, 184, 185syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  -> 
( ( om  ^o  ( x  u.  z
) )  .o  suc  1o )  =  ( ( ( om  ^o  (
x  u.  z ) )  .o  1o )  +o  ( om  ^o  ( x  u.  z
) ) ) )
187 om1 6556 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( om  ^o  ( x  u.  z ) )  e.  On  ->  (
( om  ^o  (
x  u.  z ) )  .o  1o )  =  ( om  ^o  ( x  u.  z
) ) )
188151, 187syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  -> 
( ( om  ^o  ( x  u.  z
) )  .o  1o )  =  ( om  ^o  ( x  u.  z
) ) )
189188oveq1d 5889 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  -> 
( ( ( om 
^o  ( x  u.  z ) )  .o  1o )  +o  ( om  ^o  ( x  u.  z ) ) )  =  ( ( om 
^o  ( x  u.  z ) )  +o  ( om  ^o  (
x  u.  z ) ) ) )
190186, 189eqtr2d 2329 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  -> 
( ( om  ^o  ( x  u.  z
) )  +o  ( om  ^o  ( x  u.  z ) ) )  =  ( ( om 
^o  ( x  u.  z ) )  .o 
suc  1o ) )
191 oesuc 6542 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( om  e.  On  /\  ( x  u.  z
)  e.  On )  ->  ( om  ^o  suc  ( x  u.  z
) )  =  ( ( om  ^o  (
x  u.  z ) )  .o  om )
)
192125, 142, 191syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  -> 
( om  ^o  suc  ( x  u.  z
) )  =  ( ( om  ^o  (
x  u.  z ) )  .o  om )
)
193183, 190, 1923sstr4d 3234 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  -> 
( ( om  ^o  ( x  u.  z
) )  +o  ( om  ^o  ( x  u.  z ) ) ) 
C_  ( om  ^o  suc  ( x  u.  z
) ) )
194174, 193sstrd 3202 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  -> 
( A  +o  y
)  C_  ( om  ^o 
suc  ( x  u.  z ) ) )
195 ordsucss 4625 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( Ord 
C  ->  ( (
x  u.  z )  e.  C  ->  suc  ( x  u.  z
)  C_  C )
)
196137, 140, 195sylc 56 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  ->  suc  ( x  u.  z
)  C_  C )
197 suceloni 4620 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  u.  z )  e.  On  ->  suc  ( x  u.  z
)  e.  On )
198142, 197syl 15 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  ->  suc  ( x  u.  z
)  e.  On )
199 oewordi 6605 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( suc  ( x  u.  z )  e.  On  /\  C  e.  On  /\  om  e.  On )  /\  (/)  e.  om )  ->  ( suc  (
x  u.  z ) 
C_  C  ->  ( om  ^o  suc  ( x  u.  z ) ) 
C_  ( om  ^o  C ) ) )
200198, 126, 125, 144, 199syl31anc 1185 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  -> 
( suc  ( x  u.  z )  C_  C  ->  ( om  ^o  suc  ( x  u.  z
) )  C_  ( om  ^o  C ) ) )
201196, 200mpd 14 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  -> 
( om  ^o  suc  ( x  u.  z
) )  C_  ( om  ^o  C ) )
202194, 201sstrd 3202 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  ( z  e.  C  /\  y  e.  ( om  ^o  z
) ) )  -> 
( A  +o  y
)  C_  ( om  ^o  C ) )
203202expr 598 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  z  e.  C )  ->  (
y  e.  ( om 
^o  z )  -> 
( A  +o  y
)  C_  ( om  ^o  C ) ) )
204124, 203sylan2 460 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( A  e.  ( om 
^o  C )  /\  B  e.  On )  /\  ( om  ^o  C
)  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x ) ) )  /\  z  e.  ( C  \  1o ) )  ->  (
y  e.  ( om 
^o  z )  -> 
( A  +o  y
)  C_  ( om  ^o  C ) ) )
205204rexlimdva 2680 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x
) ) )  -> 
( E. z  e.  ( C  \  1o ) y  e.  ( om  ^o  z )  ->  ( A  +o  y )  C_  ( om  ^o  C ) ) )
206123, 205sylbid 206 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x
) ) )  -> 
( y  e.  ( om  ^o  C )  ->  ( A  +o  y )  C_  ( om  ^o  C ) ) )
207206ralrimiv 2638 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x
) ) )  ->  A. y  e.  ( om  ^o  C ) ( A  +o  y ) 
C_  ( om  ^o  C ) )
208 iunss 3959 . . . . . . . . . . . . . . . . 17  |-  ( U_ y  e.  ( om  ^o  C ) ( A  +o  y )  C_  ( om  ^o  C )  <->  A. y  e.  ( om  ^o  C ) ( A  +o  y ) 
C_  ( om  ^o  C ) )
209207, 208sylibr 203 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x
) ) )  ->  U_ y  e.  ( om  ^o  C ) ( A  +o  y ) 
C_  ( om  ^o  C ) )
210117, 209eqsstrd 3225 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  /\  ( x  e.  C  /\  A  e.  ( om  ^o  x
) ) )  -> 
( A  +o  ( om  ^o  C ) ) 
C_  ( om  ^o  C ) )
211210expr 598 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  /\  x  e.  C )  ->  ( A  e.  ( om  ^o  x )  ->  ( A  +o  ( om  ^o  C ) )  C_  ( om  ^o  C ) ) )
212104, 211sylan2 460 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  /\  x  e.  ( C  \  1o ) )  ->  ( A  e.  ( om  ^o  x )  ->  ( A  +o  ( om  ^o  C ) )  C_  ( om  ^o  C ) ) )
213212rexlimdva 2680 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  ->  ( E. x  e.  ( C  \  1o ) A  e.  ( om  ^o  x
)  ->  ( A  +o  ( om  ^o  C
) )  C_  ( om  ^o  C ) ) )
214103, 213mpd 14 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  ->  ( A  +o  ( om  ^o  C
) )  C_  ( om  ^o  C ) )
21590adantr 451 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  ->  ( om  ^o  C )  C_  ( A  +o  ( om  ^o  C ) ) )
216214, 215eqssd 3209 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  ->  ( A  +o  ( om  ^o  C
) )  =  ( om  ^o  C ) )
217216ex 423 . . . . . . . . 9  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  ( Lim  C  ->  ( A  +o  ( om  ^o  C ) )  =  ( om 
^o  C ) ) )
21843, 94, 2173jaod 1246 . . . . . . . 8  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  ( ( C  =  (/)  \/  E. x  e.  On  C  =  suc  x  \/  Lim  C )  ->  ( A  +o  ( om  ^o  C
) )  =  ( om  ^o  C ) ) )
21928, 218mpd 14 . . . . . . 7  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  ( A  +o  ( om  ^o  C
) )  =  ( om  ^o  C ) )
220219adantr 451 . . . . . 6  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  x  e.  On )  ->  ( A  +o  ( om  ^o  C ) )  =  ( om  ^o  C
) )
221220oveq1d 5889 . . . . 5  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  x  e.  On )  ->  (
( A  +o  ( om  ^o  C ) )  +o  x )  =  ( ( om  ^o  C )  +o  x
) )
22223, 221eqtr3d 2330 . . . 4  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  x  e.  On )  ->  ( A  +o  ( ( om 
^o  C )  +o  x ) )  =  ( ( om  ^o  C )  +o  x
) )
223 oveq2 5882 . . . . 5  |-  ( ( ( om  ^o  C
)  +o  x )  =  B  ->  ( A  +o  ( ( om 
^o  C )  +o  x ) )  =  ( A  +o  B
) )
224 id 19 . . . . 5  |-  ( ( ( om  ^o  C
)  +o  x )  =  B  ->  (
( om  ^o  C
)  +o  x )  =  B )
225223, 224eqeq12d 2310 . . . 4  |-  ( ( ( om  ^o  C
)  +o  x )  =  B  ->  (
( A  +o  (
( om  ^o  C
)  +o  x ) )  =  ( ( om  ^o  C )  +o  x )  <->  ( A  +o  B )  =  B ) )
226222, 225syl5ibcom 211 . . 3  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  x  e.  On )  ->  (
( ( om  ^o  C )  +o  x
)  =  B  -> 
( A  +o  B
)  =  B ) )
227226rexlimdva 2680 . 2  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  ( E. x  e.  On  (
( om  ^o  C
)  +o  x )  =  B  ->  ( A  +o  B )  =  B ) )
22815, 227mpd 14 1  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  ( A  +o  B )  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    \/ w3o 933    = wceq 1632    e. wcel 1696   A.wral 2556   E.wrex 2557   E!wreu 2558    \ cdif 3162    u. cun 3163    C_ wss 3165   (/)c0 3468   U_ciun 3921   Ord word 4407   Oncon0 4408   Lim wlim 4409   suc csuc 4410   omcom 4672    X. cxp 4703   dom cdm 4705    Fn wfn 5266  (class class class)co 5874   1oc1o 6488   2oc2o 6489    +o coa 6492    .o comu 6493    ^o coe 6494
This theorem is referenced by:  cnfcomlem  7418
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-rep 4147  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-reu 2563  df-rmo 2564  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pss 3181  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-tp 3661  df-op 3662  df-uni 3844  df-int 3879  df-iun 3923  df-br 4040  df-opab 4094  df-mpt 4095  df-tr 4130  df-eprel 4321  df-id 4325  df-po 4330  df-so 4331  df-fr 4368  df-we 4370  df-ord 4411  df-on 4412  df-lim 4413  df-suc 4414  df-om 4673  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-ov 5877  df-oprab 5878  df-mpt2 5879  df-1st 6138  df-2nd 6139  df-recs 6404  df-rdg 6439  df-1o 6495  df-2o 6496  df-oadd 6499  df-omul 6500  df-oexp 6501
  Copyright terms: Public domain W3C validator