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 𝑆 = ( 𝐼 mPwSer 𝑅 )
opsrbas.o 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 )
opsrbas.t ( 𝜑𝑇 ⊆ ( 𝐼 × 𝐼 ) )
opsrbaslem.1 𝐸 = Slot 𝑁
opsrbaslem.2 𝑁 ∈ ℕ
opsrbaslem.3 𝑁 < 1 0
Assertion opsrbaslem ( 𝜑 → ( 𝐸𝑆 ) = ( 𝐸𝑂 ) )

Proof

Step Hyp Ref Expression
1 opsrbas.s 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 opsrbas.o 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 )
3 opsrbas.t ( 𝜑𝑇 ⊆ ( 𝐼 × 𝐼 ) )
4 opsrbaslem.1 𝐸 = Slot 𝑁
5 opsrbaslem.2 𝑁 ∈ ℕ
6 opsrbaslem.3 𝑁 < 1 0
7 4 5 ndxid 𝐸 = Slot ( 𝐸 ‘ ndx )
8 5 nnrei 𝑁 ∈ ℝ
9 8 6 ltneii 𝑁 1 0
10 4 5 ndxarg ( 𝐸 ‘ ndx ) = 𝑁
11 plendx ( le ‘ ndx ) = 1 0
12 10 11 neeq12i ( ( 𝐸 ‘ ndx ) ≠ ( le ‘ ndx ) ↔ 𝑁 1 0 )
13 9 12 mpbir ( 𝐸 ‘ ndx ) ≠ ( le ‘ ndx )
14 7 13 setsnid ( 𝐸𝑆 ) = ( 𝐸 ‘ ( 𝑆 sSet ⟨ ( le ‘ ndx ) , ( le ‘ 𝑂 ) ⟩ ) )
15 eqid ( le ‘ 𝑂 ) = ( le ‘ 𝑂 )
16 simprl ( ( 𝜑 ∧ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ) → 𝐼 ∈ V )
17 simprr ( ( 𝜑 ∧ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ) → 𝑅 ∈ V )
18 3 adantr ( ( 𝜑 ∧ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ) → 𝑇 ⊆ ( 𝐼 × 𝐼 ) )
19 1 2 15 16 17 18 opsrval2 ( ( 𝜑 ∧ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ) → 𝑂 = ( 𝑆 sSet ⟨ ( le ‘ ndx ) , ( le ‘ 𝑂 ) ⟩ ) )
20 19 fveq2d ( ( 𝜑 ∧ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ) → ( 𝐸𝑂 ) = ( 𝐸 ‘ ( 𝑆 sSet ⟨ ( le ‘ ndx ) , ( le ‘ 𝑂 ) ⟩ ) ) )
21 14 20 eqtr4id ( ( 𝜑 ∧ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ) → ( 𝐸𝑆 ) = ( 𝐸𝑂 ) )
22 0fv ( ∅ ‘ 𝑇 ) = ∅
23 22 eqcomi ∅ = ( ∅ ‘ 𝑇 )
24 reldmpsr Rel dom mPwSer
25 24 ovprc ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝐼 mPwSer 𝑅 ) = ∅ )
26 reldmopsr Rel dom ordPwSer
27 26 ovprc ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝐼 ordPwSer 𝑅 ) = ∅ )
28 27 fveq1d ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 ) = ( ∅ ‘ 𝑇 ) )
29 23 25 28 3eqtr4a ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝐼 mPwSer 𝑅 ) = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 ) )
30 29 adantl ( ( 𝜑 ∧ ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ) → ( 𝐼 mPwSer 𝑅 ) = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 ) )
31 30 1 2 3eqtr4g ( ( 𝜑 ∧ ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ) → 𝑆 = 𝑂 )
32 31 fveq2d ( ( 𝜑 ∧ ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) ) → ( 𝐸𝑆 ) = ( 𝐸𝑂 ) )
33 21 32 pm2.61dan ( 𝜑 → ( 𝐸𝑆 ) = ( 𝐸𝑂 ) )