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

Theorem oaabs2 6847
Description: The absorption law oaabs 6846 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 3593 . . . . . . 7  |-  ( A  e.  ( om  ^o  C )  ->  -.  ( om  ^o  C )  =  (/) )
2 fnoe 6713 . . . . . . . . 9  |-  ^o  Fn  ( On  X.  On )
3 fndm 5503 . . . . . . . . 9  |-  (  ^o  Fn  ( On  X.  On )  ->  dom  ^o  =  ( On  X.  On ) )
42, 3ax-mp 8 . . . . . . . 8  |-  dom  ^o  =  ( On  X.  On )
54ndmov 6190 . . . . . . 7  |-  ( -.  ( om  e.  On  /\  C  e.  On )  ->  ( om  ^o  C )  =  (/) )
61, 5nsyl2 121 . . . . . 6  |-  ( A  e.  ( om  ^o  C )  ->  ( om  e.  On  /\  C  e.  On ) )
76ad2antrr 707 . . . . 5  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  ( om  e.  On  /\  C  e.  On ) )
8 oecl 6740 . . . . 5  |-  ( ( om  e.  On  /\  C  e.  On )  ->  ( om  ^o  C
)  e.  On )
97, 8syl 16 . . . 4  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  ( om  ^o  C )  e.  On )
10 simplr 732 . . . 4  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  B  e.  On )
11 simpr 448 . . . 4  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  ( om  ^o  C )  C_  B
)
12 oawordeu 6757 . . . 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 1183 . . 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 2882 . . 3  |-  ( E! x  e.  On  (
( om  ^o  C
)  +o  x )  =  B  ->  E. x  e.  On  ( ( om 
^o  C )  +o  x )  =  B )
1513, 14syl 16 . 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 731 . . . . . . . 8  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  A  e.  ( om  ^o  C ) )
17 onelon 4566 . . . . . . . 8  |-  ( ( ( om  ^o  C
)  e.  On  /\  A  e.  ( om  ^o  C ) )  ->  A  e.  On )
189, 16, 17syl2anc 643 . . . . . . 7  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  A  e.  On )
1918adantr 452 . . . . . 6  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  x  e.  On )  ->  A  e.  On )
209adantr 452 . . . . . 6  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  x  e.  On )  ->  ( om  ^o  C )  e.  On )
21 simpr 448 . . . . . 6  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  x  e.  On )  ->  x  e.  On )
22 oaass 6763 . . . . . 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 1184 . . . . 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 450 . . . . . . . . . 10  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  C  e.  On )
25 eloni 4551 . . . . . . . . . 10  |-  ( C  e.  On  ->  Ord  C )
2624, 25syl 16 . . . . . . . . 9  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  Ord  C )
27 ordzsl 4784 . . . . . . . . 9  |-  ( Ord 
C  <->  ( C  =  (/)  \/  E. x  e.  On  C  =  suc  x  \/  Lim  C ) )
2826, 27sylib 189 . . . . . . . 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 735 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  C  =  (/) )  ->  A  e.  ( om  ^o  C
) )
30 oveq2 6048 . . . . . . . . . . . . . . 15  |-  ( C  =  (/)  ->  ( om 
^o  C )  =  ( om  ^o  (/) ) )
317simpld 446 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  om  e.  On )
32 oe0 6725 . . . . . . . . . . . . . . . 16  |-  ( om  e.  On  ->  ( om  ^o  (/) )  =  1o )
3331, 32syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  ( om  ^o  (/) )  =  1o )
3430, 33sylan9eqr 2458 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  C  =  (/) )  ->  ( om  ^o  C )  =  1o )
3529, 34eleqtrd 2480 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  C  =  (/) )  ->  A  e.  1o )
36 el1o 6702 . . . . . . . . . . . . 13  |-  ( A  e.  1o  <->  A  =  (/) )
3735, 36sylib 189 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  C  =  (/) )  ->  A  =  (/) )
3837oveq1d 6055 . . . . . . . . . . 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 452 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  C  =  (/) )  ->  ( om  ^o  C )  e.  On )
40 oa0r 6741 . . . . . . . . . . . 12  |-  ( ( om  ^o  C )  e.  On  ->  ( (/) 
+o  ( om  ^o  C ) )  =  ( om  ^o  C
) )
4139, 40syl 16 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  C  =  (/) )  ->  ( (/) 
+o  ( om  ^o  C ) )  =  ( om  ^o  C
) )
4238, 41eqtrd 2436 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  C  =  (/) )  ->  ( A  +o  ( om  ^o  C ) )  =  ( om  ^o  C
) )
4342ex 424 . . . . . . . . 9  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  ( C  =  (/)  ->  ( A  +o  ( om  ^o  C
) )  =  ( om  ^o  C ) ) )
4431adantr 452 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  ->  om  e.  On )
45 simprl 733 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  ->  x  e.  On )
46 oecl 6740 . . . . . . . . . . . . . 14  |-  ( ( om  e.  On  /\  x  e.  On )  ->  ( om  ^o  x
)  e.  On )
4744, 45, 46syl2anc 643 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 4819 . . . . . . . . . . . . . 14  |-  Lim  om
4944, 48jctir 525 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 735 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 734 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  (
x  e.  On  /\  C  =  suc  x ) )  ->  C  =  suc  x )
5251oveq2d 6056 . . . . . . . . . . . . . . 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  suc  x
) )
53 oesuc 6730 . . . . . . . . . . . . . . . 16  |-  ( ( om  e.  On  /\  x  e.  On )  ->  ( om  ^o  suc  x )  =  ( ( om  ^o  x
)  .o  om )
)
5444, 45, 53syl2anc 643 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 2436 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 2480 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 6779 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 1183 . . . . . . . . . . . 12  |-  ( ( ( ( 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 452 . . . . . . . . . . . . . . . . 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
)  e.  On )
60 nnon 4810 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  om  ->  y  e.  On )
6160ad2antrl 709 . . . . . . . . . . . . . . . . 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
) ) )  -> 
y  e.  On )
62 omcl 6739 . . . . . . . . . . . . . . . . 17  |-  ( ( ( om  ^o  x
)  e.  On  /\  y  e.  On )  ->  ( ( om  ^o  x )  .o  y
)  e.  On )
6359, 61, 62syl2anc 643 . . . . . . . . . . . . . . . 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
)  e.  On )
64 eloni 4551 . . . . . . . . . . . . . . . 16  |-  ( ( ( om  ^o  x
)  .o  y )  e.  On  ->  Ord  ( ( om  ^o  x )  .o  y
) )
6563, 64syl 16 . . . . . . . . . . . . . . 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
) ) )  ->  Ord  ( ( om  ^o  x )  .o  y
) )
66 simprr 734 . . . . . . . . . . . . . . 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  e.  ( ( om  ^o  x )  .o  y ) )
67 ordelss 4557 . . . . . . . . . . . . . . 15  |-  ( ( Ord  ( ( om 
^o  x )  .o  y )  /\  A  e.  ( ( om  ^o  x )  .o  y
) )  ->  A  C_  ( ( om  ^o  x )  .o  y
) )
6865, 66, 67syl2anc 643 . . . . . . . . . . . . . 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  C_  ( ( om 
^o  x )  .o  y ) )
6918ad2antrr 707 . . . . . . . . . . . . . . 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  e.  On )
709ad2antrr 707 . . . . . . . . . . . . . . 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
) ) )  -> 
( om  ^o  C
)  e.  On )
71 oawordri 6752 . . . . . . . . . . . . . . 15  |-  ( ( 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 1184 . . . . . . . . . . . . . 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  C_  (
( om  ^o  x
)  .o  y )  ->  ( A  +o  ( om  ^o  C ) )  C_  ( (
( om  ^o  x
)  .o  y )  +o  ( om  ^o  C ) ) ) )
7368, 72mpd 15 . . . . . . . . . . . . 13  |-  ( ( ( ( ( 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 452 . . . . . . . . . . . . . . . 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  e.  On )
75 odi 6781 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 1184 . . . . . . . . . . . . . . 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
) ) )  -> 
( ( om  ^o  x )  .o  (
y  +o  om )
)  =  ( ( ( om  ^o  x
)  .o  y )  +o  ( ( om 
^o  x )  .o 
om ) ) )
77 simprl 733 . . . . . . . . . . . . . . . . 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
) ) )  -> 
y  e.  om )
78 oaabslem 6845 . . . . . . . . . . . . . . . . 17  |-  ( ( om  e.  On  /\  y  e.  om )  ->  ( y  +o  om )  =  om )
7974, 77, 78syl2anc 643 . . . . . . . . . . . . . . . 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
) ) )  -> 
( y  +o  om )  =  om )
8079oveq2d 6056 . . . . . . . . . . . . . . 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
) ) )  -> 
( ( om  ^o  x )  .o  (
y  +o  om )
)  =  ( ( om  ^o  x )  .o  om ) )
8176, 80eqtr3d 2438 . . . . . . . . . . . . . 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
) ) )  -> 
( ( ( om 
^o  x )  .o  y )  +o  (
( om  ^o  x
)  .o  om )
)  =  ( ( om  ^o  x )  .o  om ) )
8255adantr 452 . . . . . . . . . . . . . . 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
) ) )  -> 
( om  ^o  C
)  =  ( ( om  ^o  x )  .o  om ) )
8382oveq2d 6056 . . . . . . . . . . . . . 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
) ) )  -> 
( ( ( om 
^o  x )  .o  y )  +o  ( om  ^o  C ) )  =  ( ( ( om  ^o  x )  .o  y )  +o  ( ( om  ^o  x )  .o  om ) ) )
8481, 83, 823eqtr4d 2446 . . . . . . . . . . . . 13  |-  ( ( ( ( ( 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 3344 . . . . . . . . . . . 12  |-  ( ( ( ( ( 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 ) )
8658, 85rexlimddv 2794 . . . . . . . . . . 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
) )  C_  ( om  ^o  C ) )
87 oaword2 6755 . . . . . . . . . . . . 13  |-  ( ( ( om  ^o  C
)  e.  On  /\  A  e.  On )  ->  ( om  ^o  C
)  C_  ( A  +o  ( om  ^o  C
) ) )
889, 18, 87syl2anc 643 . . . . . . . . . . . 12  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  ( om  ^o  C )  C_  ( A  +o  ( om  ^o  C ) ) )
8988adantr 452 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) ) )
9086, 89eqssd 3325 . . . . . . . . . 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 ) )
9190rexlimdvaa 2791 . . . . . . . . 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
) ) )
92 simplll 735 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  ->  A  e.  ( om  ^o  C ) )
9331adantr 452 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  ->  om  e.  On )
9424adantr 452 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  ->  C  e.  On )
95 simpr 448 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  ->  Lim  C )
96 oelim2 6797 . . . . . . . . . . . . . . 15  |-  ( ( om  e.  On  /\  ( C  e.  On  /\ 
Lim  C ) )  ->  ( om  ^o  C )  =  U_ x  e.  ( C  \  1o ) ( om 
^o  x ) )
9793, 94, 95, 96syl12anc 1182 . . . . . . . . . . . . . 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 ) )
9892, 97eleqtrd 2480 . . . . . . . . . . . . 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 ) )
99 eliun 4057 . . . . . . . . . . . . 13  |-  ( A  e.  U_ x  e.  ( C  \  1o ) ( om  ^o  x )  <->  E. x  e.  ( C  \  1o ) A  e.  ( om  ^o  x ) )
10098, 99sylib 189 . . . . . . . . . . . 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 ) )
101 eldifi 3429 . . . . . . . . . . . . . 14  |-  ( x  e.  ( C  \  1o )  ->  x  e.  C )
10218ad2antrr 707 . . . . . . . . . . . . . . . . 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 )
1039ad2antrr 707 . . . . . . . . . . . . . . . . 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 )
10493adantr 452 . . . . . . . . . . . . . . . . . . 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 )
105 1onn 6841 . . . . . . . . . . . . . . . . . . . 20  |-  1o  e.  om
106105a1i 11 . . . . . . . . . . . . . . . . . . 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 )
107 ondif2 6705 . . . . . . . . . . . . . . . . . . 19  |-  ( om  e.  ( On  \  2o )  <->  ( om  e.  On  /\  1o  e.  om ) )
108104, 106, 107sylanbrc 646 . . . . . . . . . . . . . . . . . 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 ) )
10994adantr 452 . . . . . . . . . . . . . . . . . 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 )
110 simplr 732 . . . . . . . . . . . . . . . . . 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 )
111 oelimcl 6802 . . . . . . . . . . . . . . . . . 18  |-  ( ( om  e.  ( On 
\  2o )  /\  ( C  e.  On  /\ 
Lim  C ) )  ->  Lim  ( om  ^o  C ) )
112108, 109, 110, 111syl12anc 1182 . . . . . . . . . . . . . . . . 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
) )
113 oalim 6735 . . . . . . . . . . . . . . . . 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 ) )
114102, 103, 112, 113syl12anc 1182 . . . . . . . . . . . . . . . 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 ) )
115 oelim2 6797 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( om  e.  On  /\  ( C  e.  On  /\ 
Lim  C ) )  ->  ( om  ^o  C )  =  U_ z  e.  ( C  \  1o ) ( om 
^o  z ) )
11693, 94, 95, 115syl12anc 1182 . . . . . . . . . . . . . . . . . . . . . 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 ) )
117116eleq2d 2471 . . . . . . . . . . . . . . . . . . . . 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 ) ) )
118 eliun 4057 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  U_ z  e.  ( C  \  1o ) ( om  ^o  z )  <->  E. z  e.  ( C  \  1o ) y  e.  ( om  ^o  z ) )
119117, 118syl6bb 253 . . . . . . . . . . . . . . . . . . . 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 ) ) )
120119adantr 452 . . . . . . . . . . . . . . . . . . 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 ) ) )
121 eldifi 3429 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  e.  ( C  \  1o )  ->  z  e.  C )
122104adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
123109adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
124 simplrl 737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
125 onelon 4566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( C  e.  On  /\  x  e.  C )  ->  x  e.  On )
126123, 124, 125syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
127122, 126, 46syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
128 eloni 4551 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( om  ^o  x )  e.  On  ->  Ord  ( om  ^o  x ) )
129127, 128syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) )
130 simplrr 738 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
131 ordelss 4557 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( Ord  ( om  ^o  x )  /\  A  e.  ( om  ^o  x
) )  ->  A  C_  ( om  ^o  x
) )
132129, 130, 131syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
133 ssun1 3470 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  x  C_  ( x  u.  z
)
13426ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
135 simprl 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
136 ordunel 4766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( Ord  C  /\  x  e.  C  /\  z  e.  C )  ->  (
x  u.  z )  e.  C )
137134, 124, 135, 136syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
138 onelon 4566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( C  e.  On  /\  ( x  u.  z
)  e.  C )  ->  ( x  u.  z )  e.  On )
139123, 137, 138syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
140 peano1 4823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  (/)  e.  om
141140a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
142 oewordi 6793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
143126, 139, 122, 141, 142syl31anc 1187 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
144133, 143mpi 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
145132, 144sstrd 3318 . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
146102adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
147 oecl 6740 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( om  e.  On  /\  ( x  u.  z
)  e.  On )  ->  ( om  ^o  ( x  u.  z
) )  e.  On )
148122, 139, 147syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
149 onelon 4566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( C  e.  On  /\  z  e.  C )  ->  z  e.  On )
150123, 135, 149syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
151 oecl 6740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( om  e.  On  /\  z  e.  On )  ->  ( om  ^o  z
)  e.  On )
152122, 150, 151syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
153 simprr 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
154 onelon 4566 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( om  ^o  z
)  e.  On  /\  y  e.  ( om  ^o  z ) )  -> 
y  e.  On )
155152, 153, 154syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
156 oawordri 6752 . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
157146, 148, 155, 156syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
158145, 157mpd 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
) ) )  -> 
( A  +o  y
)  C_  ( ( om  ^o  ( x  u.  z ) )  +o  y ) )
159 eloni 4551 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( om  ^o  z )  e.  On  ->  Ord  ( om  ^o  z ) )
160152, 159syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) )
161 ordelss 4557 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( Ord  ( om  ^o  z )  /\  y  e.  ( om  ^o  z
) )  ->  y  C_  ( om  ^o  z
) )
162160, 153, 161syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
163 ssun2 3471 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  z  C_  ( x  u.  z
)
164 oewordi 6793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
165150, 139, 122, 141, 164syl31anc 1187 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
166163, 165mpi 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
167162, 166sstrd 3318 . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
168 oaword 6751 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
169155, 148, 148, 168syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
170167, 169mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
171158, 170sstrd 3318 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
172 ordom 4813 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  Ord  om
173 ordsucss 4757 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( Ord 
om  ->  ( 1o  e.  om 
->  suc  1o  C_  om )
)
174172, 105, 173mp2 9 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  suc  1o  C_ 
om
175 1on 6690 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  1o  e.  On
176 suceloni 4752 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 1o  e.  On  ->  suc  1o  e.  On )
177175, 176mp1i 12 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
178 omwordi 6773 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
179177, 122, 148, 178syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
180174, 179mpi 17 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
181175a1i 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
) ) )  ->  1o  e.  On )
182 omsuc 6729 . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
183148, 181, 182syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
184 om1 6744 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( om  ^o  ( x  u.  z ) )  e.  On  ->  (
( om  ^o  (
x  u.  z ) )  .o  1o )  =  ( om  ^o  ( x  u.  z
) ) )
185148, 184syl 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  u.  z
) )  .o  1o )  =  ( om  ^o  ( x  u.  z
) ) )
186185oveq1d 6055 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
187183, 186eqtr2d 2437 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
188 oesuc 6730 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( om  e.  On  /\  ( x  u.  z
)  e.  On )  ->  ( om  ^o  suc  ( x  u.  z
) )  =  ( ( om  ^o  (
x  u.  z ) )  .o  om )
)
189122, 139, 188syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
)
190180, 187, 1893sstr4d 3351 . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
191171, 190sstrd 3318 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
192 ordsucss 4757 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( Ord 
C  ->  ( (
x  u.  z )  e.  C  ->  suc  ( x  u.  z
)  C_  C )
)
193134, 137, 192sylc 58 . . . . . . . . . . . . . . . . . . . . . . . 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 )
194 suceloni 4752 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  u.  z )  e.  On  ->  suc  ( x  u.  z
)  e.  On )
195139, 194syl 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
) ) )  ->  suc  ( x  u.  z
)  e.  On )
196 oewordi 6793 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
197195, 123, 122, 141, 196syl31anc 1187 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
198193, 197mpd 15 . . . . . . . . . . . . . . . . . . . . . . 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 ) )
199191, 198sstrd 3318 . . . . . . . . . . . . . . . . . . . . . 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 ) )
200199expr 599 . . . . . . . . . . . . . . . . . . . . 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 ) ) )
201121, 200sylan2 461 . . . . . . . . . . . . . . . . . . . 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 ) ) )
202201rexlimdva 2790 . . . . . . . . . . . . . . . . . . 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 ) ) )
203120, 202sylbid 207 . . . . . . . . . . . . . . . . . 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 ) ) )
204203ralrimiv 2748 . . . . . . . . . . . . . . . . 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 ) )
205 iunss 4092 . . . . . . . . . . . . . . . . 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 ) )
206204, 205sylibr 204 . . . . . . . . . . . . . . . 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 ) )
207114, 206eqsstrd 3342 . . . . . . . . . . . . . . 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 ) )
208207expr 599 . . . . . . . . . . . . . 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 ) ) )
209101, 208sylan2 461 . . . . . . . . . . . . 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 ) ) )
210209rexlimdva 2790 . . . . . . . . . . . 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 ) ) )
211100, 210mpd 15 . . . . . . . . . . 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 ) )
21288adantr 452 . . . . . . . . . . 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 ) ) )
213211, 212eqssd 3325 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  Lim  C )  ->  ( A  +o  ( om  ^o  C
) )  =  ( om  ^o  C ) )
214213ex 424 . . . . . . . . 9  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  ( Lim  C  ->  ( A  +o  ( om  ^o  C ) )  =  ( om 
^o  C ) ) )
21543, 91, 2143jaod 1248 . . . . . . . 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 ) ) )
21628, 215mpd 15 . . . . . . 7  |-  ( ( ( A  e.  ( om  ^o  C )  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B
)  ->  ( A  +o  ( om  ^o  C
) )  =  ( om  ^o  C ) )
217216adantr 452 . . . . . 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
) )
218217oveq1d 6055 . . . . 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
) )
21923, 218eqtr3d 2438 . . . 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
) )
220 oveq2 6048 . . . . 5  |-  ( ( ( om  ^o  C
)  +o  x )  =  B  ->  ( A  +o  ( ( om 
^o  C )  +o  x ) )  =  ( A  +o  B
) )
221 id 20 . . . . 5  |-  ( ( ( om  ^o  C
)  +o  x )  =  B  ->  (
( om  ^o  C
)  +o  x )  =  B )
222220, 221eqeq12d 2418 . . . 4  |-  ( ( ( om  ^o  C
)  +o  x )  =  B  ->  (
( A  +o  (
( om  ^o  C
)  +o  x ) )  =  ( ( om  ^o  C )  +o  x )  <->  ( A  +o  B )  =  B ) )
223219, 222syl5ibcom 212 . . 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 ) )
224223rexlimdva 2790 . 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 ) )
22515, 224mpd 15 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 177    /\ wa 359    \/ w3o 935    = wceq 1649    e. wcel 1721   A.wral 2666   E.wrex 2667   E!wreu 2668    \ cdif 3277    u. cun 3278    C_ wss 3280   (/)c0 3588   U_ciun 4053   Ord word 4540   Oncon0 4541   Lim wlim 4542   suc csuc 4543   omcom 4804    X. cxp 4835   dom cdm 4837    Fn wfn 5408  (class class class)co 6040   1oc1o 6676   2oc2o 6677    +o coa 6680    .o comu 6681    ^o coe 6682
This theorem is referenced by:  cnfcomlem  7612
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-recs 6592  df-rdg 6627  df-1o 6683  df-2o 6684  df-oadd 6687  df-omul 6688  df-oexp 6689
  Copyright terms: Public domain W3C validator