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

Theorem oaabs2 6881
Description: The absorption law oaabs 6880 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 3626 . . . . . . 7  |-  ( A  e.  ( om  ^o  C )  ->  -.  ( om  ^o  C )  =  (/) )
2 fnoe 6747 . . . . . . . . 9  |-  ^o  Fn  ( On  X.  On )
3 fndm 5537 . . . . . . . . 9  |-  (  ^o  Fn  ( On  X.  On )  ->  dom  ^o  =  ( On  X.  On ) )
42, 3ax-mp 8 . . . . . . . 8  |-  dom  ^o  =  ( On  X.  On )
54ndmov 6224 . . . . . . 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 6774 . . . . 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 6791 . . . 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 2915 . . 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 4599 . . . . . . . 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 6797 . . . . . 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 4584 . . . . . . . . . 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 4818 . . . . . . . . 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 6082 . . . . . . . . . . . . . . 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 6759 . . . . . . . . . . . . . . . 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 2490 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  C  =  (/) )  ->  ( om  ^o  C )  =  1o )
3529, 34eleqtrd 2512 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  ( om  ^o  C
)  /\  B  e.  On )  /\  ( om  ^o  C )  C_  B )  /\  C  =  (/) )  ->  A  e.  1o )
36 el1o 6736 . . . . . . . . . . . . 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 6089 . . . . . . . . . . 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 6775 . . . . . . . . . . . 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 2468 . . . . . . . . . 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 6774 . . . . . . . . . . . . . 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 4853 . . . . . . . . . . . . . 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 6090 . . . . . . . . . . . . . . 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 6764 . . . . . . . . . . . . . . . 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 2468 . . . . . . . . . . . . . 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 2512 . . . . . . . . . . . . 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 6813 . . . . . . . . . . . . 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 4844 . . . . . . . . . . . . . . . . . 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 6773 . . . . . . . . . . . . . . . . 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 4584 . . . . . . . . . . . . . . . 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 4590 . . . . . . . . . . . . . . 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 6786 . . . . . . . . . . . . . . 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 6815 . . . . . . . . . . . . . . . 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 6879 . . . . . . . . . . . . . . . . 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 6090 . . . . . . . . . . . . . . 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 2470 . . . . . . . . . . . . . 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 6090 . . . . . . . . . . . . . 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 2478 . . . . . . . . . . . . 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 3377 . . . . . . . . . . . 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 2827 . . . . . . . . . . 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 6789 . . . . . . . . . . . . 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 3358 . . . . . . . . . 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 2824 . . . . . . . . 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 6831 . . . . . . . . . . . . . . 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 2512 . . . . . . . . . . . . 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 4090 . . . . . . . . . . . . 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 3462 . . . . . . . . . . . . . 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 6875 . . . . . . . . . . . . . . . . . . . 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 6739 . . . . . . . . . . . . . . . . . . 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 6836 . . . . . . . . . . . . . . . . . 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 6769 . . . . . . . . . . . . . . . . 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 6831 . . . . . . . . . . . . . . . . . . . . . . 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 2503 . . . . . . . . . . . . . . . . . . . . 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 4090 . . . . . . . . . . . . . . . . . . . . 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 3462 . . . . . . . . . . . . . . . . . . . . 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 4599 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4590 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3503 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4599 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4857 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3351 . . . . . . . . . . . . . . . . . . . . . . . . . 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 6774 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4599 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4599 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6786 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4590 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3504 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  z  C_  ( x  u.  z
)
164 oewordi 6827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3351 . . . . . . . . . . . . . . . . . . . . . . . . . 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 6785 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 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
) ) )  -> 
( A  +o  y
)  C_  ( ( om  ^o  ( x  u.  z ) )  +o  ( om  ^o  (
x  u.  z ) ) ) )
172 ordom 4847 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  Ord  om
173 ordsucss 4791 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( Ord 
om  ->  ( 1o  e.  om 
->  suc  1o  C_  om )
)
174172, 105, 173mp2 9 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  suc  1o  C_ 
om
175 1on 6724 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  1o  e.  On
176 suceloni 4786 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6807 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6763 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6778 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6089 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2469 . . . . . . . . . . . . . . . . . . . . . . . . 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 6764 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3384 . . . . . . . . . . . . . . . . . . . . . . . 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 3351 . . . . . . . . . . . . . . . . . . . . . . 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 4791 . . . . . . . . . . . . . . . . . . . . . . . . 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 4786 . . . . . . . . . . . . . . . . . . . . . . . . . 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 6827 . . . . . . . . . . . . . . . . . . . . . . . . 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 3351 . . . . . . . . . . . . . . . . . . . . . 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 2823 . . . . . . . . . . . . . . . . . . 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 2781 . . . . . . . . . . . . . . . . 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 4125 . . . . . . . . . . . . . . . . 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 3375 . . . . . . . . . . . . . . 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 2823 . . . . . . . . . . . 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 3358 . . . . . . . . . 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 6089 . . . . 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 2470 . . . 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 6082 . . . . 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 2450 . . . 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 2823 . 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 1652    e. wcel 1725   A.wral 2698   E.wrex 2699   E!wreu 2700    \ cdif 3310    u. cun 3311    C_ wss 3313   (/)c0 3621   U_ciun 4086   Ord word 4573   Oncon0 4574   Lim wlim 4575   suc csuc 4576   omcom 4838    X. cxp 4869   dom cdm 4871    Fn wfn 5442  (class class class)co 6074   1oc1o 6710   2oc2o 6711    +o coa 6714    .o comu 6715    ^o coe 6716
This theorem is referenced by:  cnfcomlem  7649
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-rep 4313  ax-sep 4323  ax-nul 4331  ax-pow 4370  ax-pr 4396  ax-un 4694
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2703  df-rex 2704  df-reu 2705  df-rmo 2706  df-rab 2707  df-v 2951  df-sbc 3155  df-csb 3245  df-dif 3316  df-un 3318  df-in 3320  df-ss 3327  df-pss 3329  df-nul 3622  df-if 3733  df-pw 3794  df-sn 3813  df-pr 3814  df-tp 3815  df-op 3816  df-uni 4009  df-int 4044  df-iun 4088  df-br 4206  df-opab 4260  df-mpt 4261  df-tr 4296  df-eprel 4487  df-id 4491  df-po 4496  df-so 4497  df-fr 4534  df-we 4536  df-ord 4577  df-on 4578  df-lim 4579  df-suc 4580  df-om 4839  df-xp 4877  df-rel 4878  df-cnv 4879  df-co 4880  df-dm 4881  df-rn 4882  df-res 4883  df-ima 4884  df-iota 5411  df-fun 5449  df-fn 5450  df-f 5451  df-f1 5452  df-fo 5453  df-f1o 5454  df-fv 5455  df-ov 6077  df-oprab 6078  df-mpt2 6079  df-1st 6342  df-2nd 6343  df-recs 6626  df-rdg 6661  df-1o 6717  df-2o 6718  df-oadd 6721  df-omul 6722  df-oexp 6723
  Copyright terms: Public domain W3C validator