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

Definition df-opsr 16122
Description: Define a total order on the set of all power series in  s from the index set  i given a wellordering  r of  i and a totally ordered base ring  s. (Contributed by Mario Carneiro, 8-Feb-2015.)
Assertion
Ref Expression
df-opsr  |- ordPwSer  =  ( i  e.  _V , 
s  e.  _V  |->  ( r  e.  ~P (
i  X.  i ) 
|->  [_ ( i mPwSer  s
)  /  p ]_ ( p sSet  <. ( le
`  ndx ) ,  { <. x ,  y >.  |  ( { x ,  y }  C_  ( Base `  p )  /\  ( [. { h  e.  ( NN0  ^m  i
)  |  ( `' h " NN )  e.  Fin }  / 
d ]. E. z  e.  d  ( ( x `
 z ) ( lt `  s ) ( y `  z
)  /\  A. w  e.  d  ( w
( r  <bag  i ) z  ->  ( x `  w )  =  ( y `  w ) ) )  \/  x  =  y ) ) } >. ) ) )
Distinct variable group:    h, d, i, p, r, s, w, x, y, z

Detailed syntax breakdown of Definition df-opsr
StepHypRef Expression
1 copws 16111 . 2  class ordPwSer
2 vi . . 3  set  i
3 vs . . 3  set  s
4 cvv 2801 . . 3  class  _V
5 vr . . . 4  set  r
62cv 1631 . . . . . 6  class  i
76, 6cxp 4703 . . . . 5  class  ( i  X.  i )
87cpw 3638 . . . 4  class  ~P (
i  X.  i )
9 vp . . . . 5  set  p
103cv 1631 . . . . . 6  class  s
11 cmps 16103 . . . . . 6  class mPwSer
126, 10, 11co 5874 . . . . 5  class  ( i mPwSer 
s )
139cv 1631 . . . . . 6  class  p
14 cnx 13161 . . . . . . . 8  class  ndx
15 cple 13231 . . . . . . . 8  class  le
1614, 15cfv 5271 . . . . . . 7  class  ( le
`  ndx )
17 vx . . . . . . . . . . . 12  set  x
1817cv 1631 . . . . . . . . . . 11  class  x
19 vy . . . . . . . . . . . 12  set  y
2019cv 1631 . . . . . . . . . . 11  class  y
2118, 20cpr 3654 . . . . . . . . . 10  class  { x ,  y }
22 cbs 13164 . . . . . . . . . . 11  class  Base
2313, 22cfv 5271 . . . . . . . . . 10  class  ( Base `  p )
2421, 23wss 3165 . . . . . . . . 9  wff  { x ,  y }  C_  ( Base `  p )
25 vz . . . . . . . . . . . . . . . 16  set  z
2625cv 1631 . . . . . . . . . . . . . . 15  class  z
2726, 18cfv 5271 . . . . . . . . . . . . . 14  class  ( x `
 z )
2826, 20cfv 5271 . . . . . . . . . . . . . 14  class  ( y `
 z )
29 cplt 14091 . . . . . . . . . . . . . . 15  class  lt
3010, 29cfv 5271 . . . . . . . . . . . . . 14  class  ( lt
`  s )
3127, 28, 30wbr 4039 . . . . . . . . . . . . 13  wff  ( x `
 z ) ( lt `  s ) ( y `  z
)
32 vw . . . . . . . . . . . . . . . . 17  set  w
3332cv 1631 . . . . . . . . . . . . . . . 16  class  w
345cv 1631 . . . . . . . . . . . . . . . . 17  class  r
35 cltb 16110 . . . . . . . . . . . . . . . . 17  class  <bag
3634, 6, 35co 5874 . . . . . . . . . . . . . . . 16  class  ( r  <bag  i )
3733, 26, 36wbr 4039 . . . . . . . . . . . . . . 15  wff  w ( r  <bag  i ) z
3833, 18cfv 5271 . . . . . . . . . . . . . . . 16  class  ( x `
 w )
