Metamath Proof Explorer

Theorem opsrval

Description: The value of the "ordered power series" function. This is the same as mPwSer psrval , but with the addition of a well-order on I we can turn a strict order on R into a strict order on the power series structure. (Contributed by Mario Carneiro, 8-Feb-2015)

Ref Expression
Hypotheses opsrval.s 
|- S = ( I mPwSer R )
opsrval.o 
|- O = ( ( I ordPwSer R ) ` T )
opsrval.b 
|- B = ( Base ` S )
opsrval.q 
|- .< = ( lt ` R )
opsrval.c 
|- C = ( T
opsrval.d 
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
opsrval.l 
|- .<_ = { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) }
opsrval.i 
|- ( ph -> I e. V )
opsrval.r 
|- ( ph -> R e. W )
opsrval.t 
|- ( ph -> T C_ ( I X. I ) )
Assertion opsrval 
|- ( ph -> O = ( S sSet <. ( le ` ndx ) , .<_ >. ) )

Proof

Step Hyp Ref Expression
1 opsrval.s 
 |-  S = ( I mPwSer R )
2 opsrval.o 
 |-  O = ( ( I ordPwSer R ) ` T )
3 opsrval.b 
 |-  B = ( Base ` S )
4 opsrval.q 
 |-  .< = ( lt ` R )
5 opsrval.c 
 |-  C = ( T
6 opsrval.d 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
7 opsrval.l 
 |-  .<_ = { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) }
8 opsrval.i 
 |-  ( ph -> I e. V )
9 opsrval.r 
 |-  ( ph -> R e. W )
10 opsrval.t 
 |-  ( ph -> T C_ ( I X. I ) )
11 8 elexd 
 |-  ( ph -> I e. _V )
12 9 elexd 
 |-  ( ph -> R e. _V )
13 8 8 xpexd 
 |-  ( ph -> ( I X. I ) e. _V )
14 pwexg 
 |-  ( ( I X. I ) e. _V -> ~P ( I X. I ) e. _V )
15 mptexg 
 |-  ( ~P ( I X. I ) e. _V -> ( r e. ~P ( I X. I ) |-> ( S sSet <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) ) e. _V )
16 13 14 15 3syl 
 |-  ( ph -> ( r e. ~P ( I X. I ) |-> ( S sSet <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) ) e. _V )
17 simpl 
 |-  ( ( i = I /\ s = R ) -> i = I )
18 17 sqxpeqd 
 |-  ( ( i = I /\ s = R ) -> ( i X. i ) = ( I X. I ) )
19 18 pweqd 
 |-  ( ( i = I /\ s = R ) -> ~P ( i X. i ) = ~P ( I X. I ) )
20 ovexd 
 |-  ( ( i = I /\ s = R ) -> ( i mPwSer s ) e. _V )
21 id 
 |-  ( p = ( i mPwSer s ) -> p = ( i mPwSer s ) )
22 oveq12 
 |-  ( ( i = I /\ s = R ) -> ( i mPwSer s ) = ( I mPwSer R ) )
23 21 22 sylan9eqr 
 |-  ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> p = ( I mPwSer R ) )
24 23 1 eqtr4di 
 |-  ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> p = S )
25 24 fveq2d 
 |-  ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> ( Base ` p ) = ( Base ` S ) )
26 25 3 eqtr4di 
 |-  ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> ( Base ` p ) = B )
27 26 sseq2d 
 |-  ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> ( { x , y } C_ ( Base ` p ) <-> { x , y } C_ B ) )
28 ovex 
 |-  ( NN0 ^m i ) e. _V
29 28 rabex 
 |-  { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } e. _V
30 29 a1i 
 |-  ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } e. _V )
31 17 adantr 
 |-  ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> i = I )
32 31 oveq2d 
 |-  ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> ( NN0 ^m i ) = ( NN0 ^m I ) )
33 rabeq 
 |-  ( ( NN0 ^m i ) = ( NN0 ^m I ) -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
34 32 33 syl 
 |-  ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
35 34 6 eqtr4di 
 |-  ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } = D )
36 simpr 
 |-  ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> d = D )
37 simpllr 
 |-  ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> s = R )
38 37 fveq2d 
 |-  ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> ( lt ` s ) = ( lt ` R ) )
39 38 4 eqtr4di 
 |-  ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> ( lt ` s ) = .< )
40 39 breqd 
 |-  ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> ( ( x ` z ) ( lt ` s ) ( y ` z ) <-> ( x ` z ) .< ( y ` z ) ) )
41 31 adantr 
 |-  ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> i = I )
42 41 oveq2d 
 |-  ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> ( r
43 42 breqd 
 |-  ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> ( w ( r  w ( r
44 43 imbi1d 
 |-  ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> ( ( w ( r  ( x ` w ) = ( y ` w ) ) <-> ( w ( r  ( x ` w ) = ( y ` w ) ) ) )
45 36 44 raleqbidv 
 |-  ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> ( A. w e. d ( w ( r  ( x ` w ) = ( y ` w ) ) <-> A. w e. D ( w ( r  ( x ` w ) = ( y ` w ) ) ) )
46 40 45 anbi12d 
 |-  ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> ( ( ( x ` z ) ( lt ` s ) ( y ` z ) /\ A. w e. d ( w ( r  ( x ` w ) = ( y ` w ) ) ) <-> ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r  ( x ` w ) = ( y ` w ) ) ) ) )
