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

Theorem omabs 7353
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 2495 . . . . . . . 8  |-  ( x  =  (/)  ->  ( (/)  e.  x  <->  (/)  e.  (/) ) )
2 oveq2 6310 . . . . . . . . . 10  |-  ( x  =  (/)  ->  ( om 
^o  x )  =  ( om  ^o  (/) ) )
32oveq2d 6318 . . . . . . . . 9  |-  ( x  =  (/)  ->  ( A  .o  ( om  ^o  x ) )  =  ( A  .o  ( om  ^o  (/) ) ) )
43, 2eqeq12d 2444 . . . . . . . 8  |-  ( x  =  (/)  ->  ( ( A  .o  ( om 
^o  x ) )  =  ( om  ^o  x )  <->  ( A  .o  ( om  ^o  (/) ) )  =  ( om  ^o  (/) ) ) )
51, 4imbi12d 321 . . . . . . 7  |-  ( x  =  (/)  ->  ( (
(/)  e.  x  ->  ( A  .o  ( om 
^o  x ) )  =  ( om  ^o  x ) )  <->  ( (/)  e.  (/)  ->  ( A  .o  ( om  ^o  (/) ) )  =  ( om  ^o  (/) ) ) ) )
6 eleq2 2495 . . . . . . . 8  |-  ( x  =  y  ->  ( (/) 
e.  x  <->  (/)  e.  y ) )
7 oveq2 6310 . . . . . . . . . 10  |-  ( x  =  y  ->  ( om  ^o  x )  =  ( om  ^o  y
) )
87oveq2d 6318 . . . . . . . . 9  |-  ( x  =  y  ->  ( A  .o  ( om  ^o  x ) )  =  ( A  .o  ( om  ^o  y ) ) )
98, 7eqeq12d 2444 . . . . . . . 8  |-  ( x  =  y  ->  (
( A  .o  ( om  ^o  x ) )  =  ( om  ^o  x )  <->  ( A  .o  ( om  ^o  y
) )  =  ( om  ^o  y ) ) )
106, 9imbi12d 321 . . . . . . 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 2495 . . . . . . . 8  |-  ( x  =  suc  y  -> 
( (/)  e.  x  <->  (/)  e.  suc  y ) )
12 oveq2 6310 . . . . . . . . . 10  |-  ( x  =  suc  y  -> 
( om  ^o  x
)  =  ( om 
^o  suc  y )
)
1312oveq2d 6318 . . . . . . . . 9  |-  ( x  =  suc  y  -> 
( A  .o  ( om  ^o  x ) )  =  ( A  .o  ( om  ^o  suc  y
) ) )
1413, 12eqeq12d 2444 . . . . . . . 8  |-  ( x  =  suc  y  -> 
( ( A  .o  ( om  ^o  x ) )  =  ( om 
^o  x )  <->  ( A  .o  ( om  ^o  suc  y ) )  =  ( om  ^o  suc  y ) ) )
1511, 14imbi12d 321 . . . . . . 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 2495 . . . . . . . 8  |-  ( x  =  B  ->  ( (/) 
e.  x  <->  (/)  e.  B
) )
17 oveq2 6310 . . . . . . . . . 10  |-  ( x  =  B  ->  ( om  ^o  x )  =  ( om  ^o  B
) )
1817oveq2d 6318 . . . . . . . . 9  |-  ( x  =  B  ->  ( A  .o  ( om  ^o  x ) )  =  ( A  .o  ( om  ^o  B ) ) )
1918, 17eqeq12d 2444 . . . . . . . 8  |-  ( x  =  B  ->  (
( A  .o  ( om  ^o  x ) )  =  ( om  ^o  x )  <->  ( A  .o  ( om  ^o  B
) )  =  ( om  ^o  B ) ) )
2016, 19imbi12d 321 . . . . . . 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 3765 . . . . . . . . 9  |-  -.  (/)  e.  (/)
2221pm2.21i 134 . . . . . . . 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 762 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  om  e.  On )
25 simpll 758 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  A  e.  om )
26 simplr 760 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  (/)  e.  A
)
27 omabslem 7352 . . . . . . . . . . . . . . . 16  |-  ( ( om  e.  On  /\  A  e.  om  /\  (/)  e.  A
)  ->  ( A  .o  om )  =  om )
2824, 25, 26, 27syl3anc 1264 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  ( A  .o  om )  =  om )
2928adantr 466 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  y  e.  On ) )  /\  y  =  (/) )  -> 
( A  .o  om )  =  om )
30 suceq 5504 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  (/)  ->  suc  y  =  suc  (/) )
31 df-1o 7187 . . . . . . . . . . . . . . . . . 18  |-  1o  =  suc  (/)
3230, 31syl6eqr 2481 . . . . . . . . . . . . . . . . 17  |-  ( y  =  (/)  ->  suc  y  =  1o )
3332oveq2d 6318 . . . . . . . . . . . . . . . 16  |-  ( y  =  (/)  ->  ( om 
^o  suc  y )  =  ( om  ^o  1o ) )
34 oe1 7250 . . . . . . . . . . . . . . . . 17  |-  ( om  e.  On  ->  ( om  ^o  1o )  =  om )
3534ad2antrl 732 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  ( om  ^o  1o )  =  om )
3633, 35sylan9eqr 2485 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  y  e.  On ) )  /\  y  =  (/) )  -> 
( om  ^o  suc  y )  =  om )
3736oveq2d 6318 . . . . . . . . . . . . . 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 2473 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  y  e.  On ) )  /\  y  =  (/) )  -> 
( A  .o  ( om  ^o  suc  y ) )  =  ( om 
^o  suc  y )
)
3938ex 435 . . . . . . . . . . . 12  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  ( y  =  (/)  ->  ( A  .o  ( om  ^o  suc  y ) )  =  ( om  ^o  suc  y ) ) )
4039a1dd 47 . . . . . . . . . . 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 6309 . . . . . . . . . . . . . 14  |-  ( ( A  .o  ( om 
^o  y ) )  =  ( om  ^o  y )  ->  (
( A  .o  ( om  ^o  y ) )  .o  om )  =  ( ( om  ^o  y )  .o  om ) )
42 oesuc 7234 . . . . . . . . . . . . . . . . . 18  |-  ( ( om  e.  On  /\  y  e.  On )  ->  ( om  ^o  suc  y )  =  ( ( om  ^o  y
)  .o  om )
)
4342adantl 467 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  ( om  ^o 
suc  y )  =  ( ( om  ^o  y )  .o  om ) )
4443oveq2d 6318 . . . . . . . . . . . . . . . 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 6709 . . . . . . . . . . . . . . . . . 18  |-  ( A  e.  om  ->  A  e.  On )
4645ad2antrr 730 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  A  e.  On )
47 oecl 7244 . . . . . . . . . . . . . . . . . 18  |-  ( ( om  e.  On  /\  y  e.  On )  ->  ( om  ^o  y
)  e.  On )
4847adantl 467 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  ( om  ^o  y )  e.  On )
49 omass 7286 . . . . . . . . . . . . . . . . 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 1264 . . . . . . . . . . . . . . . 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 2466 . . . . . . . . . . . . . . 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 2444 . . . . . . . . . . . . . 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 224 . . . . . . . . . . . . 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 54 . . . . . . . . . . . 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 81 . . . . . . . . . . 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 764 . . . . . . . . . . . 12  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  y  e.  On )
57 on0eqel 5556 . . . . . . . . . . . 12  |-  ( y  e.  On  ->  (
y  =  (/)  \/  (/)  e.  y ) )
5856, 57syl 17 . . . . . . . . . . 11  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  y  e.  On )
)  ->  ( y  =  (/)  \/  (/)  e.  y ) )
5940, 55, 58mpjaod 382 . . . . . . . . . 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 47 . . . . . . . . 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 652 . . . . . . . 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 436 . . . . . . 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 734 . . . . . . . . . . . . . 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 762 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  Lim  x ) )  ->  om  e.  On )
65 simprr 764 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  Lim  x ) )  ->  Lim  x )
66 vex 3084 . . . . . . . . . . . . . . . . . 18  |-  x  e. 
_V
6765, 66jctil 539 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  Lim  x ) )  -> 
( x  e.  _V  /\ 
Lim  x ) )
68 limelon 5502 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  _V  /\  Lim  x )  ->  x  e.  On )
6967, 68syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  Lim  x ) )  ->  x  e.  On )
70 oecl 7244 . . . . . . . . . . . . . . . 16  |-  ( ( om  e.  On  /\  x  e.  On )  ->  ( om  ^o  x
)  e.  On )
7164, 69, 70syl2anc 665 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  Lim  x ) )  -> 
( om  ^o  x
)  e.  On )
7271adantr 466 . . . . . . . . . . . . . 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 7345 . . . . . . . . . . . . . . . . . 18  |-  1o  e.  om
7473a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  Lim  x ) )  ->  1o  e.  om )
75 ondif2 7209 . . . . . . . . . . . . . . . . 17  |-  ( om  e.  ( On  \  2o )  <->  ( om  e.  On  /\  1o  e.  om ) )
7664, 74, 75sylanbrc 668 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  Lim  x ) )  ->  om  e.  ( On  \  2o ) )
7776adantr 466 . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . 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 7306 . . . . . . . . . . . . . . 15  |-  ( ( om  e.  ( On 
\  2o )  /\  ( x  e.  _V  /\ 
Lim  x ) )  ->  Lim  ( om  ^o  x ) )
8077, 78, 79syl2anc 665 . . . . . . . . . . . . . 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 7240 . . . . . . . . . . . . . 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 1262 . . . . . . . . . . . . 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 768 . . . . . . . . . . . . . . . . . . . 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 7301 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( om  e.  On  /\  ( x  e.  _V  /\ 
Lim  x ) )  ->  ( om  ^o  x )  =  U_ y  e.  ( x  \  1o ) ( om 
^o  y ) )
8583, 78, 84syl2anc 665 . . . . . . . . . . . . . . . . . . 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 2492 . . . . . . . . . . . . . . . . . 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 4301 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  U_ y  e.  ( x  \  1o ) ( om  ^o  y )  <->  E. y  e.  ( x  \  1o ) z  e.  ( om  ^o  y ) )
8886, 87syl6bb 264 . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . 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 653 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( y  e.  x  /\  (/)  e.  y )  /\  z  e.  ( om  ^o  y ) )  <->  ( y  e.  x  /\  ( (/)  e.  y  /\  z  e.  ( om  ^o  y
) ) ) )
91 onelon 5464 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  On  /\  y  e.  x )  ->  y  e.  On )
92 on0eln0 5494 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  On  ->  ( (/) 
e.  y  <->  y  =/=  (/) ) )
9391, 92syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  On  /\  y  e.  x )  ->  ( (/)  e.  y  <->  y  =/=  (/) ) )
9493pm5.32da 645 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  On  ->  (
( y  e.  x  /\  (/)  e.  y )  <-> 
( y  e.  x  /\  y  =/=  (/) ) ) )
95 dif1o 7207 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  ( x  \  1o )  <->  ( y  e.  x  /\  y  =/=  (/) ) )
9694, 95syl6bbr 266 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  On  ->  (
( y  e.  x  /\  (/)  e.  y )  <-> 
y  e.  ( x 
\  1o ) ) )
9796anbi1d 709 . . . . . . . . . . . . . . . . . . . 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 262 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  On  ->  (
( y  e.  x  /\  ( (/)  e.  y  /\  z  e.  ( om  ^o  y ) ) )  <->  ( y  e.  ( x  \  1o )  /\  z  e.  ( om  ^o  y ) ) ) )
9998rexbidv2 2935 . . . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . . . 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 259 . . . . . . . . . . . . . . . 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 2963 . . . . . . . . . . . . . . . . . 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 23 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
(/)  e.  y  ->  ( A  .o  ( om 
^o  y ) )  =  ( om  ^o  y ) )  -> 
( (/)  e.  y  -> 
( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y ) ) )
104103imp 430 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( (/)  e.  y  ->  ( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y ) )  /\  (/) 
e.  y )  -> 
( A  .o  ( om  ^o  y ) )  =  ( om  ^o  y ) )
105104anim1i 570 . . . . . . . . . . . . . . . . . . . . 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 651 . . . . . . . . . . . . . . . . . . . 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 730 . . . . . . . . . . . . . . . . . . . . . . 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 5449 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( om  ^o  x )  e.  On  ->  Ord  ( om  ^o  x ) )
109107, 108syl 17 . . . . . . . . . . . . . . . . . . . . . 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 764 . . . . . . . . . . . . . . . . . . . . . . . . 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 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5464 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( om  ^o  y
)  e.  On  /\  z  e.  ( om  ^o  y ) )  -> 
z  e.  On )
117115, 110, 116syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . . . . 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 730 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  Lim  x ) )  ->  A  e.  On )
119118ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . 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 760 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  Lim  x ) )  ->  (/) 
e.  A )
121120ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . 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 7273 . . . . . . . . . . . . . . . . . . . . . . . . . 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 1267 . . . . . . . . . . . . . . . . . . . . . . . . 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 213 . . . . . . . . . . . . . . . . . . . . . . . 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 762 . . . . . . . . . . . . . . . . . . . . . . . 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 2512 . . . . . . . . . . . . . . . . . . . . . . 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 730 . . . . . . . . . . . . . . . . . . . . . . . . 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 7294 . . . . . . . . . . . . . . . . . . . . . . . . 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 1264 . . . . . . . . . . . . . . . . . . . . . . . 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 213 . . . . . . . . . . . . . . . . . . . . . . 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 5485 . . . . . . . . . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . . . . . . . . . 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 683 . . . . . . . . . . . . . . . . . . . . . 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 5455 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( Ord  ( om  ^o  x )  /\  ( A  .o  z )  e.  ( om  ^o  x
) )  ->  ( A  .o  z )  C_  ( om  ^o  x ) )
135109, 133, 134syl2anc 665 . . . . . . . . . . . . . . . . . . . . 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 435 . . . . . . . . . . . . . . . . . . . 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 33 . . . . . . . . . . . . . . . . . . 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 2917 . . . . . . . . . . . . . . . . . 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 33 . . . . . . . . . . . . . . . . 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 438 . . . . . . . . . . . . . . . 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 218 . . . . . . . . . . . . . . 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 2837 . . . . . . . . . . . . . 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 4337 . . . . . . . . . . . . . 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 215 . . . . . . . . . . . . 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 3498 . . . . . . . . . . . 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 767 . . . . . . . . . . . . 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 7280 . . . . . . . . . . . . 13  |-  ( ( ( ( om  ^o  x )  e.  On  /\  A  e.  On )  /\  (/)  e.  A )  ->  ( om  ^o  x )  C_  ( A  .o  ( om  ^o  x ) ) )
14872, 63, 146, 147syl21anc 1263 . . . . . . . . . . . 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 3481 . . . . . . . . . . 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 435 . . . . . . . . . 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 652 . . . . . . . . 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 47 . . . . . . . 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 436 . . . . . . 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 6702 . . . . . 6  |-  ( B  e.  On  ->  (
( ( A  e. 
om  /\  (/)  e.  A
)  /\  om  e.  On )  ->  ( (/)  e.  B  ->  ( A  .o  ( om  ^o  B ) )  =  ( om  ^o  B
) ) ) )
155154com12 32 . . . . 5  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  om  e.  On )  -> 
( B  e.  On  ->  ( (/)  e.  B  ->  ( A  .o  ( om  ^o  B ) )  =  ( om  ^o  B ) ) ) )
156155adantrr 721 . . . 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 434 . . 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 811 . 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 7311 . . . 4  |-  ( A  e.  om  ->  ( A  .o  (/) )  =  (/) )
160159ad3antrrr 734 . . 3  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( B  e.  On  /\  (/)  e.  B
) )  /\  -.  ( om  e.  On  /\  B  e.  On )
)  ->  ( A  .o  (/) )  =  (/) )
161 fnoe 7217 . . . . . . 7  |-  ^o  Fn  ( On  X.  On )
162 fndm 5690 . . . . . . 7  |-  (  ^o  Fn  ( On  X.  On )  ->  dom  ^o  =  ( On  X.  On ) )
163161, 162ax-mp 5 . . . . . 6  |-  dom  ^o  =  ( On  X.  On )
164163ndmov 6464 . . . . 5  |-  ( -.  ( om  e.  On  /\  B  e.  On )  ->  ( om  ^o  B )  =  (/) )
165164adantl 467 . . . 4  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( B  e.  On  /\  (/)  e.  B
) )  /\  -.  ( om  e.  On  /\  B  e.  On )
)  ->  ( om  ^o  B )  =  (/) )
166165oveq2d 6318 . . 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 2473 . 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 798 1  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( B  e.  On  /\  (/)  e.  B ) )  ->  ( A  .o  ( om  ^o  B ) )  =  ( om 
^o  B ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    \/ wo 369    /\ wa 370    = wceq 1437    e. wcel 1868    =/= wne 2618   A.wral 2775   E.wrex 2776   _Vcvv 3081    \ cdif 3433    C_ wss 3436   (/)c0 3761   U_ciun 4296    X. cxp 4848   dom cdm 4850   Ord word 5438   Oncon0 5439   Lim wlim 5440   suc csuc 5441    Fn wfn 5593  (class class class)co 6302   omcom 6703   1oc1o 7180   2oc2o 7181    .o comu 7185    ^o coe 7186
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657  ax-un 6594
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-int 4253  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4761  df-id 4765  df-po 4771  df-so 4772  df-fr 4809  df-we 4811  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-pred 5396  df-ord 5442  df-on 5443  df-lim 5444  df-suc 5445  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-f1 5603  df-fo 5604  df-f1o 5605  df-fv 5606  df-ov 6305  df-oprab 6306  df-mpt2 6307  df-om 6704  df-1st 6804  df-2nd 6805  df-wrecs 7033  df-recs 7095  df-rdg 7133  df-1o 7187  df-2o 7188  df-oadd 7191  df-omul 7192  df-oexp 7193
This theorem is referenced by:  cnfcom3  8211
  Copyright terms: Public domain W3C validator