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 syl5eq
 |-  ( ph -> O = ( S sSet <. ( le ` ndx ) , .<_ >. ) )