Metamath Proof Explorer


Theorem opsrbaslem

Description: Get a component of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015) (Revised by Mario Carneiro, 2-Oct-2015) (Revised by AV, 9-Sep-2021)

Ref Expression
Hypotheses opsrbas.s S = I mPwSer R
opsrbas.o O = I ordPwSer R T
opsrbas.t φ T I × I
opsrbaslem.1 E = Slot N
opsrbaslem.2 N
opsrbaslem.3 N < 10
Assertion opsrbaslem φ E S = E O

Proof

Step Hyp Ref Expression
1 opsrbas.s S = I mPwSer R
2 opsrbas.o O = I ordPwSer R T
3 opsrbas.t φ T I × I
4 opsrbaslem.1 E = Slot N
5 opsrbaslem.2 N
6 opsrbaslem.3 N < 10
7 4 5 ndxid E = Slot E ndx
8 5 nnrei N
9 8 6 ltneii N 10
10 4 5 ndxarg E ndx = N
11 plendx ndx = 10
12 10 11 neeq12i E ndx ndx N 10
13 9 12 mpbir E ndx ndx
14 7 13 setsnid E S = E S sSet ndx O
15 eqid O = O
16 simprl φ I V R V I V
17 simprr φ I V R V R V
18 3 adantr φ I V R V T I × I
19 1 2 15 16 17 18 opsrval2 φ I V R V O = S sSet ndx O
20 19 fveq2d φ I V R V E O = E S sSet ndx O
21 14 20 eqtr4id φ I V R V E S = E O
22 0fv T =
23 22 eqcomi = T
24 reldmpsr Rel dom mPwSer
25 24 ovprc ¬ I V R V I mPwSer R =
26 reldmopsr Rel dom ordPwSer
27 26 ovprc ¬ I V R V I ordPwSer R =
28 27 fveq1d ¬ I V R V I ordPwSer R T = T
29 23 25 28 3eqtr4a ¬ I V R V I mPwSer R = I ordPwSer R T
30 29 adantl φ ¬ I V R V I mPwSer R = I ordPwSer R T
31 30 1 2 3eqtr4g φ ¬ I V R V S = O
32 31 fveq2d φ ¬ I V R V E S = E O
33 21 32 pm2.61dan φ E S = E O