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

Theorem omabs 6645
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 2344 . . . . . . . 8  |-  ( x  =  (/)  ->  ( (/)  e.  x  <->  (/)  e.  (/) ) )
2 oveq2 5866 . . . . . . . . . 10  |-  ( x  =  (/)  ->  ( om 
^o  x )  =  ( om  ^o  (/) ) )
32oveq2d 5874 . . . . . . . . 9  |-  ( x  =  (/)  ->  ( A  .o  ( om  ^o  x ) )  =  ( A  .o  ( om  ^o  (/) ) ) )
43, 2eqeq12d 2297 . . . . . . . 8  |-  ( x  =  (/)  ->  ( ( A  .o  ( om 
^o  x ) )  =  ( om  ^o  x )  <->  ( A  .o  ( om  ^o  (/) ) )  =  ( om  ^o  (/) ) ) )
51, 4imbi12d 311 . . . . . . 7  |-  ( x  =  (/)  ->  ( (
(/)  e.  x  ->  ( A  .o  ( om 
^o  x ) )  =  ( om  ^o  x ) )  <->  ( (/)  e.  (/)  ->  ( A  .o  ( om  ^o  (/) ) )  =  ( om  ^o  (/) ) ) ) )
6 eleq2 2344 . . . . . . . 8  |-  ( x  =  y  ->  ( (/) 
e.  x  <->  (/)  e.  y ) )
7 oveq2 5866 . . . . . . . . . 10  |-  ( x  =  y  ->  ( om  ^o  x )  =  ( om  ^o  y
) )
87oveq2d 5874 . . . . . . . . 9  |-  ( x  =  y  ->  ( A  .o  ( om  ^o  x ) )  =  ( A  .o  ( om  ^o  y ) ) )
98, 7eqeq12d 2297 . . . . . . . 8  |-  ( x  =  y  ->  (
( A  .o  ( om  ^o  x ) )  =  ( om  ^o  x )  <->  ( A  .o  ( om  ^o  y
) )  =  ( om  ^o  y ) ) )
106, 9imbi12d 311 . . . . . . 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 2344 . . . . . . . 8  |-  ( x  =  suc  y  -> 
( (/)  e.  x  <->  (/)  e.  suc  y ) )
12 oveq2 5866 . . . . . . . . . 10  |-  ( x  =  suc  y  -> 
( om  ^o  x
)  =  ( om 
^o  suc  y )
)
1312oveq2d 5874 . . . . . . . . 9  |-  ( x  =  suc  y  -> 
( A  .o  ( om  ^o  x ) )  =  ( A  .o  ( om  ^o  suc  y
) ) )
1413, 12eqeq12d 2297 . . . . . . . 8  |-  ( x  =  suc  y  -> 
( ( A  .o  ( om  ^o  x ) )  =  ( om 
^o  x )  <->  ( A  .o  ( om  ^o  suc  y ) )  =  ( om  ^o  suc  y ) ) )
1511, 14imbi12d 311 . . . . . . 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 2344 . . . . . . . 8  |-  ( x  =  B  ->  ( (/) 
e.  x  <->  (/)  e.  B
) )
17 oveq2 5866 . . . . . . . . . 10  |-  ( x  =  B  ->  ( om  ^o  x )  =  ( om  ^o  B
) )
1817oveq2d 5874 . . . . . . . . 9  |-  ( x  =  B  ->  ( A  .o  ( om  ^o  x ) )  =  ( A  .o  ( om  ^o  B ) ) )
1918, 17eqeq12d 2297 . . . . . . . 8  |-  ( x  =  B  ->  (
( A  .o  ( om  ^o  x ) )  =  ( om  ^o  x )  <->  ( A  .o  ( om  ^o  B
) )  =  ( om  ^o  B ) ) )
2016, 19imbi12d 311 . . . . . . 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 3459 . . . . . . . . 9  |-  -.  (/)  e.  (/)
2221pm2.21i 123 . . . . . . . 8  |-  ( (/)  e.  (/)  ->  ( A  .o  ( om  ^o  (/) ) )  =  ( om  ^o  (/) ) )
2322a1i 10 . . . . . . 7  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  om  e.  On )  -> 
( (/)  e.  (/)  ->  ( A  .o  ( om  ^o  (/) ) )  =  ( om  ^o  (/) ) ) )
24 simprl 732 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  om  e.  On )
25 simpll 730 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  A  e.  om )
26 simplr 731 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  (/)  e.  A
)
27 omabslem 6644 . . . . . . . . . . . . . . . 16  |-  ( ( om  e.  On  /\  A  e.  om  /\  (/)  e.  A
)  ->  ( A  .o  om )  =  om )
2824, 25, 26, 27syl3anc 1182 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  ( A  .o  om )  =  om )
2928adantr 451 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  y  e.  On ) )  /\  y  =  (/) )  -> 
( A  .o  om )  =  om )
30 suceq 4457 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  (/)  ->  suc  y  =  suc  (/) )
31 df-1o 6479 . . . . . . . . . . . . . . . . . 18  |-  1o  =  suc  (/)
3230, 31syl6eqr 2333 . . . . . . . . . . . . . . . . 17  |-  ( y  =  (/)  ->  suc  y  =  1o )
3332oveq2d 5874 . . . . . . . . . . . . . . . 16  |-  ( y  =  (/)  ->  ( om 
^o  suc  y )  =  ( om  ^o  1o ) )
34 oe1 6542 . . . . . . . . . . . . . . . . 17  |-  ( om  e.  On  ->  ( om  ^o  1o )  =  om )
3534ad2antrl 708 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  ( om  ^o  1o )  =  om )
3633, 35sylan9eqr 2337 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  y  e.  On ) )  /\  y  =  (/) )  -> 
( om  ^o  suc  y )  =  om )
3736oveq2d 5874 . . . . . . . . . . . . . 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 2325 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  y  e.  On ) )  /\  y  =  (/) )  -> 
( A  .o  ( om  ^o  suc  y ) )  =  ( om 
^o  suc  y )
)
3938ex 423 . . . . . . . . . . . 12  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  ( y  =  (/)  ->  ( A  .o  ( om  ^o  suc  y ) )  =  ( om  ^o  suc  y ) ) )
4039a1dd 42 . . . . . . . . . . 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 5865 . . . . . . . . . . . . . 14  |-  ( ( A  .o  ( om 
^o  y ) )  =  ( om  ^o  y )  ->  (
( A  .o  ( om  ^o  y ) )  .o  om )  =  ( ( om  ^o  y )  .o  om ) )
42 oesuc 6526 . . . . . . . . . . . . . . . . . 18  |-  ( ( om  e.  On  /\  y  e.  On )  ->  ( om  ^o  suc  y )  =  ( ( om  ^o  y
)  .o  om )
)
4342adantl 452 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  ( om  ^o 
suc  y )  =  ( ( om  ^o  y )  .o  om ) )
4443oveq2d 5874 . . . . . . . . . . . . . . . 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 4662 . . . . . . . . . . . . . . . . . 18  |-  ( A  e.  om  ->  A  e.  On )
4645ad2antrr 706 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  A  e.  On )
47 oecl 6536 . . . . . . . . . . . . . . . . . 18  |-  ( ( om  e.  On  /\  y  e.  On )  ->  ( om  ^o  y
)  e.  On )
4847adantl 452 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  ( om  ^o  y )  e.  On )
49 omass 6578 . . . . . . . . . . . . . . . . 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 1182 . . . . . . . . . . . . . . . 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 2318 . . . . . . . . . . . . . . 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 2297 . . . . . . . . . . . . . 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 212 . . . . . . . . . . . . 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 48 . . . . . . . . . . . 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 72 . . . . . . . . . . 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 733 . . . . . . . . . . . 12  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  y  e.  On )
57 on0eqel 4510 . . . . . . . . . . . 12  |-  ( y  e.  On  ->  (
y  =  (/)  \/  (/)  e.  y ) )
5856, 57syl 15 . . . . . . . . . . 11  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  ( y  =  (/)  \/  (/)  e.  y ) )
5940, 55, 58mpjaod 370 . . . . . . . . . 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 42 . . . . . . . . 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 629 . . . . . . . 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 424 . . . . . . 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 710 . . . . . . . . . . . . . 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 732 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  Lim  x ) )  ->  om  e.  On )
65 simprr 733 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  Lim  x ) )  ->  Lim  x )
66 vex 2791 . . . . . . . . . . . . . . . . . 18  |-  x  e. 
_V
6765, 66jctil 523 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  Lim  x ) )  -> 
( x  e.  _V  /\ 
Lim  x ) )
68 limelon 4455 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  _V  /\  Lim  x )  ->  x  e.  On )
6967, 68syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  Lim  x ) )  ->  x  e.  On )
70 oecl 6536 . . . . . . . . . . . . . . . 16  |-  ( ( om  e.  On  /\  x  e.  On )  ->  ( om  ^o  x
)  e.  On )
7164, 69, 70syl2anc 642 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  Lim  x ) )  -> 
( om  ^o  x
)  e.  On )
7271adantr 451 . . . . . . . . . . . . . 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 6637 . . . . . . . . . . . . . . . . . 18  |-  1o  e.  om
7473a1i 10 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  Lim  x ) )  ->  1o  e.  om )
75 ondif2 6501 . . . . . . . . . . . . . . . . 17  |-  ( om  e.  ( On  \  2o )  <->  ( om  e.  On  /\  1o  e.  om ) )
7664, 74, 75sylanbrc 645 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  Lim  x ) )  ->  om  e.  ( On  \  2o ) )
7776adantr 451 . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . . 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 6598 . . . . . . . . . . . . . . 15  |-  ( ( om  e.  ( On 
\  2o )  /\  ( x  e.  _V  /\ 
Lim  x ) )  ->  Lim  ( om  ^o  x ) )
8077, 78, 79syl2anc 642 . . . . . . . . . . . . . 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 6532 . . . . . . . . . . . . . 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 1180 . . . . . . . . . . . . 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 736 . . . . . . . . . . . . . . . . . . . 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 6593 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( om  e.  On  /\  ( x  e.  _V  /\ 
Lim  x ) )  ->  ( om  ^o  x )  =  U_ y  e.  ( x  \  1o ) ( om 
^o  y ) )
8583, 78, 84syl2anc 642 . . . . . . . . . . . . . . . . . . 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 2350 . . . . . . . . . . . . . . . . . 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 3909 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  U_ y  e.  ( x  \  1o ) ( om  ^o  y )  <->  E. y  e.  ( x  \  1o ) z  e.  ( om  ^o  y ) )
8886, 87syl6bb 252 . . . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . . . . . 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 630 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( y  e.  x  /\  (/)  e.  y )  /\  z  e.  ( om  ^o  y ) )  <->  ( y  e.  x  /\  ( (/)  e.  y  /\  z  e.  ( om  ^o  y
) ) ) )
91 onelon 4417 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  On  /\  y  e.  x )  ->  y  e.  On )
92 on0eln0 4447 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  On  ->  ( (/) 
e.  y  <->  y  =/=  (/) ) )
9391, 92syl 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  On  /\  y  e.  x )  ->  ( (/)  e.  y  <->  y  =/=  (/) ) )
9493pm5.32da 622 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  On  ->  (
( y  e.  x  /\  (/)  e.  y )  <-> 
( y  e.  x  /\  y  =/=  (/) ) ) )
95 dif1o 6499 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  ( x  \  1o )  <->  ( y  e.  x  /\  y  =/=  (/) ) )
9694, 95syl6bbr 254 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  On  ->  (
( y  e.  x  /\  (/)  e.  y )  <-> 
y  e.  ( x 
\  1o ) ) )
9796anbi1d 685 . . . . . . . . . . . . . . . . . . . 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 250 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  On  ->  (
( y  e.  x  /\  ( (/)  e.  y  /\  z  e.  ( om  ^o  y ) ) )  <->  ( y  e.  ( x  \  1o )  /\  z  e.  ( om  ^o  y ) ) ) )
9998rexbidv2 2566 . . . . . . . . . . . . . . . . . 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 15 . . . . . . . . . . . . . . . . 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 247 . . . . . . . . . . . . . . . 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 2683 . . . . . . . . . . . . . . . . . 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 19 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
(/)  e.  y  ->  ( A  .o  ( om 
^o  y ) )  =  ( om  ^o  y ) )  -> 
( (/)  e.  y  -> 
( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y ) ) )
104103imp 418 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( (/)  e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y ) )  /\  (/) 
e.  y )  -> 
( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y ) )
105104anim1i 551 . . . . . . . . . . . . . . . . . . . . 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 628 . . . . . . . . . . . . . . . . . . . 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 706 . . . . . . . . . . . . . . . . . . . . . . 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 4402 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( om  ^o  x )  e.  On  ->  Ord  ( om  ^o  x ) )
109107, 108syl 15 . . . . . . . . . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . . . . . . . . . . . . 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 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 642 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4417 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( om  ^o  y
)  e.  On  /\  z  e.  ( om  ^o  y ) )  -> 
z  e.  On )
117115, 110, 116syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . 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 706 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  Lim  x ) )  ->  A  e.  On )
119118ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . 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 731 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  Lim  x ) )  ->  (/) 
e.  A )
121120ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . 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 6565 . . . . . . . . . . . . . . . . . . . . . . . . . 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 1185 . . . . . . . . . . . . . . . . . . . . . . . . 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 201 . . . . . . . . . . . . . . . . . . . . . . . 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 732 . . . . . . . . . . . . . . . . . . . . . . . 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 2359 . . . . . . . . . . . . . . . . . . . . . . 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 706 . . . . . . . . . . . . . . . . . . . . . . . . 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 6586 . . . . . . . . . . . . . . . . . . . . . . . . 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 1182 . . . . . . . . . . . . . . . . . . . . . . . 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 201 . . . . . . . . . . . . . . . . . . . . . . 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 4438 . . . . . . . . . . . . . . . . . . . . . . . 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 15 . . . . . . . . . . . . . . . . . . . . . . 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 660 . . . . . . . . . . . . . . . . . . . . . 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 4408 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( Ord  ( om  ^o  x )  /\  ( A  .o  z )  e.  ( om  ^o  x
) )  ->  ( A  .o  z )  C_  ( om  ^o  x ) )
135109, 133, 134syl2anc 642 . . . . . . . . . . . . . . . . . . . . 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 423 . . . . . . . . . . . . . . . . . . . 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 28 . . . . . . . . . . . . . . . . . . 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 2667 . . . . . . . . . . . . . . . . . 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 28 . . . . . . . . . . . . . . . . 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 426 . . . . . . . . . . . . . . . 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 206 . . . . . . . . . . . . . . 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 2625 . . . . . . . . . . . . . 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 3943 . . . . . . . . . . . . . 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 203 . . . . . . . . . . . . 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 3212 . . . . . . . . . . . 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 735 . . . . . . . . . . . . 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 6572 . . . . . . . . . . . . 13  |-  ( ( ( ( om  ^o  x )  e.  On  /\  A  e.  On )  /\  (/)  e.  A )  ->  ( om  ^o  x )  C_  ( A  .o  ( om  ^o  x ) ) )
14872, 63, 146, 147syl21anc 1181 . . . . . . . . . . . 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 3196 . . . . . . . . . . 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 423 . . . . . . . . . 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 629 . . . . . . . . 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 42 . . . . . . . 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 424 . . . . . . 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 4655 . . . . . 6  |-  ( B  e.  On  ->  (
( ( A  e. 
om  /\  (/)  e.  A
)  /\  om  e.  On )  ->  ( (/)  e.  B  ->  ( A  .o  ( om  ^o  B ) )  =  ( om  ^o  B
) ) ) )
155154com12 27 . . . . 5  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  om  e.  On )  -> 
( B  e.  On  ->  ( (/)  e.  B  ->  ( A  .o  ( om  ^o  B ) )  =  ( om  ^o  B ) ) ) )
156155adantrr 697 . . . 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 422 . . 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 779 . 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 6603 . . . 4  |-  ( A  e.  om  ->  ( A  .o  (/) )  =  (/) )
160159ad3antrrr 710 . . 3  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( B  e.  On  /\  (/)  e.  B
) )  /\  -.  ( om  e.  On  /\  B  e.  On )
)  ->  ( A  .o  (/) )  =  (/) )
161 fnoe 6509 . . . . . . 7  |-  ^o  Fn  ( On  X.  On )
162 fndm 5343 . . . . . . 7  |-  (  ^o  Fn  ( On  X.  On )  ->  dom  ^o  =  ( On  X.  On ) )
163161, 162ax-mp 8 . . . . . 6  |-  dom  ^o  =  ( On  X.  On )
164163ndmov 6004 . . . . 5  |-  ( -.  ( om  e.  On  /\  B  e.  On )  ->  ( om  ^o  B )  =  (/) )
165164adantl 452 . . . 4  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( B  e.  On  /\  (/)  e.  B
) )  /\  -.  ( om  e.  On  /\  B  e.  On )
)  ->  ( om  ^o  B )  =  (/) )
166165oveq2d 5874 . . 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 2325 . 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 766 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 176    \/ wo 357    /\ wa 358    = wceq 1623    e. wcel 1684    =/= wne 2446   A.wral 2543   E.wrex 2544   _Vcvv 2788    \ cdif 3149    C_ wss 3152   (/)c0 3455   U_ciun 3905   Ord word 4391   Oncon0 4392   Lim wlim 4393   suc csuc 4394   omcom 4656    X. cxp 4687   dom cdm 4689    Fn wfn 5250  (class class class)co 5858   1oc1o 6472   2oc2o 6473    .o comu 6477    ^o coe 6478
This theorem is referenced by:  cnfcom3  7407
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-reu 2550  df-rmo 2551  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-int 3863  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-1st 6122  df-2nd 6123  df-recs 6388  df-rdg 6423  df-1o 6479  df-2o 6480  df-oadd 6483  df-omul 6484  df-oexp 6485
  Copyright terms: Public domain W3C validator