Metamath Proof Explorer


Theorem opsrbas

Description: The base set of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015) (Revised by Mario Carneiro, 30-Aug-2015) (Revised by AV, 1-Nov-2024)

Ref Expression
Hypotheses opsrbas.s
|- S = ( I mPwSer R )
opsrbas.o
|- O = ( ( I ordPwSer R ) ` T )
opsrbas.t
|- ( ph -> T C_ ( I X. I ) )
Assertion opsrbas
|- ( ph -> ( Base ` S ) = ( Base ` O ) )

Proof

Step Hyp Ref Expression
1 opsrbas.s
 |-  S = ( I mPwSer R )
2 opsrbas.o
 |-  O = ( ( I ordPwSer R ) ` T )
3 opsrbas.t
 |-  ( ph -> T C_ ( I X. I ) )
4 baseid
 |-  Base = Slot ( Base ` ndx )
5 plendxnbasendx
 |-  ( le ` ndx ) =/= ( Base ` ndx )
6 5 necomi
 |-  ( Base ` ndx ) =/= ( le ` ndx )
7 1 2 3 4 6 opsrbaslem
 |-  ( ph -> ( Base ` S ) = ( Base ` O ) )