47 36 46 rexeqbidv 
 |-  ( ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) /\ d = D ) -> ( E. z e. d ( ( x ` z ) ( lt ` s ) ( y ` z ) /\ A. w e. d ( w ( r  ( x ` w ) = ( y ` w ) ) ) <-> E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r  ( x ` w ) = ( y ` w ) ) ) ) )
48 30 35 47 sbcied2 
 |-  ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> ( [. { 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 ) ) ) <-> E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r  ( x ` w ) = ( y ` w ) ) ) ) )
49 48 orbi1d 
 |-  ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> ( ( [. { 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 ) <-> ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) )
50 27 49 anbi12d 
 |-  ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> ( ( { 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 ) ) <-> ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) ) )
51 50 opabbidv 
 |-  ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> { <. 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 ) ) } = { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } )
52 51 opeq2d 
 |-  ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> <. ( 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 ) ) } >. = <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. )
53 24 52 oveq12d 
 |-  ( ( ( i = I /\ s = R ) /\ p = ( i mPwSer s ) ) -> ( 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 ) ) } >. ) = ( S sSet <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) )
54 20 53 csbied 
 |-  ( ( i = I /\ s = R ) -> [_ ( 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 ) ) } >. ) = ( S sSet <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) )
55 19 54 mpteq12dv 
 |-  ( ( i = I /\ s = R ) -> ( 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 ) ) } >. ) ) = ( r e. ~P ( I X. I ) |-> ( S sSet <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) ) )
56 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 ) ) } >. ) ) )
57 55 56 ovmpoga 
 |-  ( ( I e. _V /\ R e. _V /\ ( r e. ~P ( I X. I ) |-> ( S sSet <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) ) e. _V ) -> ( I ordPwSer R ) = ( r e. ~P ( I X. I ) |-> ( S sSet <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) ) )
58 11 12 16 57 syl3anc 
 |-  ( ph -> ( I ordPwSer R ) = ( r e. ~P ( I X. I ) |-> ( S sSet <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) ) )
59 simpr 
 |-  ( ( ph /\ r = T ) -> r = T )
60 59 oveq1d 
 |-  ( ( ph /\ r = T ) -> ( r
61 60 5 eqtr4di 
 |-  ( ( ph /\ r = T ) -> ( r
62 61 breqd 
 |-  ( ( ph /\ r = T ) -> ( w ( r  w C z ) )
63 62 imbi1d 
 |-  ( ( ph /\ r = T ) -> ( ( w ( r  ( x ` w ) = ( y ` w ) ) <-> ( w C z -> ( x ` w ) = ( y ` w ) ) ) )
64 63 ralbidv 
 |-  ( ( ph /\ r = T ) -> ( A. w e. D ( w ( r  ( x ` w ) = ( y ` w ) ) <-> A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) )
65 64 anbi2d 
 |-  ( ( ph /\ r = T ) -> ( ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r  ( x ` w ) = ( y ` w ) ) ) <-> ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) ) )
66 65 rexbidv 
 |-  ( ( ph /\ r = T ) -> ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r  ( x ` w ) = ( y ` w ) ) ) <-> E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) ) )
67 66 orbi1d 
 |-  ( ( ph /\ r = T ) -> ( ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) <-> ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) )
68 67 anbi2d 
 |-  ( ( ph /\ r = T ) -> ( ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) <-> ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) ) )
69 68 opabbidv 
 |-  ( ( ph /\ r = T ) -> { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } = { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } )
70 69 7 eqtr4di 
 |-  ( ( ph /\ r = T ) -> { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } = .<_ )
71 70 opeq2d 
 |-  ( ( ph /\ r = T ) -> <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. = <. ( le ` ndx ) , .<_ >. )
72 71 oveq2d 
 |-  ( ( ph /\ r = T ) -> ( S sSet <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w ( r  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) = ( S sSet <. ( le ` ndx ) , .<_ >. ) )
73 13 10 sselpwd 
 |-  ( ph -> T e. ~P ( I X. I ) )
74 ovexd 
 |-  ( ph -> ( S sSet <. ( le ` ndx ) , .<_ >. ) e. _V )
75 58 72 73 74 fvmptd 
 |-  ( ph -> ( ( I ordPwSer R ) ` T ) = ( S sSet <. ( le ` ndx ) , .<_ >. ) )
76 2 75 eqtrid 
 |-  ( ph -> O = ( S sSet <. ( le ` ndx ) , .<_ >. ) )