Metamath Proof Explorer

Definition df-opsr

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)

Ref Expression
Assertion 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  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 copws 
 |-  ordPwSer
1 vi 
 |-  i
2 cvv 
 |-  _V
3 vs 
 |-  s
4 vr 
 |-  r
5 1 cv 
 |-  i
6 5 5 cxp 
 |-  ( i X. i )
7 6 cpw 
 |-  ~P ( i X. i )
8 cmps 
 |-  mPwSer
9 3 cv 
 |-  s
10 5 9 8 co 
 |-  ( i mPwSer s )
11 vp 
 |-  p
12 11 cv 
 |-  p
13 csts 
 |-  sSet
14 cple 
 |-  le
15 cnx 
 |-  ndx
16 15 14 cfv 
 |-  ( le ` ndx )
17 vx 
 |-  x
18 vy 
 |-  y
19 17 cv 
 |-  x
20 18 cv 
 |-  y
21 19 20 cpr 
 |-  { x , y }
22 cbs 
 |-  Base
23 12 22 cfv 
 |-  ( Base ` p )
24 21 23 wss 
 |-  { x , y } C_ ( Base ` p )
25 vh 
 |-  h
26 cn0 
 |-  NN0
27 cmap 
 |-  ^m
28 26 5 27 co 
 |-  ( NN0 ^m i )
29 25 cv 
 |-  h
30 29 ccnv 
 |-  `' h
31 cn 
 |-  NN
32 30 31 cima 
 |-  ( `' h " NN )
33 cfn 
 |-  Fin
34 32 33 wcel 
 |-  ( `' h " NN ) e. Fin
35 34 25 28 crab 
 |-  { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin }
36 vd 
 |-  d
37 vz 
 |-  z
38 36 cv 
 |-  d
39 37 cv 
 |-  z
40 39 19 cfv 
 |-  ( x ` z )
41 cplt 
 |-  lt
42 9 41 cfv 
 |-  ( lt ` s )
43 39 20 cfv 
 |-  ( y ` z )
44 40 43 42 wbr 
 |-  ( x ` z ) ( lt ` s ) ( y ` z )
45 vw 
 |-  w
46 45 cv 
 |-  w
47 4 cv 
 |-  r
48 cltb 
 |-
49 47 5 48 co 
 |-  ( r
50 46 39 49 wbr 
 |-  w ( r
51 46 19 cfv 
 |-  ( x ` w )
52 46 20 cfv 
 |-  ( y ` w )
53 51 52 wceq 
 |-  ( x ` w ) = ( y ` w )
54 50 53 wi 
 |-  ( w ( r  ( x ` w ) = ( y ` w ) )
55 54 45 38 wral 
 |-  A. w e. d ( w ( r  ( x ` w ) = ( y ` w ) )
56 44 55 wa 
 |-  ( ( x ` z ) ( lt ` s ) ( y ` z ) /\ A. w e. d ( w ( r  ( x ` w ) = ( y ` w ) ) )
57 56 37 38 wrex 
 |-  E. z e. d ( ( x ` z ) ( lt ` s ) ( y ` z ) /\ A. w e. d ( w ( r  ( x ` w ) = ( y ` w ) ) )
58 57 36 35 wsbc 
 |-  [. { 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  ( x ` w ) = ( y ` w ) ) )
59 19 20 wceq 
 |-  x = y
60 58 59 wo 
 |-  ( [. { 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  ( x ` w ) = ( y ` w ) ) ) \/ x = y )
61 24 60 wa 
 |-  ( { 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  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) )
62 61 17 18 copab 
 |-  { <. 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  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) }
63 16 62 cop 
 |-  <. ( 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  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >.
64 12 63 13 co 
 |-  ( 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  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. )
65 11 10 64 csb 
 |-  [_ ( 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  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. )
66 4 7 65 cmpt 
 |-  ( 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  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) )
67 1 3 2 2 66 cmpo 
 |-  ( 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  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) ) )
68 0 67 wceq 
 |-  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  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) ) )