This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opsrval2

Description: Self-referential expression for the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015)

Ref Expression
Hypotheses opsrval2.s 
|- S = ( I mPwSer R )
opsrval2.o 
|- O = ( ( I ordPwSer R ) ` T )
opsrval2.l 
|- .<_ = ( le ` O )
opsrval2.i 
|- ( ph -> I e. V )
opsrval2.r 
|- ( ph -> R e. W )
opsrval2.t 
|- ( ph -> T C_ ( I X. I ) )
Assertion opsrval2 
|- ( ph -> O = ( S sSet <. ( le ` ndx ) , .<_ >. ) )

Proof

Step Hyp Ref Expression
1 opsrval2.s 
 |-  S = ( I mPwSer R )
2 opsrval2.o 
 |-  O = ( ( I ordPwSer R ) ` T )
3 opsrval2.l 
 |-  .<_ = ( le ` O )
4 opsrval2.i 
 |-  ( ph -> I e. V )
5 opsrval2.r 
 |-  ( ph -> R e. W )
6 opsrval2.t 
 |-  ( ph -> T C_ ( I X. I ) )
7 eqid 
 |-  ( Base ` S ) = ( Base ` S )
8 eqid 
 |-  ( lt ` R ) = ( lt ` R )
9 eqid 
 |-  ( T
10 eqid 
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
11 eqid 
 |-  { <. x , y >. | ( { x , y } C_ ( Base ` S ) /\ ( E. z e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ( ( x ` z ) ( lt ` R ) ( y ` z ) /\ A. w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ( w ( T  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } = { <. x , y >. | ( { x , y } C_ ( Base ` S ) /\ ( E. z e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ( ( x ` z ) ( lt ` R ) ( y ` z ) /\ A. w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ( w ( T  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) }
12 1 2 7 8 9 10 11 4 5 6 opsrval 
 |-  ( ph -> O = ( S sSet <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ ( Base ` S ) /\ ( E. z e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ( ( x ` z ) ( lt ` R ) ( y ` z ) /\ A. w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ( w ( T  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) )
13 1 2 7 8 9 10 3 6 opsrle 
 |-  ( ph -> .<_ = { <. x , y >. | ( { x , y } C_ ( Base ` S ) /\ ( E. z e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ( ( x ` z ) ( lt ` R ) ( y ` z ) /\ A. w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ( w ( T  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } )
14 13 opeq2d 
 |-  ( ph -> <. ( le ` ndx ) , .<_ >. = <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ ( Base ` S ) /\ ( E. z e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ( ( x ` z ) ( lt ` R ) ( y ` z ) /\ A. w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ( w ( T  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. )
15 14 oveq2d 
 |-  ( ph -> ( S sSet <. ( le ` ndx ) , .<_ >. ) = ( S sSet <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ ( Base ` S ) /\ ( E. z e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ( ( x ` z ) ( lt ` R ) ( y ` z ) /\ A. w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ( w ( T  ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) )
16 12 15 eqtr4d 
 |-  ( ph -> O = ( S sSet <. ( le ` ndx ) , .<_ >. ) )