3933, 20cfv 5271 . . . . . . . . . . . . . . . 16  class  ( y `
 w )
4038, 39wceq 1632 . . . . . . . . . . . . . . 15  wff  ( x `
 w )  =  ( y `  w
)
4137, 40wi 4 . . . . . . . . . . . . . 14  wff  ( w ( r  <bag  i ) z  ->  ( x `  w )  =  ( y `  w ) )
42 vd . . . . . . . . . . . . . . 15  set  d
4342cv 1631 . . . . . . . . . . . . . 14  class  d
4441, 32, 43wral 2556 . . . . . . . . . . . . 13  wff  A. w  e.  d  ( w
( r  <bag  i ) z  ->  ( x `  w )  =  ( y `  w ) )
4531, 44wa 358 . . . . . . . . . . . 12  wff  ( ( x `  z ) ( lt `  s
) ( y `  z )  /\  A. w  e.  d  (
w ( r  <bag  i ) z  ->  (
x `  w )  =  ( y `  w ) ) )
4645, 25, 43wrex 2557 . . . . . . . . . . 11  wff  E. z  e.  d  ( (
x `  z )
( lt `  s
) ( y `  z )  /\  A. w  e.  d  (
w ( r  <bag  i ) z  ->  (
x `  w )  =  ( y `  w ) ) )
47 vh . . . . . . . . . . . . . . . 16  set  h
4847cv 1631 . . . . . . . . . . . . . . 15  class  h
4948ccnv 4704 . . . . . . . . . . . . . 14  class  `' h
50 cn 9762 . . . . . . . . . . . . . 14  class  NN
5149, 50cima 4708 . . . . . . . . . . . . 13  class  ( `' h " NN )
52 cfn 6879 . . . . . . . . . . . . 13  class  Fin
5351, 52wcel 1696 . . . . . . . . . . . 12  wff  ( `' h " NN )  e.  Fin
54 cn0 9981 . . . . . . . . . . . . 13  class  NN0
55 cmap 6788 . . . . . . . . . . . . 13  class  ^m
5654, 6, 55co 5874 . . . . . . . . . . . 12  class  ( NN0 
^m  i )
5753, 47, 56crab 2560 . . . . . . . . . . 11  class  { h  e.  ( NN0  ^m  i
)  |  ( `' h " NN )  e.  Fin }
5846, 42, 57wsbc 3004 . . . . . . . . . 10  wff  [. {
h  e.  ( NN0 
^m  i )  |  ( `' h " NN )  e.  Fin }  /  d ]. E. z  e.  d  (
( x `  z
) ( lt `  s ) ( y `
 z )  /\  A. w  e.  d  ( w ( r  <bag  i ) z  ->  (
x `  w )  =  ( y `  w ) ) )
5917, 19weq 1633 . . . . . . . . . 10  wff  x  =  y
6058, 59wo 357 . . . . . . . . 9  wff  ( [. { h  e.  ( NN0  ^m  i )  |  ( `' h " NN )  e.  Fin }  /  d ]. E. z  e.  d  (
( x `  z
) ( lt `  s ) ( y `
 z )  /\  A. w  e.  d  ( w ( r  <bag  i ) z  ->  (
x `  w )  =  ( y `  w ) ) )  \/  x  =  y )
6124, 60wa 358 . . . . . . . 8  wff  ( { x ,  y } 
C_  ( Base `  p
)  /\  ( [. { h  e.  ( NN0  ^m  i )  |  ( `' h " NN )  e.  Fin }  /  d ]. E. z  e.  d  (
( x `  z
) ( lt `  s ) ( y `
 z )  /\  A. w  e.  d  ( w ( r  <bag  i ) z  ->  (
x `  w )  =  ( y `  w ) ) )  \/  x  =  y ) )
6261, 17, 19copab 4092 . . . . . . 7  class  { <. x ,  y >.  |  ( { x ,  y }  C_  ( Base `  p )  /\  ( [. { h  e.  ( NN0  ^m  i )  |  ( `' h " NN )  e.  Fin }  /  d ]. E. z  e.  d  (
( x `  z
) ( lt `  s ) ( y `
 z )  /\  A. w  e.  d  ( w ( r  <bag  i ) z  ->  (
x `  w )  =  ( y `  w ) ) )  \/  x  =  y ) ) }
6316, 62cop 3656 . . . . . 6  class  <. ( le `  ndx ) ,  { <. x ,  y
>.  |  ( {
x ,  y } 
C_  ( Base `  p
)  /\  ( [. { h  e.  ( NN0  ^m  i )  |  ( `' h " NN )  e.  Fin }  /  d ]. E. z  e.  d  (
( x `  z
) ( lt `  s ) ( y `
 z )  /\  A. w  e.  d  ( w ( r  <bag  i ) z  ->  (
x `  w )  =  ( y `  w ) ) )  \/  x  =  y ) ) } >.
64 csts 13162 . . . . . 6  class sSet
6513, 63, 64co 5874 . . . . 5  class  ( p sSet  <. ( le `  ndx ) ,  { <. x ,  y >.  |  ( { x ,  y }  C_  ( Base `  p )  /\  ( [. { h  e.  ( NN0  ^m  i )  |  ( `' h " NN )  e.  Fin }  /  d ]. E. z  e.  d  (
( x `  z
) ( lt `  s ) ( y `
 z )  /\  A. w  e.  d  ( w ( r  <bag  i ) z  ->  (
x `  w )  =  ( y `  w ) ) )  \/  x  =  y ) ) } >. )
669, 12, 65csb 3094 . . . 4  class  [_ (
i mPwSer  s )  /  p ]_ ( p sSet  <. ( le `  ndx ) ,  { <. x ,  y
>.  |  ( {
x ,  y } 
C_  ( Base `  p
)  /\  ( [. { h  e.  ( NN0  ^m  i )  |  ( `' h " NN )  e.  Fin }  /  d ]. E. z  e.  d  (
( x `  z
) ( lt `  s ) ( y `
 z )  /\  A. w  e.  d  ( w ( r  <bag  i ) z  ->  (
x `  w )  =  ( y `  w ) ) )  \/  x  =  y ) ) } >. )
675, 8, 66cmpt 4093 . . 3  class  ( r  e.  ~P ( i  X.  i )  |->  [_ ( i mPwSer  s )  /  p ]_ ( p sSet  <. ( le `  ndx ) ,  { <. x ,  y >.  |  ( { x ,  y }  C_  ( Base `  p )  /\  ( [. { h  e.  ( NN0  ^m  i )  |  ( `' h " NN )  e.  Fin }  /  d ]. E. z  e.  d  (
( x `  z
) ( lt `  s ) ( y `
 z )  /\  A. w  e.  d  ( w ( r  <bag  i ) z  ->  (
x `  w )  =  ( y `  w ) ) )  \/  x  =  y ) ) } >. ) )
682, 3, 4, 4, 67cmpt2 5876 . 2  class  ( i  e.  _V ,  s  e.  _V  |->  ( r  e.  ~P ( i  X.  i )  |->  [_ ( i mPwSer  s )  /  p ]_ ( p sSet  <. ( le `  ndx ) ,  { <. x ,  y >.  |  ( { x ,  y }  C_  ( Base `  p )  /\  ( [. { h  e.  ( NN0  ^m  i )  |  ( `' h " NN )  e.  Fin }  /  d ]. E. z  e.  d  (
( x `  z
) ( lt `  s ) ( y `
 z )  /\  A. w  e.  d  ( w ( r  <bag  i ) z  ->  (
x `  w )  =  ( y `  w ) ) )  \/  x  =  y ) ) } >. ) ) )
691, 68wceq 1632 1  wff ordPwSer  =  ( i  e.  _V , 
s  e.  _V  |->  ( r  e.  ~P (
i  X.  i ) 
|->  [_ ( i mPwSer  s
)  /  p ]_ ( p sSet  <. ( le
`  ndx ) ,  { <. x ,  y >.  |  ( { x ,  y }  C_  ( Base `  p )  /\  ( [. { h  e.  ( NN0  ^m  i
)  |  ( `' h " NN )  e.  Fin }  / 
d ]. E. z  e.  d  ( ( x `
 z ) ( lt `  s ) ( y `  z
)  /\  A. w  e.  d  ( w
( r  <bag  i ) z  ->  ( x `  w )  =  ( y `  w ) ) )  \/  x  =  y ) ) } >. ) ) )
Colors of variables: wff set class
This definition is referenced by:  reldmopsr  16231  opsrval  16232
  Copyright terms: Public domain W3C validator