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 ) , .<_ >. ) )