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