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

Theorem omabs 6890
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 2497 . . . . . . . 8  |-  ( x  =  (/)  ->  ( (/)  e.  x  <->  (/)  e.  (/) ) )
2 oveq2 6089 . . . . . . . . . 10  |-  ( x  =  (/)  ->  ( om 
^o  x )  =  ( om  ^o  (/) ) )
32oveq2d 6097 . . . . . . . . 9  |-  ( x  =  (/)  ->  ( A  .o  ( om  ^o  x ) )  =  ( A  .o  ( om  ^o  (/) ) ) )
43, 2eqeq12d 2450 . . . . . . . 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 2497 . . . . . . . 8  |-  ( x  =  y  ->  ( (/) 
e.  x  <->  (/)  e.  y ) )
7 oveq2 6089 . . . . . . . . . 10  |-  ( x  =  y  ->  ( om  ^o  x )  =  ( om  ^o  y
) )
87oveq2d 6097 . . . . . . . . 9  |-  ( x  =  y  ->  ( A  .o  ( om  ^o  x ) )  =  ( A  .o  ( om  ^o  y ) ) )
98, 7eqeq12d 2450 . . . . . . . 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 2497 . . . . . . . 8  |-  ( x  =  suc  y  -> 
( (/)  e.  x  <->  (/)  e.  suc  y ) )
12 oveq2 6089 . . . . . . . . . 10  |-  ( x  =  suc  y  -> 
( om  ^o  x
)  =  ( om 
^o  suc  y )
)
1312oveq2d 6097 . . . . . . . . 9  |-  ( x  =  suc  y  -> 
( A  .o  ( om  ^o  x ) )  =  ( A  .o  ( om  ^o  suc  y
) ) )
1413, 12eqeq12d 2450 . . . . . . . 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 2497 . . . . . . . 8  |-  ( x  =  B  ->  ( (/) 
e.  x  <->  (/)  e.  B
) )
17 oveq2 6089 . . . . . . . . . 10  |-  ( x  =  B  ->  ( om  ^o  x )  =  ( om  ^o  B
) )
1817oveq2d 6097 . . . . . . . . 9  |-  ( x  =  B  ->  ( A  .o  ( om  ^o  x ) )  =  ( A  .o  ( om  ^o  B ) ) )
1918, 17eqeq12d 2450 . . . . . . . 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 3632 . . . . . . . . 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 6889 . . . . . . . . . . . . . . . 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 4646 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  (/)  ->  suc  y  =  suc  (/) )
31 df-1o 6724 . . . . . . . . . . . . . . . . . 18  |-  1o  =  suc  (/)
3230, 31syl6eqr 2486 . . . . . . . . . . . . . . . . 17  |-  ( y  =  (/)  ->  suc  y  =  1o )
3332oveq2d 6097 . . . . . . . . . . . . . . . 16  |-  ( y  =  (/)  ->  ( om 
^o  suc  y )  =  ( om  ^o  1o ) )
34 oe1 6787 . . . . . . . . . . . . . . . . 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 2490 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e. 
om  /\  (/)  e.  A
)  /\  ( om  e.  On  /\  y  e.  On ) )  /\  y  =  (/) )  -> 
( om  ^o  suc  y )  =  om )
3736oveq2d 6097 . . . . . . . . . . . . . 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 2478 . . . . . . . . . . . . 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 6088 . . . . . . . . . . . . . 14  |-  ( ( A  .o  ( om 
^o  y ) )  =  ( om  ^o  y )  ->  (
( A  .o  ( om  ^o  y ) )  .o  om )  =  ( ( om  ^o  y )  .o  om ) )
42 oesuc 6771 . . . . . . . . . . . . . . . . . 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 6097 . . . . . . . . . . . . . . . 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 4851 . . . . . . . . . . . . . . . . . 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 6781 . . . . . . . . . . . . . . . . . 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 6823 . . . . . . . . . . . . . . . . 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 2471 . . . . . . . . . . . . . . 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 2450 . . . . . . . . . . . . . 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 4699 . . . . . . . . . . . 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 2959 . . . . . . . . . . . . . . . . . 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 4644 . . . . . . . . . . . . . . . . 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 6781 . . . . . . . . . . . . . . . 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 6882 . . . . . . . . . . . . . . . . . 18  |-  1o  e.  om
7473a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  om  /\  (/)  e.  A )  /\  ( om  e.  On  /\  Lim  x ) )  ->  1o  e.  om )
75 ondif2 6746 . . . . . . . . . . . . . . . . 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 6843 . . . . . . . . . . . . . . 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 6777 . . . . . . . . . . . . . 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 6838 . . . . . . . . . . . . . . . . . . . 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 2503 . . . . . . . . . . . . . . . . . 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 4097 . . . . . . . . . . . . . . . . . 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 4606 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  On  /\  y  e.  x )  ->  y  e.  On )
92 on0eln0 4636 . . . . . . . . . . . . . . . . . . . . . . . 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 6744 . . . . . . . . . . . . . . . . . . . . . 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 2728 . . . . . . . . . . . . . . . . . 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 2846 . . . . . . . . . . . . . . . . . 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 4591 . . . . . . . . . . . . . . . . . . . . . . 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 4606 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6810 . . . . . . . . . . . . . . . . . . . . . . . . . 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 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 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 6831 . . . . . . . . . . . . . . . . . . . . . . . . 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 4627 . . . . . . . . . . . . . . . . . . . . . . . 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 4597 . . . . . . . . . . . . . . . . . . . . . 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 2830 . . . . . . . . . . . . . . . . . 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 2788 . . . . . . . . . . . . . 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 4132 . . . . . . . . . . . . . 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 3382 . . . . . . . . . . . 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 6817 . . . . . . . . . . . . 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 3365 . . . . . . . . . . 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 4844 . . . . . 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 6848 . . . 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 6754 . . . . . . 7  |-  ^o  Fn  ( On  X.  On )
162 fndm 5544 . . . . . . 7  |-  (  ^o  Fn  ( On  X.  On )  ->  dom  ^o  =  ( On  X.  On ) )
163161, 162ax-mp 8 . . . . . 6  |-  dom  ^o  =  ( On  X.  On )
164163ndmov 6231 . . . . 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 6097 . . 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 2478 . 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 1652    e. wcel 1725    =/= wne 2599   A.wral 2705   E.wrex 2706   _Vcvv 2956    \ cdif 3317    C_ wss 3320   (/)c0 3628   U_ciun 4093   Ord word 4580   Oncon0 4581   Lim wlim 4582   suc csuc 4583   omcom 4845    X. cxp 4876   dom cdm 4878    Fn wfn 5449  (class class class)co 6081   1oc1o 6717   2oc2o 6718    .o comu 6722    ^o coe 6723
This theorem is referenced by:  cnfcom3  7661
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-rep 4320  ax-sep 4330  ax-nul 4338  ax-pow 4377  ax-pr 4403  ax-un 4701
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2958  df-sbc 3162  df-csb 3252  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-pss 3336  df-nul 3629  df-if 3740  df-pw 3801  df-sn 3820  df-pr 3821  df-tp 3822  df-op 3823  df-uni 4016  df-int 4051  df-iun 4095  df-br 4213  df-opab 4267  df-mpt 4268  df-tr 4303  df-eprel 4494  df-id 4498  df-po 4503  df-so 4504  df-fr 4541  df-we 4543  df-ord 4584  df-on 4585  df-lim 4586  df-suc 4587  df-om 4846  df-xp 4884  df-rel 4885  df-cnv 4886  df-co 4887  df-dm 4888  df-rn 4889  df-res 4890  df-ima 4891  df-iota 5418  df-fun 5456  df-fn 5457  df-f 5458  df-f1 5459  df-fo 5460  df-f1o 5461  df-fv 5462  df-ov 6084  df-oprab 6085  df-mpt2 6086  df-1st 6349  df-2nd 6350  df-recs 6633  df-rdg 6668  df-1o 6724  df-2o 6725  df-oadd 6728  df-omul 6729  df-oexp 6730
  Copyright terms: Public domain W3C validator