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	⊢ ( 𝜑 → ( 𝐸 ‘ 𝑆 ) = ( 𝐸 ‘ 𝑂 ) )

Metamath Proof Explorer

Theorem opsrbaslem

Proof