Theorem opsrbaslemOLD

Description: Obsolete version of opsrbaslem as of 1-Nov-2024. 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) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	opsrbas.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
	opsrbas.o	⊢ 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 )
	opsrbas.t	⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐼 × 𝐼 ) )
	opsrbaslemOLD.1	⊢ 𝐸 = Slot 𝑁
	opsrbaslemOLD.2	⊢ 𝑁 ∈ ℕ
	opsrbaslemOLD.3	⊢ 𝑁 < ; 1 0
Assertion	opsrbaslemOLD	⊢ ( 𝜑 → ( 𝐸 ‘ 𝑆 ) = ( 𝐸 ‘ 𝑂 ) )

Proof

Step	Hyp	Ref	Expression
1		opsrbas.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2		opsrbas.o	⊢ 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 )
3		opsrbas.t	⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐼 × 𝐼 ) )
4		opsrbaslemOLD.1	⊢ 𝐸 = Slot 𝑁
5		opsrbaslemOLD.2	⊢ 𝑁 ∈ ℕ
6		opsrbaslemOLD.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	⊢ ( 𝜑 → ( 𝐸 ‘ 𝑆 ) = ( 𝐸 ‘ 𝑂 ) )