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

Theorem omabs 6849
Description: Ordinal multiplication is also absorbed by powers of  om. (Contributed by Mario Carneiro, 30-May-2015.)
Assertion
Ref Expression
omabs  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( B  e.  On  /\  (/)  e.  B ) )  ->  ( A  .o  ( om  ^o  B ) )  =  ( om 
^o  B ) )

Proof of Theorem omabs
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eleq2 2465 . . . . . . . 8  |-  ( x  =  (/)  ->  ( (/)  e.  x  <->  (/)  e.  (/) ) )
2 oveq2 6048 . . . . . . . . . 10  |-  ( x  =  (/)  ->  ( om 
^o  x )  =  ( om  ^o  (/) ) )
32oveq2d 6056 . . . . . . . . 9  |-  ( x  =  (/)  ->  ( A  .o  ( om  ^o  x ) )  =  ( A  .o  ( om  ^o  (/) ) ) )
43, 2eqeq12d 2418 . . . . . . . 8  |-  ( x  =  (/)  ->  ( ( A  .o  ( om 
^o  x ) )  =  ( om  ^o  x )  <->  ( A  .o  ( om  ^o  (/) ) )  =  ( om  ^o  (/) ) ) )
51, 4imbi12d 312 . . . . . . 7  |-  ( x  =  (/)  ->  ( (
(/)  e.  x  ->  ( A  .o  ( om 
^o  x ) )  =  ( om  ^o  x ) )  <->  ( (/)  e.  (/)  ->  ( A  .o  ( om  ^o  (/) ) )  =  ( om  ^o  (/) ) ) ) )
6 eleq2 2465 . . . . . . . 8  |-  ( x  =  y  ->  ( (/) 
e.  x  <->  (/)  e.  y ) )
7 oveq2 6048 . . . . . . . . . 10  |-  ( x  =  y  ->  ( om  ^o  x )  =  ( om  ^o  y
) )
87oveq2d 6056 . . . . . . . . 9  |-  ( x  =  y  ->  ( A  .o  ( om  ^o  x ) )  =  ( A  .o  ( om  ^o  y ) ) )
98, 7eqeq12d 2418 . . . . . . . 8  |-  ( x  =  y  ->  (
( A  .o  ( om  ^o  x ) )  =  ( om  ^o  x )  <->  ( A  .o  ( om  ^o  y
) )  =  ( om  ^o  y ) ) )
106, 9imbi12d 312 . . . . . . 7  |-  ( x  =  y  ->  (
( (/)  e.  x  -> 
( A  .o  ( om  ^o  x ) )  =  ( om  ^o  x ) )  <->  ( (/)  e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om 
^o  y ) ) ) )
11 eleq2 2465 . . . . . . . 8  |-  ( x  =  suc  y  -> 
( (/)  e.  x  <->  (/)  e.  suc  y ) )
12 oveq2 6048 . . . . . . . . . 10  |-  ( x  =  suc  y  -> 
( om  ^o  x
)  =  ( om 
^o  suc  y )
)
1312oveq2d 6056 . . . . . . . . 9  |-  ( x  =  suc  y  -> 
( A  .o  ( om  ^o  x ) )  =  ( A  .o  ( om  ^o  suc  y
) ) )
1413, 12eqeq12d 2418 . . . . . . . 8  |-  ( x  =  suc  y  -> 
( ( A  .o  ( om  ^o  x ) )  =  ( om 
^o  x )  <->  ( A  .o  ( om  ^o  suc  y ) )  =  ( om  ^o  suc  y ) ) )
1511, 14imbi12d 312 . . . . . . 7  |-  ( x  =  suc  y  -> 
( ( (/)  e.  x  ->  ( A  .o  ( om  ^o  x ) )  =  ( om  ^o  x ) )  <->  ( (/)  e.  suc  y  ->  ( A  .o  ( om  ^o  suc  y
) )  =  ( om  ^o  suc  y
) ) ) )
16 eleq2 2465 . . . . . . . 8  |-  ( x  =  B  ->  ( (/) 
e.  x  <->  (/)  e.  B
) )
17 oveq2 6048 . . . . . . . . . 10  |-  ( x  =  B  ->  ( om  ^o  x )  =  ( om  ^o  B
) )
1817oveq2d 6056 . . . . . . . . 9  |-  ( x  =  B  ->  ( A  .o  ( om  ^o  x ) )  =  ( A  .o  ( om  ^o  B ) ) )
1918, 17eqeq12d 2418 . . . . . . . 8  |-  ( x  =  B  ->  (
( A  .o  ( om  ^o  x ) )  =  ( om  ^o  x )  <->  ( A  .o  ( om  ^o  B
) )  =  ( om  ^o  B ) ) )
2016, 19imbi12d 312 . . . . . . 7  |-  ( x  =  B  ->  (
( (/)  e.  x  -> 
( A  .o  ( om  ^o  x ) )  =  ( om  ^o  x ) )  <->  ( (/)  e.  B  ->  ( A  .o  ( om  ^o  B ) )  =  ( om  ^o  B ) ) ) )
21 noel 3592 . . . . . . . . 9  |-  -.  (/)  e.  (/)
2221pm2.21i 125 . . . . . . . 8  |-  ( (/)  e.  (/)  ->  ( A  .o  ( om  ^o  (/) ) )  =  ( om  ^o  (/) ) )
2322a1i 11 . . . . . . 7  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  om  e.  On )  -> 
( (/)  e.  (/)  ->  ( A  .o  ( om  ^o  (/) ) )  =  ( om  ^o  (/) ) ) )
24 simprl 733 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  om  e.  On )
25 simpll 731 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  A  e.  om )
26 simplr 732 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  (/)  e.  A
)
27 omabslem 6848 . . . . . . . . . . . . . . . 16  |-  ( ( om  e.  On  /\  A  e.  om  /\  (/)  e.  A
)  ->  ( A  .o  om )  =  om )
2824, 25, 26, 27syl3anc 1184 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  ( A  .o  om )  =  om )
2928adantr 452 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  y  e.  On ) )  /\  y  =  (/) )  -> 
( A  .o  om )  =  om )
30 suceq 4606 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  (/)  ->  suc  y  =  suc  (/) )
31 df-1o 6683 . . . . . . . . . . . . . . . . . 18  |-  1o  =  suc  (/)
3230, 31syl6eqr 2454 . . . . . . . . . . . . . . . . 17  |-  ( y  =  (/)  ->  suc  y  =  1o )
3332oveq2d 6056 . . . . . . . . . . . . . . . 16  |-  ( y  =  (/)  ->  ( om 
^o  suc  y )  =  ( om  ^o  1o ) )
34 oe1 6746 . . . . . . . . . . . . . . . . 17  |-  ( om  e.  On  ->  ( om  ^o  1o )  =  om )
3534ad2antrl 709 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  ( om  ^o  1o )  =  om )
3633, 35sylan9eqr 2458 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  y  e.  On ) )  /\  y  =  (/) )  -> 
( om  ^o  suc  y )  =  om )
3736oveq2d 6056 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  y  e.  On ) )  /\  y  =  (/) )  -> 
( A  .o  ( om  ^o  suc  y ) )  =  ( A  .o  om ) )
3829, 37, 363eqtr4d 2446 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  y  e.  On ) )  /\  y  =  (/) )  -> 
( A  .o  ( om  ^o  suc  y ) )  =  ( om 
^o  suc  y )
)
3938ex 424 . . . . . . . . . . . 12  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  ( y  =  (/)  ->  ( A  .o  ( om  ^o  suc  y ) )  =  ( om  ^o  suc  y ) ) )
4039a1dd 44 . . . . . . . . . . 11  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  ( y  =  (/)  ->  ( ( (/) 
e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y
) )  ->  ( A  .o  ( om  ^o  suc  y ) )  =  ( om  ^o  suc  y ) ) ) )
41 oveq1 6047 . . . . . . . . . . . . . 14  |-  ( ( A  .o  ( om 
^o  y ) )  =  ( om  ^o  y )  ->  (
( A  .o  ( om  ^o  y ) )  .o  om )  =  ( ( om  ^o  y )  .o  om ) )
42 oesuc 6730 . . . . . . . . . . . . . . . . . 18  |-  ( ( om  e.  On  /\  y  e.  On )  ->  ( om  ^o  suc  y )  =  ( ( om  ^o  y
)  .o  om )
)
4342adantl 453 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  ( om  ^o 
suc  y )  =  ( ( om  ^o  y )  .o  om ) )
4443oveq2d 6056 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  ( A  .o  ( om  ^o  suc  y ) )  =  ( A  .o  (
( om  ^o  y
)  .o  om )
) )
45 nnon 4810 . . . . . . . . . . . . . . . . . 18  |-  ( A  e.  om  ->  A  e.  On )
4645ad2antrr 707 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  A  e.  On )
47 oecl 6740 . . . . . . . . . . . . . . . . . 18  |-  ( ( om  e.  On  /\  y  e.  On )  ->  ( om  ^o  y
)  e.  On )
4847adantl 453 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  ( om  ^o  y )  e.  On )
49 omass 6782 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  On  /\  ( om  ^o  y )  e.  On  /\  om  e.  On )  ->  (
( A  .o  ( om  ^o  y ) )  .o  om )  =  ( A  .o  (
( om  ^o  y
)  .o  om )
) )
5046, 48, 24, 49syl3anc 1184 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  ( ( A  .o  ( om  ^o  y ) )  .o 
om )  =  ( A  .o  ( ( om  ^o  y )  .o  om ) ) )
5144, 50eqtr4d 2439 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  ( A  .o  ( om  ^o  suc  y ) )  =  ( ( A  .o  ( om  ^o  y ) )  .o  om )
)
5251, 43eqeq12d 2418 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  ( ( A  .o  ( om  ^o  suc  y ) )  =  ( om  ^o  suc  y )  <->  ( ( A  .o  ( om  ^o  y ) )  .o 
om )  =  ( ( om  ^o  y
)  .o  om )
) )
5341, 52syl5ibr 213 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  ( ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y
)  ->  ( A  .o  ( om  ^o  suc  y ) )  =  ( om  ^o  suc  y ) ) )
5453imim2d 50 . . . . . . . . . . . 12  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  ( ( (/) 
e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y
) )  ->  ( (/) 
e.  y  ->  ( A  .o  ( om  ^o  suc  y ) )  =  ( om  ^o  suc  y ) ) ) )
5554com23 74 . . . . . . . . . . 11  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  ( (/)  e.  y  ->  ( ( (/)  e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y
) )  ->  ( A  .o  ( om  ^o  suc  y ) )  =  ( om  ^o  suc  y ) ) ) )
56 simprr 734 . . . . . . . . . . . 12  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  y  e.  On )
57 on0eqel 4658 . . . . . . . . . . . 12  |-  ( y  e.  On  ->  (
y  =  (/)  \/  (/)  e.  y ) )
5856, 57syl 16 . . . . . . . . . . 11  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  ( y  =  (/)  \/  (/)  e.  y ) )
5940, 55, 58mpjaod 371 . . . . . . . . . 10  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  ( ( (/) 
e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y
) )  ->  ( A  .o  ( om  ^o  suc  y ) )  =  ( om  ^o  suc  y ) ) )
6059a1dd 44 . . . . . . . . 9  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  ( ( (/) 
e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y
) )  ->  ( (/) 
e.  suc  y  ->  ( A  .o  ( om 
^o  suc  y )
)  =  ( om 
^o  suc  y )
) ) )
6160anassrs 630 . . . . . . . 8  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  om  e.  On )  /\  y  e.  On )  ->  (
( (/)  e.  y  -> 
( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y ) )  -> 
( (/)  e.  suc  y  ->  ( A  .o  ( om  ^o  suc  y ) )  =  ( om 
^o  suc  y )
) ) )
6261expcom 425 . . . . . . 7  |-  ( y  e.  On  ->  (
( ( A  e. 
om  /\  (/)  e.  A
)  /\  om  e.  On )  ->  ( (
(/)  e.  y  ->  ( A  .o  ( om 
^o  y ) )  =  ( om  ^o  y ) )  -> 
( (/)  e.  suc  y  ->  ( A  .o  ( om  ^o  suc  y ) )  =  ( om 
^o  suc  y )
) ) ) )
6345ad3antrrr 711 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  A. y  e.  x  ( (/) 
e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y
) ) )  ->  A  e.  On )
64 simprl 733 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  Lim  x ) )  ->  om  e.  On )
65 simprr 734 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  Lim  x ) )  ->  Lim  x )
66 vex 2919 . . . . . . . . . . . . . . . . . 18  |-  x  e. 
_V
6765, 66jctil 524 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  Lim  x ) )  -> 
( x  e.  _V  /\ 
Lim  x ) )
68 limelon 4604 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  _V  /\  Lim  x )  ->  x  e.  On )
6967, 68syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  Lim  x ) )  ->  x  e.  On )
70 oecl 6740 . . . . . . . . . . . . . . . 16  |-  ( ( om  e.  On  /\  x  e.  On )  ->  ( om  ^o  x
)  e.  On )
7164, 69, 70syl2anc 643 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  Lim  x ) )  -> 
( om  ^o  x
)  e.  On )
7271adantr 452 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  A. y  e.  x  ( (/) 
e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y
) ) )  -> 
( om  ^o  x
)  e.  On )
73 1onn 6841 . . . . . . . . . . . . . . . . . 18  |-  1o  e.  om
7473a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  Lim  x ) )  ->  1o  e.  om )
75 ondif2 6705 . . . . . . . . . . . . . . . . 17  |-  ( om  e.  ( On  \  2o )  <->  ( om  e.  On  /\  1o  e.  om ) )
7664, 74, 75sylanbrc 646 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  Lim  x ) )  ->  om  e.  ( On  \  2o ) )
7776adantr 452 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  A. y  e.  x  ( (/) 
e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y
) ) )  ->  om  e.  ( On  \  2o ) )
7867adantr 452 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  A. y  e.  x  ( (/) 
e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y
) ) )  -> 
( x  e.  _V  /\ 
Lim  x ) )
79 oelimcl 6802 . . . . . . . . . . . . . . 15  |-  ( ( om  e.  ( On 
\  2o )  /\  ( x  e.  _V  /\ 
Lim  x ) )  ->  Lim  ( om  ^o  x ) )
8077, 78, 79syl2anc 643 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  A. y  e.  x  ( (/) 
e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y
) ) )  ->  Lim  ( om  ^o  x
) )
81 omlim 6736 . . . . . . . . . . . . . 14  |-  ( ( A  e.  On  /\  ( ( om  ^o  x )  e.  On  /\ 
Lim  ( om  ^o  x ) ) )  ->  ( A  .o  ( om  ^o  x ) )  =  U_ z  e.  ( om  ^o  x
) ( A  .o  z ) )
8263, 72, 80, 81syl12anc 1182 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  A. y  e.  x  ( (/) 
e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y
) ) )  -> 
( A  .o  ( om  ^o  x ) )  =  U_ z  e.  ( om  ^o  x
) ( A  .o  z ) )
83 simplrl 737 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  A. y  e.  x  ( (/) 
e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y
) ) )  ->  om  e.  On )
84 oelim2 6797 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( om  e.  On  /\  ( x  e.  _V  /\ 
Lim  x ) )  ->  ( om  ^o  x )  =  U_ y  e.  ( x  \  1o ) ( om 
^o  y ) )
8583, 78, 84syl2anc 643 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  A. y  e.  x  ( (/) 
e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y
) ) )  -> 
( om  ^o  x
)  =  U_ y  e.  ( x  \  1o ) ( om  ^o  y ) )
8685eleq2d 2471 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  A. y  e.  x  ( (/) 
e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y
) ) )  -> 
( z  e.  ( om  ^o  x )  <-> 
z  e.  U_ y  e.  ( x  \  1o ) ( om  ^o  y ) ) )
87 eliun 4057 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  U_ y  e.  ( x  \  1o ) ( om  ^o  y )  <->  E. y  e.  ( x  \  1o ) z  e.  ( om  ^o  y ) )
8886, 87syl6bb 253 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  A. y  e.  x  ( (/) 
e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y
) ) )  -> 
( z  e.  ( om  ^o  x )  <->  E. y  e.  (
x  \  1o )
z  e.  ( om 
^o  y ) ) )
8969adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  A. y  e.  x  ( (/) 
e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y
) ) )  ->  x  e.  On )
90 anass 631 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( y  e.  x  /\  (/)  e.  y )  /\  z  e.  ( om  ^o  y ) )  <->  ( y  e.  x  /\  ( (/)  e.  y  /\  z  e.  ( om  ^o  y
) ) ) )
91 onelon 4566 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  On  /\  y  e.  x )  ->  y  e.  On )
92 on0eln0 4596 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  On  ->  ( (/) 
e.  y  <->  y  =/=  (/) ) )
9391, 92syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  On  /\  y  e.  x )  ->  ( (/)  e.  y  <->  y  =/=  (/) ) )
9493pm5.32da 623 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  On  ->  (
( y  e.  x  /\  (/)  e.  y )  <-> 
( y  e.  x  /\  y  =/=  (/) ) ) )
95 dif1o 6703 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  ( x  \  1o )  <->  ( y  e.  x  /\  y  =/=  (/) ) )
9694, 95syl6bbr 255 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  On  ->  (
( y  e.  x  /\  (/)  e.  y )  <-> 
y  e.  ( x 
\  1o ) ) )
9796anbi1d 686 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  On  ->  (
( ( y  e.  x  /\  (/)  e.  y )  /\  z  e.  ( om  ^o  y
) )  <->  ( y  e.  ( x  \  1o )  /\  z  e.  ( om  ^o  y ) ) ) )
9890, 97syl5bbr 251 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  On  ->  (
( y  e.  x  /\  ( (/)  e.  y  /\  z  e.  ( om  ^o  y ) ) )  <->  ( y  e.  ( x  \  1o )  /\  z  e.  ( om  ^o  y ) ) ) )
9998rexbidv2 2689 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  On  ->  ( E. y  e.  x  ( (/)  e.  y  /\  z  e.  ( om  ^o  y ) )  <->  E. y  e.  ( x  \  1o ) z  e.  ( om  ^o  y ) ) )
10089, 99syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  A. y  e.  x  ( (/) 
e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y
) ) )  -> 
( E. y  e.  x  ( (/)  e.  y  /\  z  e.  ( om  ^o  y ) )  <->  E. y  e.  ( x  \  1o ) z  e.  ( om 
^o  y ) ) )
10188, 100bitr4d 248 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  A. y  e.  x  ( (/) 
e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y
) ) )  -> 
( z  e.  ( om  ^o  x )  <->  E. y  e.  x  ( (/)  e.  y  /\  z  e.  ( om  ^o  y ) ) ) )
102 r19.29 2806 . . . . . . . . . . . . . . . . . 18  |-  ( ( A. y  e.  x  ( (/)  e.  y  -> 
( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y ) )  /\  E. y  e.  x  (
(/)  e.  y  /\  z  e.  ( om  ^o  y ) ) )  ->  E. y  e.  x  ( ( (/)  e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om 
^o  y ) )  /\  ( (/)  e.  y  /\  z  e.  ( om  ^o  y ) ) ) )
103 id 20 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
(/)  e.  y  ->  ( A  .o  ( om 
^o  y ) )  =  ( om  ^o  y ) )  -> 
( (/)  e.  y  -> 
( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y ) ) )
104103imp 419 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( (/)  e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y ) )  /\  (/) 
e.  y )  -> 
( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y ) )
105104anim1i 552 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( (/)  e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om 
^o  y ) )  /\  (/)  e.  y )  /\  z  e.  ( om  ^o  y ) )  ->  ( ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y
)  /\  z  e.  ( om  ^o  y ) ) )
106105anasss 629 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( (/)  e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y ) )  /\  ( (/)  e.  y  /\  z  e.  ( om  ^o  y ) ) )  ->  ( ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y
)  /\  z  e.  ( om  ^o  y ) ) )
10771ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( A  e.  om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  y  e.  x )  /\  (
( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y )  /\  z  e.  ( om  ^o  y
) ) )  -> 
( om  ^o  x
)  e.  On )
108 eloni 4551 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( om  ^o  x )  e.  On  ->  Ord  ( om  ^o  x ) )
109107, 108syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( A  e.  om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  y  e.  x )  /\  (
( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y )  /\  z  e.  ( om  ^o  y
) ) )  ->  Ord  ( om  ^o  x
) )
110 simprr 734 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( A  e.  om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  y  e.  x )  /\  (
( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y )  /\  z  e.  ( om  ^o  y
) ) )  -> 
z  e.  ( om 
^o  y ) )
11164ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( A  e.  om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  y  e.  x )  /\  (
( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y )  /\  z  e.  ( om  ^o  y
) ) )  ->  om  e.  On )
11269ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( A  e.  om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  y  e.  x )  /\  (
( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y )  /\  z  e.  ( om  ^o  y
) ) )  ->  x  e.  On )
113 simplr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( A  e.  om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  y  e.  x )  /\  (
( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y )  /\  z  e.  ( om  ^o  y
) ) )  -> 
y  e.  x )
114112, 113, 91syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( A  e.  om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  y  e.  x )  /\  (
( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y )  /\  z  e.  ( om  ^o  y
) ) )  -> 
y  e.  On )
115111, 114, 47syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( A  e.  om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  y  e.  x )  /\  (
( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y )  /\  z  e.  ( om  ^o  y
) ) )  -> 
( om  ^o  y
)  e.  On )
116 onelon 4566 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( om  ^o  y
)  e.  On  /\  z  e.  ( om  ^o  y ) )  -> 
z  e.  On )
117115, 110, 116syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( A  e.  om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  y  e.  x )  /\  (
( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y )  /\  z  e.  ( om  ^o  y
) ) )  -> 
z  e.  On )
11845ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  Lim  x ) )  ->  A  e.  On )
119118ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( A  e.  om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  y  e.  x )  /\  (
( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y )  /\  z  e.  ( om  ^o  y
) ) )  ->  A  e.  On )
120 simplr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  Lim  x ) )  ->  (/) 
e.  A )
121120ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( A  e.  om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  y  e.  x )  /\  (
( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y )  /\  z  e.  ( om  ^o  y
) ) )  ->  (/) 
e.  A )
122 omord2 6769 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( z  e.  On  /\  ( om  ^o  y
)  e.  On  /\  A  e.  On )  /\  (/)  e.  A )  ->  ( z  e.  ( om  ^o  y
)  <->  ( A  .o  z )  e.  ( A  .o  ( om 
^o  y ) ) ) )
123117, 115, 119, 121, 122syl31anc 1187 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( A  e.  om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  y  e.  x )  /\  (
( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y )  /\  z  e.  ( om  ^o  y
) ) )  -> 
( z  e.  ( om  ^o  y )  <-> 
( A  .o  z
)  e.  ( A  .o  ( om  ^o  y ) ) ) )
124110, 123mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( A  e.  om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  y  e.  x )  /\  (
( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y )  /\  z  e.  ( om  ^o  y
) ) )  -> 
( A  .o  z
)  e.  ( A  .o  ( om  ^o  y ) ) )
125 simprl 733 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( A  e.  om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  y  e.  x )  /\  (
( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y )  /\  z  e.  ( om  ^o  y
) ) )  -> 
( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y ) )
126124, 125eleqtrd 2480 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( A  e.  om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  y  e.  x )  /\  (
( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y )  /\  z  e.  ( om  ^o  y
) ) )  -> 
( A  .o  z
)  e.  ( om 
^o  y ) )
12776ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( A  e.  om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  y  e.  x )  /\  (
( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y )  /\  z  e.  ( om  ^o  y
) ) )  ->  om  e.  ( On  \  2o ) )
128 oeord 6790 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( y  e.  On  /\  x  e.  On  /\  om  e.  ( On  \  2o ) )  ->  (
y  e.  x  <->  ( om  ^o  y )  e.  ( om  ^o  x ) ) )
129114, 112, 127, 128syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( A  e.  om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  y  e.  x )  /\  (
( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y )  /\  z  e.  ( om  ^o  y
) ) )  -> 
( y  e.  x  <->  ( om  ^o  y )  e.  ( om  ^o  x ) ) )
130113, 129mpbid 202 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( A  e.  om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  y  e.  x )  /\  (
( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y )  /\  z  e.  ( om  ^o  y
) ) )  -> 
( om  ^o  y
)  e.  ( om 
^o  x ) )
131 ontr1 4587 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( om  ^o  x )  e.  On  ->  (
( ( A  .o  z )  e.  ( om  ^o  y )  /\  ( om  ^o  y )  e.  ( om  ^o  x ) )  ->  ( A  .o  z )  e.  ( om  ^o  x ) ) )
132107, 131syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( A  e.  om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  y  e.  x )  /\  (
( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y )  /\  z  e.  ( om  ^o  y
) ) )  -> 
( ( ( A  .o  z )  e.  ( om  ^o  y
)  /\  ( om  ^o  y )  e.  ( om  ^o  x ) )  ->  ( A  .o  z )  e.  ( om  ^o  x ) ) )
133126, 130, 132mp2and 661 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( A  e.  om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  y  e.  x )  /\  (
( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y )  /\  z  e.  ( om  ^o  y
) ) )  -> 
( A  .o  z
)  e.  ( om 
^o  x ) )
134 ordelss 4557 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( Ord  ( om  ^o  x )  /\  ( A  .o  z )  e.  ( om  ^o  x
) )  ->  ( A  .o  z )  C_  ( om  ^o  x ) )
135109, 133, 134syl2anc 643 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( A  e.  om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  y  e.  x )  /\  (
( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y )  /\  z  e.  ( om  ^o  y
) ) )  -> 
( A  .o  z
)  C_  ( om  ^o  x ) )
136135ex 424 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  y  e.  x )  ->  (
( ( A  .o  ( om  ^o  y ) )  =  ( om 
^o  y )  /\  z  e.  ( om  ^o  y ) )  -> 
( A  .o  z
)  C_  ( om  ^o  x ) ) )
137106, 136syl5 30 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  y  e.  x )  ->  (
( ( (/)  e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om 
^o  y ) )  /\  ( (/)  e.  y  /\  z  e.  ( om  ^o  y ) ) )  ->  ( A  .o  z )  C_  ( om  ^o  x ) ) )
138137rexlimdva 2790 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  Lim  x ) )  -> 
( E. y  e.  x  ( ( (/)  e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y
) )  /\  ( (/) 
e.  y  /\  z  e.  ( om  ^o  y
) ) )  -> 
( A  .o  z
)  C_  ( om  ^o  x ) ) )
139102, 138syl5 30 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  Lim  x ) )  -> 
( ( A. y  e.  x  ( (/)  e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om 
^o  y ) )  /\  E. y  e.  x  ( (/)  e.  y  /\  z  e.  ( om  ^o  y ) ) )  ->  ( A  .o  z )  C_  ( om  ^o  x ) ) )
140139expdimp 427 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  A. y  e.  x  ( (/) 
e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y
) ) )  -> 
( E. y  e.  x  ( (/)  e.  y  /\  z  e.  ( om  ^o  y ) )  ->  ( A  .o  z )  C_  ( om  ^o  x ) ) )
141101, 140sylbid 207 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  A. y  e.  x  ( (/) 
e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y
) ) )  -> 
( z  e.  ( om  ^o  x )  ->  ( A  .o  z )  C_  ( om  ^o  x ) ) )
142141ralrimiv 2748 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  A. y  e.  x  ( (/) 
e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y
) ) )  ->  A. z  e.  ( om  ^o  x ) ( A  .o  z ) 
C_  ( om  ^o  x ) )
143 iunss 4092 . . . . . . . . . . . . . 14  |-  ( U_ z  e.  ( om  ^o  x ) ( A  .o  z )  C_  ( om  ^o  x )  <->  A. z  e.  ( om  ^o  x ) ( A  .o  z ) 
C_  ( om  ^o  x ) )
144142, 143sylibr 204 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  A. y  e.  x  ( (/) 
e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y
) ) )  ->  U_ z  e.  ( om  ^o  x ) ( A  .o  z ) 
C_  ( om  ^o  x ) )
14582, 144eqsstrd 3342 . . . . . . . . . . . 12  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  A. y  e.  x  ( (/) 
e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y
) ) )  -> 
( A  .o  ( om  ^o  x ) ) 
C_  ( om  ^o  x ) )
146 simpllr 736 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  A. y  e.  x  ( (/) 
e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y
) ) )  ->  (/) 
e.  A )
147 omword2 6776 . . . . . . . . . . . . 13  |-  ( ( ( ( om  ^o  x )  e.  On  /\  A  e.  On )  /\  (/)  e.  A )  ->  ( om  ^o  x )  C_  ( A  .o  ( om  ^o  x ) ) )
14872, 63, 146, 147syl21anc 1183 . . . . . . . . . . . 12  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  A. y  e.  x  ( (/) 
e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y
) ) )  -> 
( om  ^o  x
)  C_  ( A  .o  ( om  ^o  x
) ) )
149145, 148eqssd 3325 . . . . . . . . . . 11  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  Lim  x
) )  /\  A. y  e.  x  ( (/) 
e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y
) ) )  -> 
( A  .o  ( om  ^o  x ) )  =  ( om  ^o  x ) )
150149ex 424 . . . . . . . . . 10  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  Lim  x ) )  -> 
( A. y  e.  x  ( (/)  e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om 
^o  y ) )  ->  ( A  .o  ( om  ^o  x ) )  =  ( om 
^o  x ) ) )
151150anassrs 630 . . . . . . . . 9  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  om  e.  On )  /\  Lim  x
)  ->  ( A. y  e.  x  ( (/) 
e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y
) )  ->  ( A  .o  ( om  ^o  x ) )  =  ( om  ^o  x
) ) )
152151a1dd 44 . . . . . . . 8  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  om  e.  On )  /\  Lim  x
)  ->  ( A. y  e.  x  ( (/) 
e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y
) )  ->  ( (/) 
e.  x  ->  ( A  .o  ( om  ^o  x ) )  =  ( om  ^o  x
) ) ) )
153152expcom 425 . . . . . . 7  |-  ( Lim  x  ->  ( (
( A  e.  om  /\  (/)  e.  A )  /\  om  e.  On )  -> 
( A. y  e.  x  ( (/)  e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om 
^o  y ) )  ->  ( (/)  e.  x  ->  ( A  .o  ( om  ^o  x ) )  =  ( om  ^o  x ) ) ) ) )
1545, 10, 15, 20, 23, 62, 153tfinds3 4803 . . . . . 6  |-  ( B  e.  On  ->  (
( ( A  e. 
om  /\  (/)  e.  A
)  /\  om  e.  On )  ->  ( (/)  e.  B  ->  ( A  .o  ( om  ^o  B ) )  =  ( om  ^o  B
) ) ) )
155154com12 29 . . . . 5  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  om  e.  On )  -> 
( B  e.  On  ->  ( (/)  e.  B  ->  ( A  .o  ( om  ^o  B ) )  =  ( om  ^o  B ) ) ) )
156155adantrr 698 . . . 4  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  B  e.  On )
)  ->  ( B  e.  On  ->  ( (/)  e.  B  ->  ( A  .o  ( om  ^o  B ) )  =  ( om  ^o  B ) ) ) )
157156imp32 423 . . 3  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  B  e.  On ) )  /\  ( B  e.  On  /\  (/)  e.  B ) )  ->  ( A  .o  ( om  ^o  B ) )  =  ( om 
^o  B ) )
158157an32s 780 . 2  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( B  e.  On  /\  (/)  e.  B
) )  /\  ( om  e.  On  /\  B  e.  On ) )  -> 
( A  .o  ( om  ^o  B ) )  =  ( om  ^o  B ) )
159 nnm0 6807 . . . 4  |-  ( A  e.  om  ->  ( A  .o  (/) )  =  (/) )
160159ad3antrrr 711 . . 3  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( B  e.  On  /\  (/)  e.  B
) )  /\  -.  ( om  e.  On  /\  B  e.  On )
)  ->  ( A  .o  (/) )  =  (/) )
161 fnoe 6713 . . . . . . 7  |-  ^o  Fn  ( On  X.  On )
162 fndm 5503 . . . . . . 7  |-  (  ^o  Fn  ( On  X.  On )  ->  dom  ^o  =  ( On  X.  On ) )
163161, 162ax-mp 8 . . . . . 6  |-  dom  ^o  =  ( On  X.  On )
164163ndmov 6190 . . . . 5  |-  ( -.  ( om  e.  On  /\  B  e.  On )  ->  ( om  ^o  B )  =  (/) )
165164adantl 453 . . . 4  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( B  e.  On  /\  (/)  e.  B
) )  /\  -.  ( om  e.  On  /\  B  e.  On )
)  ->  ( om  ^o  B )  =  (/) )
166165oveq2d 6056 . . 3  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( B  e.  On  /\  (/)  e.  B
) )  /\  -.  ( om  e.  On  /\  B  e.  On )
)  ->  ( A  .o  ( om  ^o  B
) )  =  ( A  .o  (/) ) )
167160, 166, 1653eqtr4d 2446 . 2  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( B  e.  On  /\  (/)  e.  B
) )  /\  -.  ( om  e.  On  /\  B  e.  On )
)  ->  ( A  .o  ( om  ^o  B
) )  =  ( om  ^o  B ) )
168158, 167pm2.61dan 767 1  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( B  e.  On  /\  (/)  e.  B ) )  ->  ( A  .o  ( om  ^o  B ) )  =  ( om 
^o  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    \/ wo 358    /\ wa 359    = wceq 1649    e. wcel 1721    =/= wne 2567   A.wral 2666   E.wrex 2667   _Vcvv 2916    \ cdif 3277    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 comu 6681    ^o coe 6682
This theorem is referenced by:  cnfcom3  7617
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