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) (Revised by AV, 1-Nov-2024)

Ref Expression
Hypotheses opsrbas.s 𝑆 = ( 𝐼 mPwSer 𝑅 )
opsrbas.o 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 )
opsrbas.t ( 𝜑𝑇 ⊆ ( 𝐼 × 𝐼 ) )
opsrbaslem.1 𝐸 = Slot ( 𝐸 ‘ ndx )
opsrbaslem.2 ( 𝐸 ‘ ndx ) ≠ ( le ‘ ndx )
Assertion opsrbaslem ( 𝜑 → ( 𝐸𝑆 ) = ( 𝐸𝑂 ) )

Proof

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