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 eqid ⊢ ≤ O = ≤ O
8 simprl ⊢ φ ∧ I ∈ V ∧ R ∈ V → I ∈ V
9 simprr ⊢ φ ∧ I ∈ V ∧ R ∈ V → R ∈ V
10 3 adantr ⊢ φ ∧ I ∈ V ∧ R ∈ V → T ⊆ I × I
11 1 2 7 8 9 10 opsrval2 ⊢ φ ∧ I ∈ V ∧ R ∈ V → O = S sSet ≤ ndx ≤ O
12 11 fveq2d ⊢ φ ∧ I ∈ V ∧ R ∈ V → E ⁡ O = E ⁡ S sSet ≤ ndx ≤ O
13 4 5 ndxid ⊢ E = Slot E ⁡ ndx
14 5 nnrei ⊢ N ∈ ℝ
15 14 6 ltneii ⊢ N ≠ 10
16 4 5 ndxarg ⊢ E ⁡ ndx = N
17 plendx ⊢ ≤ ndx = 10
18 16 17 neeq12i ⊢ E ⁡ ndx ≠ ≤ ndx ↔ N ≠ 10
19 15 18 mpbir ⊢ E ⁡ ndx ≠ ≤ ndx
20 13 19 setsnid ⊢ E ⁡ S = E ⁡ S sSet ≤ ndx ≤ O
21 12 20 syl6reqr ⊢ φ ∧ 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