Metamath Proof Explorer

Theorem reldmopsr

Description: Lemma for ordered power series. (Contributed by Stefan O'Rear, 2-Oct-2015)

Ref Expression
Assertion reldmopsr 
|- Rel dom ordPwSer

Proof

Step Hyp Ref Expression
1 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 ) ) } >. ) ) )
2 1 reldmmpo 
 |-  Rel dom ordPwSer